Require Import Basics Types HFiber Truncations.Core Truncations.SeparatedTrunc Pointed
  Modalities.ReflectiveSubuniverse.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

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), _].
O: ReflectiveSubuniverse
X, Y: pType
O_pcover O (X * Y) pt <~>*
O_pcover O X pt * O_pcover O Y pt
Proof.
O: ReflectiveSubuniverse
X, Y: pType
O_pcover O (X * Y) pt <~>*
O_pcover O X pt * O_pcover O Y pt
  srapply Build_pEquiv'.
O: ReflectiveSubuniverse
X, Y: pType
O_pcover O (X * Y) pt <~>
[O_pcover O X pt * O_pcover O Y pt, ispointed_prod]
O: ReflectiveSubuniverse
X, Y: pType
?f pt = pt
  {
O: ReflectiveSubuniverse
X, Y: pType
O_pcover O (X * Y) pt <~>
[O_pcover O X pt * O_pcover O Y pt, ispointed_prod] refine (_ oE equiv_functor_sigma_id _).
O: ReflectiveSubuniverse
X, Y: pType
{x : _ & ?Goal0 x} <~>
[O_pcover O X pt * O_pcover O Y pt, ispointed_prod]
O: ReflectiveSubuniverse
X, Y: pType
forall a : [X * Y, pt],
pto O [X * Y, pt] a = pt <~> ?Goal0 a
    2: intro; nrapply equiv_path_O_prod.
O: ReflectiveSubuniverse
X, Y: pType
{a : [X * Y, pt] &
((to O X (fst a) = to O X pt) *
 (to O Y (snd a) = to O Y pt))%type} <~>
[O_pcover O X pt * O_pcover O Y pt, ispointed_prod]
    nrapply equiv_sigma_prod_prod. }
O: ReflectiveSubuniverse
X, Y: pType
(equiv_sigma_prod_prod
   (fun x : [X, pt] => pto O [X, pt] x = pt)
   (fun x : [Y, pt] => pto O [Y, pt] x = pt)
 oE equiv_functor_sigma_id
      (fun a : [X * Y, pt] => equiv_path_O_prod O)) pt =
pt
  nrapply path_prod; cbn.
O: ReflectiveSubuniverse
X, Y: pType
(pt;
ap fst
  (((O_rec_beta (O_prod_unit O X Y) (pt, pt))^ @ 1) @
   O_rec_beta (O_prod_unit O X Y) (pt, pt))) = pt
O: ReflectiveSubuniverse
X, Y: pType
(pt;
ap snd
  (((O_rec_beta (O_prod_unit O X Y) (pt, pt))^ @ 1) @
   O_rec_beta (O_prod_unit O X Y) (pt, pt))) = pt
  all: snrapply path_sigma'.
O: ReflectiveSubuniverse
X, Y: pType
pt = pt
O: ReflectiveSubuniverse
X, Y: pType
transport (fun x : X => to O X x = ispointed_O X) 
  ?p
  (ap fst
     (((O_rec_beta (O_prod_unit O X Y) (pt, pt))^ @ 1) @
      O_rec_beta (O_prod_unit O X Y) (pt, pt))) =
point_eq (pto O [X, pt])
O: ReflectiveSubuniverse
X, Y: pType
pt = pt
O: ReflectiveSubuniverse
X, Y: pType
transport (fun x : Y => to O Y x = ispointed_O Y) 
  ?p0
  (ap snd
     (((O_rec_beta (O_prod_unit O X Y) (pt, pt))^ @ 1) @
      O_rec_beta (O_prod_unit O X Y) (pt, pt))) =
point_eq (pto O [Y, pt])
  1,3: exact idpath.
O: ReflectiveSubuniverse
X, Y: pType
transport (fun x : X => to O X x = ispointed_O X) 1
  (ap fst
     (((O_rec_beta (O_prod_unit O X Y) (pt, pt))^ @ 1) @
      O_rec_beta (O_prod_unit O X Y) (pt, pt))) =
point_eq (pto O [X, pt])
O: ReflectiveSubuniverse
X, Y: pType
transport (fun x : Y => to O Y x = ispointed_O Y) 1
  (ap snd
     (((O_rec_beta (O_prod_unit O X Y) (pt, pt))^ @ 1) @
      O_rec_beta (O_prod_unit O X Y) (pt, pt))) =
point_eq (pto O [Y, pt])
  all: cbn.
O: ReflectiveSubuniverse
X, Y: pType
ap fst
  (((O_rec_beta (O_prod_unit O X Y) (pt, pt))^ @ 1) @
   O_rec_beta (O_prod_unit O X Y) (pt, pt)) = 1
