Require Import Basics Types WildCat Truncations
  Pointed.Core Pointed.pEquiv Pointed.Loops Pointed.pModality.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

Local Open Scope pointed_scope.

(** * Truncations of pointed types *)

(** TODO: Many things here can be generalized to any modality or any reflective subuniverse, and could be moved to pModality.v *)

Definition pTr (n : trunc_index) (A : pType) : pType
  := [Tr n A, _].

(** We specialize [pto] and [pequiv_pto] from pModalities.v to truncations. *)

Definition ptr {n : trunc_index} {A : pType} : A ->* pTr n A
  := pto (Tr n) _.

Definition pequiv_ptr {n : trunc_index} {A : pType} `{IsTrunc n A}
  : A <~>* pTr n A := @pequiv_pto (Tr n) A _.

(** We could specialize [pO_rec] to give the following result, but since maps induced by truncation-recursion compute on elements of the form [tr _], we can give a better proof of pointedness than the one coming from [pO_rec]. *)
Definition pTr_rec n {X Y : pType} `{IsTrunc n Y} (f : X ->* Y)
  : pTr n X ->* Y
  := Build_pMap (pTr n X) Y (Trunc_rec f) (point_eq f).

(** Note that we get an equality of pointed functions here, without Funext, while [pO_rec_beta] only gives a pointed homotopy. This is because [pTr_rec] computes on elements of the form [tr _]. *)
Definition pTr_rec_beta_path n {X Y : pType} `{IsTrunc n Y} (f : X ->* Y)
  : pTr_rec n f o* ptr = f.
n: trunc_index
X, Y: pType
IsTrunc0: IsTrunc n Y
f: X ->* Y
pTr_rec n f o* ptr = f
Proof.
n: trunc_index
X, Y: pType
IsTrunc0: IsTrunc n Y
f: X ->* Y
pTr_rec n f o* ptr = f
  unfold pTr_rec, "o*"; cbn.
n: trunc_index
X, Y: pType
IsTrunc0: IsTrunc n Y
f: X ->* Y
Build_pMap X Y (fun x : X => f x) (1 @ point_eq f) = f
  (* Since [f] is definitionally equal to [Build_pMap _ _ f (point_eq f)], this works: *)
  apply (ap (Build_pMap _ _ f)).
n: trunc_index
X, Y: pType
IsTrunc0: IsTrunc n Y
f: X ->* Y
1 @ point_eq f = dpoint_eq f
  apply concat_1p.
Defined.

(** The version with a pointed homotopy. *)
Definition pTr_rec_beta n {X Y : pType} `{IsTrunc n Y} (f : X ->* Y)
  : pTr_rec n f o* ptr ==* f
  := phomotopy_path (pTr_rec_beta_path n f).

