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 (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 (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] *)

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.

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)^
  |}
    snapply 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)
  tapply (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
  snapply 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: napply 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+n+1]-truncated types, the type of pointed sections is [n]-truncated.  We formalize it with [j] replaced with a trunc index [m.+1] to enforce [j >= -1]. 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)
  napply (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 with [Tr (m.+1)] replaced with any reflective subuniverse [O] and doesn't require 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. *)
Instance is_minus_one_connected_pointed (X : pType)
  : IsConnected (Tr (-1)) X
  := contr_inhabited_hprop _ (tr pt).