2-cat of pointed types (#1795)

* 2-cat of pointed types We show the (2,1)-category structure for pointed types. In order to do this easily, we introduce a new tactic called pelim which allows easy path induction on the pointed equation of various pointed structures. This is particularly useful in removing funext from various pType coherences. Signed-off-by: Ali Caglayan <[email protected]> * more proof simplications with pelim Signed-off-by: Ali Caglayan <[email protected]> * address review comments Signed-off-by: Ali Caglayan <[email protected]> * make pelim clearing optional Signed-off-by: Ali Caglayan <[email protected]> --------- Signed-off-by: Ali Caglayan <[email protected]>
HoTT · Dec 29, 2023 · dfe1e10 · dfe1e10
1 parent a7909d0
commit dfe1e10
Show file tree

Hide file tree

Showing 7 changed files with 137 additions and 91 deletions.
diff --git a/theories/Algebra/AbSES/SixTerm.v b/theories/Algebra/AbSES/SixTerm.v
@@ -200,7 +200,7 @@ Local Definition ext_cyclic_exact@{u v w +} `{Univalence}
          o* (pequiv_groupisomorphism (equiv_Z1_hom A))^-1*).
 Proof.
   (* we first move [equiv_Z1_hom] across the total space *)
-  apply moveL_isexact_equiv@{v v v w}.
+  apply moveL_isexact_equiv@{v w}.
   (* now we change the left map so as to apply exactness at iii from above *)
   snrapply (isexact_homotopic_i (Tr (-1))).
   1: exact (fmap10 (A:=Group^op) ab_hom (Z1_mul_nat n) A o*

diff --git a/theories/Homotopy/ExactSequence.v b/theories/Homotopy/ExactSequence.v
@@ -81,14 +81,19 @@ Definition iscomplex_homotopic_f {F X Y : pType}
 
 Definition iscomplex_cancelR {F X Y Y' : pType}
   (i : F ->* X) (f : X ->* Y) (e : Y <~>* Y') (cx : IsComplex i (e o* f))
-  : IsComplex i f
-  := (compose_V_hh e (f o* i))^$ $@ cat_postwhisker _ ((cat_assoc i _ _)^$ $@ cx)
-       $@ precompose_pconst _.
+  : IsComplex i f.
+Proof.
+  refine (_ @* precompose_pconst e^-1*).
+  refine ((compose_V_hh e (f o* i))^$ $@ _).
+  refine (cat_postwhisker e^-1* _).
+  refine ((cat_assoc _ _ _)^$ $@ _).
+  exact cx.
+Defined.
 
 (** And likewise passage across squares with equivalences *)
 Definition iscomplex_equiv_i {F F' X X' Y : pType}
   (i : F ->* X) (i' : F' ->* X')
-  (g : F' <~>* F) (h : X' <~>* X) (p : Square g h i' i)
+  (g : F' $<~> F) (h : X' $<~> X) (p : Square g h i' i)
   (f : X ->* Y)
   (cx: IsComplex i f)
   : IsComplex i' (f o* h).
@@ -212,7 +217,7 @@ Defined.
 (** And also passage across squares with equivalences. *)
 Definition isexact_equiv_i n  {F F' X X' Y : pType}
   (i : F ->* X) (i' : F' ->* X')
-  (g : F' <~>* F) (h : X' <~>* X) (p : Square g h i' i)
+  (g : F' $<~> F) (h : X' $<~> X) (p : Square g h i' i)
   (f : X ->* Y) `{IsExact n F X Y i f}
   : IsExact n i' (f o* h).
 Proof.
@@ -259,15 +264,15 @@ Defined.
 Definition isexact_square_if n  {F F' X X' Y Y' : pType}
   {i : F ->* X} {i' : F' ->* X'}
   {f : X ->* Y} {f' : X' ->* Y'}
-  (g : F' <~>* F) (h : X' <~>* X) (k : Y' <~>* Y)
+  (g : F' $<~> F) (h : X' $<~> X) (k : Y' $<~> Y)
   (p : Square g h i' i) (q : Square h k f' f)
   `{IsExact n F X Y i f}
   : IsExact n i' f'.
 Proof.
   pose (I := isexact_equiv_i n i i' g h p f).
   pose (I2 := isexact_homotopic_f n i' q).
   exists (iscomplex_cancelR i' f' k cx_isexact).
-  epose (e := (pequiv_pfiber (id_cate _) k (cat_idr (k o* f'))^$
+  epose (e := (pequiv_pfiber (id_cate _) k (cat_idr (k $o f'))^$
     : pfiber f' <~>* pfiber (k o* f'))).
   nrefine (cancelR_isequiv_conn_map n _ e).
   1: apply pointed_isequiv.
@@ -358,7 +363,7 @@ Defined.
 
 Definition pequiv_cxfib {F X Y : pType} {i : F ->* X} {f : X ->* Y}
   `{IsExact purely F X Y i f}
-  : F <~>* pfiber f
+  : F $<~> pfiber f
   := Build_pEquiv _ _ (cxfib cx_isexact) _.
 
 Definition fiberseq_isexact_purely {F X Y : pType} (i : F ->* X) (f : X ->* Y)

diff --git a/theories/Homotopy/Join/Core.v b/theories/Homotopy/Join/Core.v
@@ -327,9 +327,10 @@ Definition joinrecdata_0gpd_fun (A B : Type) : Fun11 Type ZeroGpd
 (** By the Yoneda lemma, it follows from [JoinRecData] being a 1-functor that given [JoinRecData] in [J], we get a map [(J -> P) $-> (JoinRecData A B P)] of 0-groupoids which is natural in [P]. Below we will specialize to the case where [J] is [Join A B] with the canonical [JoinRecData]. *)
 Definition join_nattrans_recdata {A B J : Type} (f : JoinRecData A B J)
   : NatTrans (opyon_0gpd J) (joinrecdata_0gpd_fun A B).
-Proof.
-  srapply Build_NatTrans.  (* This finds the Yoneda lemma via typeclass search. Is that what we want? *)
-  Unshelve.
+Proof. 
+  snrapply Build_NatTrans.
+  1: rapply opyoneda_0gpd.
+  2: exact _.
   exact f.
 Defined.
 

diff --git a/theories/Pointed/Core.v b/theories/Pointed/Core.v
@@ -186,6 +186,23 @@ Ltac pointed_reduce_pmap f
     | _ ->* ?Y => let p := fresh in destruct Y as [Y ?], f as [f p]; cbn in *; destruct p; cbn
     end.
 
+(** A general tactic to replace pointedness paths in a pForall with reflexivity.  It clears the function, so can only be applied once the function itself is not longer needed. *)
+Ltac pelim q :=
+  destruct q as [q ?];
+  unfold pointed_fun, point_htpy in *;
+  cbn;
+  generalize dependent (q pt);
+  nrapply paths_ind_r;
+  try clear q.
+
+Tactic Notation "pelim" constr(x0) := pelim x0.
+Tactic Notation "pelim" constr(x0) constr(x1) := pelim x0; pelim x1.
+Tactic Notation "pelim" constr(x0) constr(x1) constr(x2) := pelim x0; pelim x1 x2.
+Tactic Notation "pelim" constr(x0) constr(x1) constr(x2) constr(x3) := pelim x0; pelim x1 x2 x3.
+Tactic Notation "pelim" constr(x0) constr(x1) constr(x2) constr(x3) constr(x4) := pelim x0; pelim x1 x2 x3 x4.
+Tactic Notation "pelim" constr(x0) constr(x1) constr(x2) constr(x3) constr(x4) constr(x5) := pelim x0; pelim x1 x2 x3 x4 x5.
+Tactic Notation "pelim" constr(x0) constr(x1) constr(x2) constr(x3) constr(x4) constr(x5) constr(x6) := pelim x0; pelim x1 x2 x3 x4 x5 x6.
+
 (** ** Equivalences to sigma-types. *)
 
 (** pType *)
@@ -244,8 +261,8 @@ Global Instance phomotopy_symmetric {A B} : Symmetric (@pHomotopy A B).
 Proof.
   intros f g p.
   snrefine (Build_pHomotopy _ _); cbn.
-  - intros x; exact ((p x)^).
-  - refine (inverse2 (dpoint_eq p) @ inv_pV _ _).
+  1: intros x; exact ((p x)^).
+  by pelim p f g.
 Defined.
 
 Notation "p ^*" := (phomotopy_symmetric _ _ p) : pointed_scope.
@@ -268,21 +285,17 @@ Definition pmap_postwhisker {A B C : pType} {f g : A ->* B}
   : h o* f ==* h o* g.
 Proof.
   snrefine (Build_pHomotopy _ _); cbn.
-  - exact (fun x => ap h (p x)).
-  - nrefine (ap _ (dpoint_eq p) @ ap_pp _ _ _ @ whiskerL _ (ap_V _ _) @ _^).
-    nrefine (whiskerL _ (inv_pp _ _) @ concat_pp_p _ _ _ @ _).
-    exact (whiskerL _ (concat_p_Vp _ _)).
+  1: exact (fun x => ap h (p x)).
+  by pelim p f g h.
 Defined.
 
 Definition pmap_prewhisker {A B C : pType} (f : A ->* B)
   {g h : B ->* C} (p : g ==* h)
   : g o* f ==* h o* f.
 Proof.
   snrefine (Build_pHomotopy _ _); cbn.
-  - exact (fun x => p (f x)).
-  - apply moveL_pV.
-    nrefine (concat_p_pp _ _ _ @ whiskerR (concat_Ap p (point_eq f))^ _ @ _).
-    exact (concat_pp_p _ _ _ @ whiskerL _ (point_htpy p)).
+  1: exact (fun x => p (f x)).
+  by pelim f p g h.
 Defined.
 
 (** ** 1-categorical properties of [pType]. *)
@@ -294,10 +307,7 @@ Definition pmap_compose_assoc {A B C D : pType} (h : C ->* D)
 Proof.
   snrapply Build_pHomotopy.
   1: reflexivity.
-  pointed_reduce_pmap f.
-  pointed_reduce_pmap g.
-  pointed_reduce_pmap h.
-  reflexivity.
+  by pelim f g h.
 Defined.
 
 (** precomposition of identity pointed map *)
@@ -306,8 +316,7 @@ Definition pmap_precompose_idmap {A B : pType} (f : A ->* B)
 Proof.
   snrapply Build_pHomotopy.
   1: reflexivity.
-  symmetry.
-  apply concat_pp_V.
+  by pelim f.
 Defined.
 
 (** postcomposition of identity pointed map *)
@@ -316,10 +325,7 @@ Definition pmap_postcompose_idmap {A B : pType} (f : A ->* B)
 Proof.
   snrapply Build_pHomotopy.
   1: reflexivity.
-  symmetry.
-  apply moveR_pV.
-  simpl.
-  apply equiv_p1_1q, ap_idmap.
+  by pelim f.
 Defined.
 
 (** ** Funext for pointed types and direct consequences. *)
@@ -434,10 +440,10 @@ Defined.
 
 (* A pointed equivalence is a section of its inverse *)
 Definition peissect {A B : pType} (f : A <~>* B)
-  : (pequiv_inverse f) o* f ==* pmap_idmap. 
+  : (pequiv_inverse f) o* f ==* pmap_idmap.
 Proof.
   srefine (Build_pHomotopy _ _).
-  1: apply (eissect f). 
+  1: apply (eissect f).
   simpl. unfold moveR_equiv_V.
   pointed_reduce.
   symmetry.
@@ -525,84 +531,64 @@ Notation "'ppforall'  x .. y , P"
      : pointed_scope.
 
 (** ** 1-categorical properties of [pForall]. *)
-(** TODO: remove funext *)
 
-Definition phomotopy_postwhisker `{Funext} {A : pType} {P : pFam A}
+Definition phomotopy_postwhisker {A : pType} {P : pFam A}
   {f g h : pForall A P} {p p' : f ==* g} (r : p ==* p') (q : g ==* h)
   : p @* q ==* p' @* q.
 Proof.
   snrapply Build_pHomotopy.
   1: exact (fun x => whiskerR (r x) (q x)).
-  revert p' r. srapply phomotopy_ind.
-  revert h q. srapply phomotopy_ind.
-  revert g p. srapply phomotopy_ind.
-  pointed_reduce. reflexivity.
+  by pelim q r p p' f g h.
 Defined.
 
-Definition phomotopy_prewhisker `{Funext} {A : pType} {P : pFam A}
+Definition phomotopy_prewhisker {A : pType} {P : pFam A}
   {f g h : pForall A P} (p : f ==* g) {q q' : g ==* h} (s : q ==* q')
   : p @* q ==* p @* q'.
 Proof.
   snrapply Build_pHomotopy.
   1: exact (fun x => whiskerL (p x) (s x)).
-  revert q' s. srapply phomotopy_ind.
-  revert h q. srapply phomotopy_ind.
-  revert g p. srapply phomotopy_ind.
-  pointed_reduce. reflexivity.
+  by pelim s q q' p f g h.
 Defined.
 
-Definition phomotopy_compose_assoc `{Funext} {A : pType} {P : pFam A}
+Definition phomotopy_compose_assoc {A : pType} {P : pFam A}
   {f g h k : pForall A P} (p : f ==* g) (q : g ==* h) (r : h ==* k)
   : p @* (q @* r) ==* (p @* q) @* r.
 Proof.
   snrapply Build_pHomotopy.
   1: exact (fun x => concat_p_pp (p x) (q x) (r x)).
-  revert k r. srapply phomotopy_ind.
-  revert h q. srapply phomotopy_ind.
-  revert g p. srapply phomotopy_ind.
-  pointed_reduce. reflexivity.
+  by pelim r q p f g h k.
 Defined.
 
 Definition phomotopy_compose_p1 {A : pType} {P : pFam A} {f g : pForall A P}
  (p : f ==* g) : p @* reflexivity g ==* p.
 Proof.
   srapply Build_pHomotopy.
   1: intro; apply concat_p1.
-  pointed_reduce.
-  rewrite (concat_pp_V H (concat_p1 _))^. generalize (H @ concat_p1 _).
-  clear H. intros H. destruct H.
-  generalize (p point); generalize (g point).
-  intros x q. destruct q. reflexivity.
+  by pelim p f g.
 Defined.
 
 Definition phomotopy_compose_1p {A : pType} {P : pFam A} {f g : pForall A P}
  (p : f ==* g) : reflexivity f @* p ==* p.
 Proof.
   srapply Build_pHomotopy.
-  + intro x. apply concat_1p.
-  + pointed_reduce.
-    rewrite (concat_pp_V H (concat_p1 _))^. generalize (H @ concat_p1 _).
-    clear H. intros H. destruct H.
-    generalize (p point). generalize (g point).
-    intros x q. destruct q. reflexivity.
+  1: intro x; apply concat_1p.
+  by pelim p f g.
 Defined.
 
-Definition phomotopy_compose_pV `{Funext} {A : pType} {P : pFam A} {f g : pForall A P}
+Definition phomotopy_compose_pV {A : pType} {P : pFam A} {f g : pForall A P}
  (p : f ==* g) : p @* p ^* ==* phomotopy_reflexive f.
 Proof.
   srapply Build_pHomotopy.
-  + intro x. apply concat_pV.
-  + revert g p. srapply phomotopy_ind.
-    pointed_reduce. reflexivity.
+  1: intro x; apply concat_pV.
+  by pelim p f g.
 Defined.
 
-Definition phomotopy_compose_Vp `{Funext} {A : pType} {P : pFam A} {f g : pForall A P}
+Definition phomotopy_compose_Vp {A : pType} {P : pFam A} {f g : pForall A P}
  (p : f ==* g) : p ^* @* p ==* phomotopy_reflexive g.
 Proof.
   srapply Build_pHomotopy.
-  + intro x. apply concat_Vp.
-  + revert g p. srapply phomotopy_ind.
-    pointed_reduce. reflexivity.
+  1: intro x; apply concat_Vp.
+  by pelim p f g.
 Defined.
 
 Definition equiv_phomotopy_concat_l `{Funext} {A B : pType}
@@ -752,7 +738,7 @@ Definition path_zero_morphism_pconst (A B : pType)
   : (@pconst A B) = zero_morphism := idpath.
 
 (** pForall is a 1-category *)
-Global Instance is1cat_pforall `{Funext} (A : pType) (P : pFam A) : Is1Cat (pForall A P).
+Global Instance is1cat_pforall (A : pType) (P : pFam A) : Is1Cat (pForall A P) | 10.
 Proof.
   econstructor.
   - intros f g h p; rapply Build_Is0Functor.
@@ -765,13 +751,76 @@ Proof.
 Defined.
 
 (** pForall is a 1-groupoid *)
-Global Instance is1gpd_pforall `{Funext} (A : pType) (P : pFam A) : Is1Gpd (pForall A P).
+Global Instance is1gpd_pforall (A : pType) (P : pFam A) : Is1Gpd (pForall A P) | 10.
 Proof.
   econstructor.
   + intros ? ? p. exact (phomotopy_compose_pV p).
   + intros ? ? p. exact (phomotopy_compose_Vp p).
 Defined.
 
+Global Instance is3graph_ptype : Is3Graph pType
+  := fun f g => is2graph_pforall _ _.
+
+Global Instance is21cat_ptype : Is21Cat pType.
+Proof.
+  unshelve econstructor.
+  - exact _.
+  - intros A B C f; nrapply Build_Is1Functor.
+    + intros g h p q r.
+      srapply Build_pHomotopy.
+      1: exact (fun _ => ap _ (r _)).
+      by pelim r p q g h f.
+    + intros g.
+      srapply Build_pHomotopy.
+      1: reflexivity.
+      by pelim g f.
+    + intros g h i p q.
+      srapply Build_pHomotopy.
+      1: cbn; exact (fun _ => ap_pp _ _ _).
+      by pelim p q g h i f.
+  - intros A B C f; nrapply Build_Is1Functor.
+    + intros g h p q r.
+      srapply Build_pHomotopy.
+      1: intro; exact (r _).
+      by pelim f r p q g h.
+    + intros g.
+      srapply Build_pHomotopy.
+      1: reflexivity.
+      by pelim f g.
+    + intros g h i p q.
+      srapply Build_pHomotopy.
+      1: reflexivity.
+      by pelim f p q i g h.
+  - intros A B C D f g r1 r2 s1.
+    srapply Build_pHomotopy.
+    1: exact (fun _ => concat_p1 _ @ (concat_1p _)^).
+    by pelim f g s1 r1 r2.
+  - intros A B C D f g r1 r2 s1.
+    srapply Build_pHomotopy.
+    1: exact (fun _ => concat_p1 _ @ (concat_1p _)^).
+    by pelim f s1 r1 r2 g.
+  - intros A B C D f g r1 r2 s1.
+    srapply Build_pHomotopy.
+    1: cbn; exact (fun _ => concat_p1 _ @ ap_compose _ _ _ @ (concat_1p _)^).
+    by pelim s1 r1 r2 f g.
+  - intros A B r1 r2 s1.
+    srapply Build_pHomotopy.
+    1: exact (fun _ => concat_p1 _ @ ap_idmap _ @ (concat_1p _)^).
+    by pelim s1 r1 r2.
+  - intros A B r1 r2 s1.
+    srapply Build_pHomotopy.
+    1: exact (fun _ => concat_p1 _ @ (concat_1p _)^).
+    simpl; by pelim s1 r1 r2.
+  - intros A B C D E f g h j.
+    srapply Build_pHomotopy.
+    1: reflexivity.
+    by pelim f g h j.
+  - intros A B C f g.
+    srapply Build_pHomotopy.
+    1: reflexivity.
+    by pelim f g.
+Defined.
+
 (** The forgetful map from pType to Type is a 0-functor *)
 Global Instance is0functor_pointed_type : Is0Functor pointed_type.
 Proof.

diff --git a/theories/Pointed/Loops.v b/theories/Pointed/Loops.v
@@ -99,8 +99,9 @@ Defined.
 (** Loops is a pointed functor *)
 Global Instance ispointedfunctor_loops : IsPointedFunctor loops.
 Proof.
-  rapply Build_IsPointedFunctor'.
-  apply pequiv_loops_punit.
+  snrapply Build_IsPointedFunctor'.
+  1-4: exact _.
+  exact pequiv_loops_punit.
 Defined.
 
 Lemma fmap_loops_pconst {A B : pType} : fmap loops (@pconst A B) ==* pconst.
@@ -122,7 +123,7 @@ Global Instance is1functor_iterated_loops n : Is1Functor (iterated_loops n).
 Proof.
   induction n.
   1: exact _.
-  rapply is1functor_compose.
+  nrapply is1functor_compose; exact _.
 Defined.
 
 Lemma fmap_iterated_loops_pp {X Y : pType} (f : X ->* Y) n