(** A pointed version of the induction principle. *)
Definition pTr_ind n {X : pType} {Y : pFam (pTr n X)} `{forall x, IsTrunc n (Y x)}
  (f : pForall X (Build_pFam (Y o tr) (dpoint Y)))
  : pForall (pTr n X) Y
  := Build_pForall (pTr n X) Y (Trunc_ind Y f) (dpoint_eq f).

Definition pequiv_ptr_rec `{Funext} {n} {X Y : pType} `{IsTrunc n Y}
  : (pTr n X ->** Y) <~>* (X ->** Y)
  := pequiv_o_pto_O _ X Y.

(** ** Functoriality of [pTr] *)

Global Instance is0functor_ptr n : Is0Functor (pTr n).
n: trunc_index
Is0Functor (pTr n)
Proof.
n: trunc_index
Is0Functor (pTr n)
  apply Build_Is0Functor.
n: trunc_index
forall a b : pType, (a $-> b) -> pTr n a $-> pTr n b
  intros X Y f.
n: trunc_index
X, Y: pType
f: X $-> Y
pTr n X $-> pTr n Y
  exact (pTr_rec _ (ptr o* f)).
Defined.

Global Instance is1functor_ptr n : Is1Functor (pTr n).
n: trunc_index
Is1Functor (pTr n)
Proof.
n: trunc_index
Is1Functor (pTr n)
  apply Build_Is1Functor.
n: trunc_index
forall (a b : pType) (f g : a $-> b),
f $== g -> fmap (pTr n) f $== fmap (pTr n) g
n: trunc_index
forall a : pType, fmap (pTr n) (Id a) $== Id (pTr n a)
n: trunc_index
forall (a b c : pType) (f : a $-> b) (g : b $-> c),
fmap (pTr n) (g $o f) $==
fmap (pTr n) g $o fmap (pTr n) f
  -
n: trunc_index
forall (a b : pType) (f g : a $-> b),
f $== g -> fmap (pTr n) f $== fmap (pTr n) g intros X Y f g p.
n: trunc_index
X, Y: pType
f, g: X $-> Y
p: f $== g
fmap (pTr n) f $== fmap (pTr n) g
    srapply pTr_ind; cbn.
n: trunc_index
X, Y: pType
f, g: X $-> Y
p: f $== g
pForall X
  {|
    pfam_pr1 := fun x : X => tr (f x) = tr (g x);
    dpoint :=
      (ap tr (point_eq f) @ 1) @
      (ap tr (point_eq g) @ 1)^
  |}
    snrapply Build_pForall.
n: trunc_index
X, Y: pType
f, g: X $-> Y
p: f $== g
forall x : X,
{|
  pfam_pr1 := fun x0 : X => tr (f x0) = tr (g x0);
  dpoint :=
    (ap tr (point_eq f) @ 1) @
    (ap tr (point_eq g) @ 1)^
|} x
n: trunc_index
X, Y: pType
f, g: X $-> Y
p: f $== g
?pointed_fun pt =
dpoint
  {|
    pfam_pr1 := fun x : X => tr (f x) = tr (g x);
    dpoint :=
      (ap tr (point_eq f) @ 1) @
      (ap tr (point_eq g) @ 1)^
  |}
    +
n: trunc_index
X, Y: pType
f, g: X $-> Y
p: f $== g
forall x : X,
{|
  pfam_pr1 := fun x0 : X => tr (f x0) = tr (g x0);
  dpoint :=
    (ap tr (point_eq f) @ 1) @
    (ap tr (point_eq g) @ 1)^
|} x cbn.
n: trunc_index
X, Y: pType
f, g: X $-> Y
p: f $== g
forall x : X, tr (f x) = tr (g x) exact (fun x => ap tr (p x)).
    +
n: trunc_index
X, Y: pType
f, g: X $-> Y
p: f $== g
((fun x : X => ap tr (p x))
 :
 forall x : X,
 {|
   pfam_pr1 := fun x0 : X => tr (f x0) = tr (g x0);
   dpoint :=
     (ap tr (point_eq f) @ 1) @
     (ap tr (point_eq g) @ 1)^
 |} x) pt =
dpoint
  {|
    pfam_pr1 := fun x : X => tr (f x) = tr (g x);
    dpoint :=
      (ap tr (point_eq f) @ 1) @
      (ap tr (point_eq g) @ 1)^
  |} pointed_reduce.
n: trunc_index
X: Type
point0: IsPointed X
Y: Type
f, g: X -> Y
p: forall x : X, f x = g x
ap tr (p point0) = (ap tr (p point0 @ 1) @ 1) @ 1
      exact (concat_p1 _ @ concat_p1 _ @ ap _ (concat_p1 _))^.
  -
n: trunc_index
forall a : pType, fmap (pTr n) (Id a) $== Id (pTr n a) intros X.
n: trunc_index
X: pType
fmap (pTr n) (Id X) $== Id (pTr n X)
    srapply Build_pHomotopy.
n: trunc_index
X: pType
fmap (pTr n) (Id X) == Id (pTr n X)
n: trunc_index
X: pType
?p pt =
dpoint_eq (fmap (pTr n) (Id X)) @
(dpoint_eq (Id (pTr n X)))^
    1: apply Trunc_rec_tr.
n: trunc_index
X: pType
Trunc_rec_tr n pt =
dpoint_eq (fmap (pTr n) (Id X)) @
(dpoint_eq (Id (pTr n X)))^
    cbn.
n: trunc_index
X: pType
1 = 1 reflexivity.
  -
n: trunc_index
forall (a b c : pType) (f : a $-> b) 
(g : b $-> c),
fmap (pTr n) (g $o f) $==
fmap (pTr n) g $o fmap (pTr n) f intros X Y Z f g.
n: trunc_index
X, Y, Z: pType
f: X $-> Y
g: Y $-> Z
fmap (pTr n) (g $o f) $==
fmap (pTr n) g $o fmap (pTr n) f
    srapply Build_pHomotopy.
n: trunc_index
X, Y, Z: pType
f: X $-> Y
g: Y $-> Z
fmap (pTr n) (g $o f) ==
fmap (pTr n) g $o fmap (pTr n) f
n: trunc_index
X, Y, Z: pType
f: X $-> Y
g: Y $-> Z
?p pt =
dpoint_eq (fmap (pTr n) (g $o f)) @
(dpoint_eq (fmap (pTr n) g $o fmap (pTr n) f))^
    1: by rapply Trunc_ind.
n: trunc_index
X, Y, Z: pType
f: X $-> Y
g: Y $-> Z
Trunc_ind
  (fun aa : Trunc n X =>
   fmap (pTr n) (g $o f) aa =
   (fmap (pTr n) g $o fmap (pTr n) f) aa)
  (fun a : X => 1) pt =
dpoint_eq (fmap (pTr n) (g $o f)) @
(dpoint_eq (fmap (pTr n) g $o fmap (pTr n) f))^
    by pointed_reduce.
Defined.

(** Naturality of [ptr].  Note that we get a equality of pointed functions, not just a pointed homotopy. *)
Definition ptr_natural_path (n : trunc_index) {X Y : pType} (f : X ->* Y)
  : fmap (pTr n) f o* ptr = ptr o* f
  := pTr_rec_beta_path n (ptr o* f).

(** The version with a pointed homotopy. *)
Definition ptr_natural (n : trunc_index) {X Y : pType} (f : X ->* Y)
  : fmap (pTr n) f o* ptr ==* ptr o* f
  := phomotopy_path (ptr_natural_path n f).

Definition ptr_functor_pconst {X Y : pType} n
  : fmap (pTr n) (@pconst X Y) ==* pconst.
X, Y: pType
n: trunc_index
fmap (pTr n) pconst ==* pconst
Proof.
X, Y: pType
n: trunc_index
fmap (pTr n) pconst ==* pconst
  srapply Build_pHomotopy.
X, Y: pType
n: trunc_index
fmap (pTr n) pconst == pconst
X, Y: pType
n: trunc_index
?p pt =
dpoint_eq (fmap (pTr n) pconst) @ (dpoint_eq pconst)^
  1: by rapply Trunc_ind.
X, Y: pType
n: trunc_index
Trunc_ind
  (fun aa : Trunc n X =>
   fmap (pTr n) pconst aa = pconst aa)
  (fun a : X => 1) pt =
dpoint_eq (fmap (pTr n) pconst) @ (dpoint_eq pconst)^
  reflexivity.
Defined.

Definition pequiv_ptr_functor {X Y : pType} (n : trunc_index) (f : X <~>* Y)
  : pTr n X <~>* pTr n Y
  := emap (pTr n) f.

Definition ptr_loops `{Univalence} (n : trunc_index) (A : pType)
  : pTr n (loops A) <~>* loops (pTr n.+1 A).
