Library HoTT.Homotopy.Cover

Require Import Basics Types HFiber Truncations.Core Truncations.SeparatedTrunc Pointed
  Modalities.ReflectiveSubuniverse.

Local Open Scope pointed_scope.

O-connected covers

Given a reflective subuniverse O, for any type X and x : O X, the O-connected cover of X at x is the fibre of to O X at x.
Definition O_cover@{u} `{O : ReflectiveSubuniverse@{u}}
  (X : Type@{u}) (x : O X) : Type@{u}
  := hfiber (to O _) x.

The "O-connected" cover is in fact O-connected when O is a modality, using isconnected_hfiber_conn_map. Since Coq can infer this using typeclasses, we don't restate it here.
Characterization of paths in O_cover is given by equiv_path_hfiber.

(* If x is an actual point of X, then the connected cover is pointed. *)
Definition O_pcover@{u} (O : ReflectiveSubuniverse@{u})
  (X : Type@{u}) (x : X) : pType@{u}
  := pfiber@{u u u} (pto O [X,x]).

Covers commute with products
Definition O_pcover_prod `{O : ReflectiveSubuniverse} {X Y : pType@{u}}
  : O_pcover O (X × Y) pt <~>* [(O_pcover O X pt) × (O_pcover O Y pt), _].
Proof.
  srapply Build_pEquiv'.
  { refine (_ oE equiv_functor_sigma_id _).
    2: intro; nrapply equiv_path_O_prod.
    nrapply equiv_sigma_prod_prod. }
  nrapply path_prod; cbn.
  all: snrapply path_sigma'.
  1,3: exact idpath.
  all: cbn.
  all: by rewrite concat_p1, concat_Vp.
Defined.

Functoriality of O_cover

Given X and x : O X, any map f : X → Y out of X induces a map O_cover X x → O_cover Y (O_functor O f x).
Definition functor_O_cover@{u v} `{O : ReflectiveSubuniverse} {X Y : Type@{u}}
  (f : X → Y) (x : O X) : O_cover@{u} X x → O_cover@{u} Y (O_functor O f x)
  := functor_hfiber (f:=to O _) (g:=to O _)
       (h:=f) (k:=O_functor O f) (to_O_natural O f) x.

Definition equiv_functor_O_cover `{O : ReflectiveSubuniverse}
  {X Y : Type} (f : X → Y) `{IsEquiv _ _ f} (x : O X)
  : O_cover X x <~> O_cover Y (O_functor O f x)
  := Build_Equiv _ _ (functor_O_cover f x) _.

Pointed functoriality


Definition pfunctor_O_pcover `{O : ReflectiveSubuniverse} {X Y : pType}
  (f : X ->* Y) : O_pcover O X pt ->* O_pcover O Y pt
  := functor_pfiber (pto_O_natural O f).

Definition pequiv_pfunctor_O_pcover `{O : ReflectiveSubuniverse} {X Y : pType}
  (f : X ->* Y) `{IsEquiv _ _ f} : O_pcover O X pt <~>* O_pcover O Y pt
  := Build_pEquiv _ _ (pfunctor_O_pcover f) _.

In the case of truncations, ptr_natural gives a better proof of pointedness.
Definition pfunctor_pTr_pcover `{n : trunc_index} {X Y : pType}
  (f : X ->* Y) : O_pcover (Tr n) X pt ->* O_pcover (Tr n) Y pt
  := functor_pfiber (ptr_natural n f).

Definition pequiv_pfunctor_pTr_pcover `{n : trunc_index}
  {X Y : pType} (f : X ->* Y) `{IsEquiv _ _ f}
  : O_pcover (Tr n) X pt <~>* O_pcover (Tr n) Y pt
  := Build_pEquiv _ _ (pfunctor_pTr_pcover f) _.

Components

Path components are given by specializing to O being set-truncation.
Definition comp := O_cover (O:=Tr 0).
Definition pcomp := O_pcover (Tr 0).

Definition pfunctor_pcomp {X Y : pType} := @pfunctor_pTr_pcover (-1) X Y.
Definition pequiv_pfunctor_pcomp {X Y : pType}
  := @pequiv_pfunctor_pTr_pcover (-1) X Y.

If a property holds at a given point, then it holds for the whole component. This yields equivalences like the following:
Definition equiv_comp_property `{Univalence} {X : Type} (x : X)
  (P : X → Type) `{∀ x, IsHProp (P x)} (Px : P x)
  : comp (sig P) (tr (x; Px)) <~> comp X (tr x).
Proof.
  unfold comp, O_cover, hfiber. simpl.
  refine (_ oE (equiv_sigma_assoc _ _)^-1).
  apply equiv_functor_sigma_id; intro y.
  apply equiv_iff_hprop.
  - intros [py q].
    exact (ap (Trunc_functor _ pr1) q).
  - refine (equiv_ind (equiv_path_Tr _ _) _ _).
    apply Trunc_rec; intros p; induction p.
    exact (Px; idpath).
Defined.

For example, we may take components of equivalences among underlying maps.
Definition equiv_comp_equiv_map `{Univalence} {A B : Type} (e : A <~> B)
  : comp (A <~> B) (tr e) <~> comp (A → B) (tr (equiv_fun e)).
Proof.
  refine (_ oE equiv_functor_O_cover (issig_equiv _ _)^-1 _); cbn.
  rapply equiv_comp_property.
Defined.