From a867baddbfd418296f14ad5e5a1cc7f595470317 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Thu, 28 Dec 2023 17:04:03 +0000 Subject: [PATCH] 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 --- theories/Algebra/AbSES/SixTerm.v | 2 +- theories/Homotopy/ExactSequence.v | 21 +++--- theories/Homotopy/Join/Core.v | 7 +- theories/Pointed/Core.v | 115 +++++++++++++++++++++++------- theories/Pointed/Loops.v | 7 +- theories/Pointed/pFiber.v | 2 +- theories/Pointed/pHomotopy.v | 22 ++---- 7 files changed, 120 insertions(+), 56 deletions(-) diff --git a/theories/Algebra/AbSES/SixTerm.v b/theories/Algebra/AbSES/SixTerm.v index b3e4a87d2c8..99119372494 100644 --- 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 index 18914ccd3ed..d7f423e4f0f 100644 --- 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,7 +264,7 @@ 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'. @@ -267,7 +272,7 @@ 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 index b8808542817..672c43ea241 100644 --- 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 index 81bd9c896a2..7005d59b417 100644 --- 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 index 86b6a1ab72f..b96705ecdaa 100644 --- 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 index c7a551ae043..189ccf533ad 100644 --- 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 index 9983d5ac27c..ff24a875381 100644 --- 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. *)