H: Univalence
n: trunc_index
A: pType
pTr n (loops A) <~>* loops (pTr n.+1 A)
Proof.
H: Univalence
n: trunc_index
A: pType
pTr n (loops A) <~>* loops (pTr n.+1 A)
  srapply Build_pEquiv'.
H: Univalence
n: trunc_index
A: pType
pTr n (loops A) <~> loops (pTr n.+1 A)
H: Univalence
n: trunc_index
A: pType
?f pt = pt
  1: apply equiv_path_Tr.
H: Univalence
n: trunc_index
A: pType
equiv_path_Tr pt pt pt = pt
  reflexivity.
Defined.

Definition ptr_iterated_loops `{Univalence} (n : trunc_index)
  (k : nat) (A : pType)
  : pTr n (iterated_loops k A) <~>* iterated_loops k (pTr (trunc_index_inc' n k) A).
H: Univalence
n: trunc_index
k: nat
A: pType
pTr n (iterated_loops k A) <~>*
iterated_loops k (pTr (trunc_index_inc' n k) A)
Proof.
H: Univalence
n: trunc_index
k: nat
A: pType
pTr n (iterated_loops k A) <~>*
iterated_loops k (pTr (trunc_index_inc' n k) A)
  revert A n.
H: Univalence
k: nat
forall (A : pType) (n : trunc_index),
pTr n (iterated_loops k A) <~>*
iterated_loops k (pTr (trunc_index_inc' n k) A)
  induction k.
H: Univalence
forall (A : pType) (n : trunc_index),
pTr n (iterated_loops 0 A) <~>*
iterated_loops 0 (pTr (trunc_index_inc' n 0) A)
H: Univalence
k: nat
IHk: forall (A : pType) (n : trunc_index),
pTr n (iterated_loops k A) <~>*
iterated_loops k (pTr (trunc_index_inc' n k) A)
forall (A : pType) (n : trunc_index),
pTr n (iterated_loops k.+1 A) <~>*
iterated_loops k.+1 (pTr (trunc_index_inc' n k.+1) A)
  {
H: Univalence
forall (A : pType) (n : trunc_index),
pTr n (iterated_loops 0 A) <~>*
iterated_loops 0 (pTr (trunc_index_inc' n 0) A) intros A n; cbn.
H: Univalence
A: pType
n: trunc_index
pTr n A <~>* pTr n A
    reflexivity. }
H: Univalence
k: nat
IHk: forall (A : pType) (n : trunc_index),
pTr n (iterated_loops k A) <~>*
iterated_loops k (pTr (trunc_index_inc' n k) A)
forall (A : pType) (n : trunc_index),
pTr n (iterated_loops k.+1 A) <~>*
iterated_loops k.+1 (pTr (trunc_index_inc' n k.+1) A)
  intros A n.
H: Univalence
k: nat
IHk: forall (A : pType) (n : trunc_index),
pTr n (iterated_loops k A) <~>*
iterated_loops k (pTr (trunc_index_inc' n k) A)
A: pType
n: trunc_index
pTr n (iterated_loops k.+1 A) <~>*
iterated_loops k.+1 (pTr (trunc_index_inc' n k.+1) A)
  cbn; etransitivity.
H: Univalence
k: nat
IHk: forall (A : pType) (n : trunc_index),
pTr n (iterated_loops k A) <~>*
iterated_loops k (pTr (trunc_index_inc' n k) A)
A: pType
n: trunc_index
pTr n
  (loops
     ((fix F (m : nat) : pType :=
         match m with
         | 0%nat => A
         | (m'.+1)%nat => loops (F m')
         end) k)) <~>* ?Goal
H: Univalence
k: nat
IHk: forall (A : pType) (n : trunc_index),
pTr n (iterated_loops k A) <~>*
iterated_loops k (pTr (trunc_index_inc' n k) A)
A: pType
n: trunc_index
?Goal <~>*
loops
  ((fix F (m : nat) : pType :=
      match m with
      | 0%nat => pTr (trunc_index_inc' n.+1 k) A
      | (m'.+1)%nat => loops (F m')
      end) k)
  1: apply ptr_loops.
H: Univalence
k: nat
IHk: forall (A : pType) (n : trunc_index),
pTr n (iterated_loops k A) <~>*
iterated_loops k (pTr (trunc_index_inc' n k) A)
A: pType
n: trunc_index
loops
  (pTr n.+1
     ((fix F (m : nat) : pType :=
         match m with
         | 0%nat => A
         | (m'.+1)%nat => loops (F m')
         end) k)) <~>*
loops
  ((fix F (m : nat) : pType :=
      match m with
      | 0%nat => pTr (trunc_index_inc' n.+1 k) A
      | (m'.+1)%nat => loops (F m')
      end) k)
  rapply (emap loops).
H: Univalence
k: nat
IHk: forall (A : pType) (n : trunc_index),
pTr n (iterated_loops k A) <~>*
iterated_loops k (pTr (trunc_index_inc' n k) A)
A: pType
n: trunc_index
pTr n.+1
  ((fix F (m : nat) : pType :=
      match m with
      | 0%nat => A
      | (m'.+1)%nat => loops (F m')
      end) k) $<~>
(fix F (m : nat) : pType :=
   match m with
   | 0%nat => pTr (trunc_index_inc' n.+1 k) A
   | (m'.+1)%nat => loops (F m')
   end) k
  apply IHk.
Defined.

Definition ptr_loops_eq `{Univalence} (n : trunc_index) (A : pType)
  : pTr n (loops A) = loops (pTr n.+1 A) :> pType
  := path_ptype (ptr_loops n A).

