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]>
HoTT · Dec 29, 2023 · af4cc1e · af4cc1e
1 parent 27cf62b
commit af4cc1e
Show file tree

Hide file tree

Showing 7 changed files with 120 additions and 56 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.
 
+(** General tactic to reduce any pointed equations of a pForall *)
+Ltac pelim q :=
+  destruct q as [q ?];
+  unfold pointed_fun, point_htpy in *;    
+  cbn;
+  generalize dependent (q pt);
+  rapply paths_ind_r;
+  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 *)
@@ -525,42 +542,32 @@ 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}
@@ -587,22 +594,20 @@ Proof.
     intros x q. destruct q. reflexivity.
 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.
+  + 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.
+  + by pelim p f g.
 Defined.
 
 Definition equiv_phomotopy_concat_l `{Funext} {A B : pType}
@@ -752,7 +757,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 +770,75 @@ 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 => _.
+
+Global Instance is21cat_ptype : Is21Cat pType.
+Proof.
+  unshelve econstructor.
+  1: exact _.
+  - intros f g h p; nrapply Build_Is1Functor.
+    + intros q r s t u.
+      srapply Build_pHomotopy.
+      1: exact (fun _ => ap _ (u _)).
+      by pelim u s t q r p.
+    + intros q.
+      srapply Build_pHomotopy.
+      1: reflexivity.
+      by pelim q p.
+    + intros a b c s t.
+      srapply Build_pHomotopy.
+      1: cbn; exact (fun _ => ap_pp _ _ _).
+      by pelim s t a b c p.
+  - intros f g h p; nrapply Build_Is1Functor.
+    + intros q r s t u.
+      srapply Build_pHomotopy.
+      1: intro; exact (u _).
+      by pelim p u s t q r.
+    + intros q.
+      srapply Build_pHomotopy.
+      1: reflexivity.
+      by pelim p q.
+    + intros a b c s t.
+      srapply Build_pHomotopy.
+      1: reflexivity.
+      by pelim p s t a b c.
+  - 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

diff --git a/theories/Pointed/pFiber.v b/theories/Pointed/pFiber.v
@@ -84,7 +84,7 @@ Defined.
 Definition pequiv_pfiber {A B C D}
            {f : A ->* B} {g : C ->* D} (h : A <~>* C) (k : B <~>* D)
            (p : k o* f ==* g o* h)
-  : pfiber f <~>* pfiber g
+  : pfiber f $<~> pfiber g
   := Build_pEquiv _ _ (functor_pfiber p) _.
 
 Definition square_functor_pfiber {A B C D}

diff --git a/theories/Pointed/pHomotopy.v b/theories/Pointed/pHomotopy.v
@@ -25,26 +25,16 @@ Defined.
 
 (** ** Whiskering of pointed homotopies by pointed functions *)
 
-Definition pmap_postwhisker {A B C : pType} {f g : A ->* B}
-  (h : B ->* C) (p : f ==* g) : h o* f ==* h o* g.
+Definition pmap_postwhisker {A B C : pType} {f g : A $-> B}
+  (h : B $-> C) (p : f ==* g) : h o* f ==* h o* g.
 Proof.
-  snrapply Build_pHomotopy; cbn.
-  1: intros a; apply ap, p.
-  pointed_reduce.
-  symmetry.
-  simpl.
-  refine (concat_p1 _ @ concat_p1 _ @ ap _ _).
-  exact (concat_p1 _).
+  exact (h $@L p).
 Defined.
 
-Definition pmap_prewhisker {A B C : pType} (f : A ->* B)
-  {g h : B ->* C} (p : g ==* h) : g o* f ==* h o* f.
+Definition pmap_prewhisker {A B C : pType} (f : A $-> B)
+  {g h : B $-> C} (p : g $== h) : g o* f ==* h o* f.
 Proof.
-  snrapply Build_pHomotopy; cbn.
-  1: intros a; apply p.
-  pointed_reduce.
-  symmetry.
-  refine (concat_p1 _ @ concat_1p _ @ concat_p1 _).
+  exact (p $@R f).
 Defined.
 
 (** ** [phomotopy_path] respects 2-cells. *)