O: ReflectiveSubuniverse
X, Y: pType
ap snd
  (((O_rec_beta (O_prod_unit O X Y) (pt, pt))^ @ 1) @
   O_rec_beta (O_prod_unit O X Y) (pt, pt)) = 1
  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) `{forall x, IsHProp (P x)} (Px : P x)
  : comp (sig P) (tr (x; Px)) <~> comp X (tr x).
H: Univalence
X: Type
x: X
P: X -> Type
H0: forall x : X, IsHProp (P x)
Px: P x
comp {x : _ & P x} (tr (x; Px)) <~> comp X (tr x)
Proof.
H: Univalence
X: Type
x: X
P: X -> Type
H0: forall x : X, IsHProp (P x)
Px: P x
comp {x : _ & P x} (tr (x; Px)) <~> comp X (tr x)
  unfold comp, O_cover, hfiber.
H: Univalence
X: Type
x: X
P: X -> Type
H0: forall x : X, IsHProp (P x)
Px: P x
{x0 : {x : _ & P x} &
to (Tr 0) {x : _ & P x} x0 = tr (x; Px)} <~>
{x0 : X & to (Tr 0) X x0 = tr x} simpl.
H: Univalence
X: Type
x: X
P: X -> Type
H0: forall x : X, IsHProp (P x)
Px: P x
{x0 : {x : _ & P x} & tr x0 = tr (x; Px)} <~>
{x0 : X & tr x0 = tr x}
  refine (_ oE (equiv_sigma_assoc _ _)^-1).
H: Univalence
X: Type
x: X
P: X -> Type
H0: forall x : X, IsHProp (P x)
Px: P x
{a : X & {p : P a & tr (a; p) = tr (x; Px)}} <~>
{x0 : X & tr x0 = tr x}
  apply equiv_functor_sigma_id; intro y.
H: Univalence
X: Type
x: X
P: X -> Type
H0: forall x : X, IsHProp (P x)
Px: P x
y: X
{p : P y & tr (y; p) = tr (x; Px)} <~> tr y = tr x
  apply equiv_iff_hprop.
H: Univalence
X: Type
x: X
P: X -> Type
H0: forall x : X, IsHProp (P x)
Px: P x
y: X
{p : P y & tr (y; p) = tr (x; Px)} -> tr y = tr x
H: Univalence
X: Type
x: X
P: X -> Type
H0: forall x : X, IsHProp (P x)
Px: P x
y: X
tr y = tr x -> {p : P y & tr (y; p) = tr (x; Px)}
  -
H: Univalence
X: Type
x: X
P: X -> Type
H0: forall x : X, IsHProp (P x)
Px: P x
y: X
{p : P y & tr (y; p) = tr (x; Px)} -> tr y = tr x intros [py q].
H: Univalence
X: Type
x: X
P: X -> Type
H0: forall x : X, IsHProp (P x)
Px: P x
y: X
py: P y
q: tr (y; py) = tr (x; Px)
tr y = tr x
    exact (ap (Trunc_functor _ pr1) q).
  -
H: Univalence
X: Type
x: X
P: X -> Type
H0: forall x : X, IsHProp (P x)
Px: P x
y: X
tr y = tr x -> {p : P y & tr (y; p) = tr (x; Px)} refine (equiv_ind (equiv_path_Tr _ _) _ _).
H: Univalence
X: Type
x: X
P: X -> Type
H0: forall x : X, IsHProp (P x)
Px: P x
y: X
Tr (-1) (y = x) -> {p : P y & tr (y; p) = tr (x; Px)}
    apply Trunc_rec; intros p; induction p.
H: Univalence
X: Type
P: X -> Type
H0: forall x : X, IsHProp (P x)
y: X
Px: P y
{p : P y & tr (y; p) = tr (y; Px)}
    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)).
H: Univalence
A, B: Type
e: A <~> B
comp (A <~> B) (tr e) <~> comp (A -> B) (tr e)
Proof.
H: Univalence
A, B: Type
e: A <~> B
comp (A <~> B) (tr e) <~> comp (A -> B) (tr e)
  refine (_ oE equiv_functor_O_cover (issig_equiv _ _)^-1 _); cbn.
H: Univalence
A, B: Type
e: A <~> B
O_cover {f : A -> B & IsEquiv f}
  (tr (e; equiv_isequiv e)) <~> comp (A -> B) (tr e)
  rapply equiv_comp_property.
Defined.