(* This lemma generalizes a goal that appears in [ptr_loops_commutes], allowing us to prove it by path induction. *)
Definition path_Tr_commutes (n : trunc_index) (A : Type) (a0 a1 : A) (p : a0 = a1)
  : path_Tr (n:=n) (tr p) = ap tr p.
n: trunc_index
A: Type
a0, a1: A
p: a0 = a1
path_Tr (tr p) = ap tr p
Proof.
n: trunc_index
A: Type
a0, a1: A
p: a0 = a1
path_Tr (tr p) = ap tr p
  by destruct p.
Defined.

(* [ptr_loops] commutes with the two [ptr] maps. *)
Definition ptr_loops_commutes `{Univalence} (n : trunc_index) (A : pType)
  : (ptr_loops n A) o* ptr ==* fmap loops ptr.
H: Univalence
n: trunc_index
A: pType
ptr_loops n A o* ptr ==* fmap loops ptr
Proof.
H: Univalence
n: trunc_index
A: pType
ptr_loops n A o* ptr ==* fmap loops ptr
  srapply Build_pHomotopy.
H: Univalence
n: trunc_index
A: pType
ptr_loops n A o* ptr == fmap loops ptr
H: Univalence
n: trunc_index
A: pType
?p pt =
dpoint_eq (ptr_loops n A o* ptr) @
(dpoint_eq (fmap loops ptr))^
  -
H: Univalence
n: trunc_index
A: pType
ptr_loops n A o* ptr == fmap loops ptr intro p.
H: Univalence
n: trunc_index
A: pType
p: loops A
(ptr_loops n A o* ptr) p = fmap loops ptr p
    simpl.
H: Univalence
n: trunc_index
A: pType
p: loops A
Descent.path_OO (Tr n.+1) (Tr n) pt pt (tr p) =
1 @ (ap tr p @ 1)
    refine (_ @ _).
H: Univalence
n: trunc_index
A: pType
p: loops A
Descent.path_OO (Tr n.+1) (Tr n) pt pt (tr p) = ?Goal
H: Univalence
n: trunc_index
A: pType
p: loops A
?Goal = 1 @ (ap tr p @ 1)
    +
H: Univalence
n: trunc_index
A: pType
p: loops A
Descent.path_OO (Tr n.+1) (Tr n) pt pt (tr p) = ?Goal apply path_Tr_commutes.
    +
H: Univalence
n: trunc_index
A: pType
p: loops A
ap tr p = 1 @ (ap tr p @ 1) symmetry; refine (_ @ _).
H: Univalence
n: trunc_index
A: pType
p: loops A
1 @ (ap tr p @ 1) = ?Goal
H: Univalence
n: trunc_index
A: pType
p: loops A
?Goal = ap tr p
      *
H: Univalence
n: trunc_index
A: pType
p: loops A
1 @ (ap tr p @ 1) = ?Goal apply concat_1p.
      *
H: Univalence
n: trunc_index
A: pType
p: loops A
ap tr p @ 1 = ap tr p apply concat_p1.
  -
H: Univalence
n: trunc_index
A: pType
((fun p : loops A =>
  path_Tr_commutes n A pt pt p @
  (concat_1p (ap tr p @ 1) @ concat_p1 (ap tr p))^
  :
  (ptr_loops n A o* ptr) p = fmap loops ptr p)
 :
 ptr_loops n A o* ptr == fmap loops ptr) pt =
dpoint_eq (ptr_loops n A o* ptr) @
(dpoint_eq (fmap loops ptr))^ simpl.
H: Univalence
n: trunc_index
A: pType
1 = 1
    reflexivity.
Defined.

(** Pointed truncation preserves binary products. *)
Definition pequiv_ptr_prod (n : trunc_index) (A B : pType)
  : pTr n (A * B) <~>* pTr n A * pTr n B.
n: trunc_index
A, B: pType
pTr n (A * B) <~>* pTr n A * pTr n B
Proof.
n: trunc_index
A, B: pType
pTr n (A * B) <~>* pTr n A * pTr n B
  snrapply Build_pEquiv'.
n: trunc_index
A, B: pType
pTr n (A * B) <~> [pTr n A * pTr n B, ispointed_prod]
n: trunc_index
A, B: pType
?f pt = pt
  1: nrapply equiv_Trunc_prod_cmp.
n: trunc_index
A, B: pType
equiv_Trunc_prod_cmp n pt = pt
  reflexivity.
Defined.

(** ** Truncatedness of [pForall] and [pMap] *)

(** Buchholtz-van Doorn-Rijke, Theorem 4.2:  Let [j >= -1] and [n >= -2].  When [X] is [j]-connected and [Y] is a pointed family of [j+k+1]-truncated types, the type of pointed sections is [n]-truncated.  We formalize it with [j] replaced with a trunc index [m], and so there is a shift compared to the informal statement. This version also allows [n] to be one smaller than BvDR allow. *)
Definition istrunc_pforall `{Univalence} {m n : trunc_index}
  (X : pType@{u}) {iscX : IsConnected m.+1 X}
  (Y : pFam@{u v} X) {istY : forall x, IsTrunc (n +2+ m) (Y x)}
  : IsTrunc@{w} n (pForall X Y).
