From dfe1e100bbfe896709373f9626f5b543dac6ac4e Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Fri, 29 Dec 2023 16:13:14 +0000 Subject: [PATCH] 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 * more proof simplications with pelim Signed-off-by: Ali Caglayan * address review comments Signed-off-by: Ali Caglayan * make pelim clearing optional Signed-off-by: Ali Caglayan --------- 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 | 167 +++++++++++++++++++----------- theories/Pointed/Loops.v | 7 +- theories/Pointed/pFiber.v | 2 +- theories/Pointed/pHomotopy.v | 22 ++-- 7 files changed, 137 insertions(+), 91 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..423ac5d43c7 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. +(** 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,10 +285,8 @@ 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) @@ -279,10 +294,8 @@ Definition pmap_prewhisker {A B C : pType} (f : A ->* B) : 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,42 +531,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} @@ -568,41 +564,31 @@ Definition phomotopy_compose_p1 {A : pType} {P : pFam A} {f g : pForall A 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 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. *)