H: Univalence
m, n: trunc_index
X: pType
iscX: IsConnected (Tr m.+1) X
Y: pFam X
istY: forall x : X, IsTrunc (n +2+ m) (Y x)
IsTrunc n (pForall X Y)
Proof.
H: Univalence
m, n: trunc_index
X: pType
iscX: IsConnected (Tr m.+1) X
Y: pFam X
istY: forall x : X, IsTrunc (n +2+ m) (Y x)
IsTrunc n (pForall X Y)
  nrapply (istrunc_equiv_istrunc _ (equiv_extension_along_pforall@{v w u} Y)).
H: Univalence
m, n: trunc_index
X: pType
iscX: IsConnected (Tr m.+1) X
Y: pFam X
istY: forall x : X, IsTrunc (n +2+ m) (Y x)
IsTrunc n
  (Extensions.ExtensionAlong 
     (unit_name pt) Y (unit_name (dpoint Y)))
  rapply (istrunc_extension_along_conn (n:=m) _ Y (HP:=istY)).
Defined.

(** From this we deduce the non-dependent version, which is Corollary 4.3 of BvDR.  We include [n = -2] here as well, but in this case it is not interesting.  Since [X ->* Y] is inhabited, the [n = -1] case also gives contractibility, with weaker hypotheses. *)
Definition istrunc_pmap `{Univalence} {m n : trunc_index} (X Y : pType)
  `{!IsConnected m.+1 X} `{!IsTrunc (n +2+ m) Y}
  : IsTrunc n (X ->* Y)
  := istrunc_pforall X (pfam_const Y).

(** We can give a different proof of the [n = -1] case (with the conclusion upgraded to contractibility).  This proof works for any reflective subuniverse and avoids univalence.  Is it possible to generalize this to dependent functions while still avoiding univalence and/or keeping [O] a general RSU or modality?  Can [istrunc_pmap] be proven without univalence?  What about [istrunc_pforall]?  If the [n = -2] or [n = -1] cases can be proven without univalence, the rest can be done inductively without univalence. *)
Definition contr_pmap_isconnected_inO `{Funext} (O : ReflectiveSubuniverse)
  (X : pType) `{IsConnected O X} (Y : pType) `{In O Y}
  : Contr (X ->* Y).
H: Funext
O: ReflectiveSubuniverse
X: pType
H0: IsConnected O X
Y: pType
H1: In O Y
Contr (X ->* Y)
Proof.
H: Funext
O: ReflectiveSubuniverse
X: pType
H0: IsConnected O X
Y: pType
H1: In O Y
Contr (X ->* Y)
  srapply (contr_equiv' ([O X, _] ->* Y)).
H: Funext
O: ReflectiveSubuniverse
X: pType
H0: IsConnected O X
Y: pType
H1: In O Y
([O X, ispointed_O X] ->* Y) <~> (X ->* Y)
  rapply pequiv_o_pto_O.
Defined.

(** Every pointed type is (-1)-connected. *)
Global Instance is_minus_one_connected_pointed (X : pType)
  : IsConnected (Tr (-1)) X
  := contr_inhabited_hprop _ (tr pt).