diff --git a/theories/Algebra/AbSES/SixTerm.v b/theories/Algebra/AbSES/SixTerm.v index 856e3f0a52e..818f00e6750 100644 --- a/theories/Algebra/AbSES/SixTerm.v +++ b/theories/Algebra/AbSES/SixTerm.v @@ -191,16 +191,15 @@ Local Definition isexact_ext_cyclic_ab_iii@{u v w | u < v, v < w} `{Univalence} (abses_from_inclusion (Z1_mul_nat n)). (** We show exactness of [A -> A -> Ext Z/n A] where the first map is multiplication by [n], but considered in universe [v]. *) -(* The [+] is needed in the list of universes, but in the end there are no others. *) -Local Definition ext_cyclic_exact@{u v w +} `{Univalence} +Local Definition ext_cyclic_exact@{u v w} `{Univalence} (n : nat) `{IsEmbedding (Z1_mul_nat n)} {A : AbGroup@{u}} - : IsExact@{v v v v v v} (Tr (-1)) + : IsExact@{v v v v v} (Tr (-1)) (ab_mul_nat (A:=A) n) - (abses_pushout_ext (abses_from_inclusion (Z1_mul_nat n)) + (abses_pushout_ext@{u w v} (abses_from_inclusion (Z1_mul_nat n)) o* (pequiv_groupisomorphism (equiv_Z1_hom A))^-1*). Proof. (* we first move [equiv_Z1_hom] across the total space *) - apply moveL_isexact_equiv@{v w}. + apply moveL_isexact_equiv. (* 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/Algebra/Groups/ShortExactSequence.v b/theories/Algebra/Groups/ShortExactSequence.v index 3dc413717fb..0a77c3088ca 100644 --- a/theories/Algebra/Groups/ShortExactSequence.v +++ b/theories/Algebra/Groups/ShortExactSequence.v @@ -38,9 +38,6 @@ Proof. exact (grp_homo_unit f). Defined. -Local Existing Instance ishprop_phomotopy_hset. -Local Existing Instance ishprop_isexact_hset. - (** A complex 0 -> A -> B of groups is purely exact if and only if the map A -> B is an embedding. *) Lemma iff_grp_isexact_isembedding `{Funext} {A B : Group} (f : A $-> B) : IsExact purely (@grp_homo_const grp_trivial A) f <-> IsEmbedding f. diff --git a/theories/Homotopy/ExactSequence.v b/theories/Homotopy/ExactSequence.v index f39f0032148..6c60c8c14e9 100644 --- a/theories/Homotopy/ExactSequence.v +++ b/theories/Homotopy/ExactSequence.v @@ -93,7 +93,7 @@ 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 : h o* i' ==* i o* g) (f : X ->* Y) (cx: IsComplex i f) : IsComplex i' (f o* h). @@ -127,14 +127,11 @@ Proof. exact (concat_p1 _ @ concat_1p _). Defined. -Local Existing Instance ishprop_phomotopy_hset. - (** If Y is a set, then IsComplex is an HProp. *) Global Instance ishprop_iscomplex_hset `{Univalence} {F X Y : pType} `{IsHSet Y} (i : F ->* X) (f : X ->* Y) : IsHProp (IsComplex i f) := {}. - (** ** Very short exact sequences and fiber sequences *) (** A complex is [n]-exact if the induced map [cxfib] is [n]-connected. *) @@ -182,9 +179,9 @@ Defined. (** If the base is contractible, then [i] is [O]-connected. *) Definition isconnmap_O_isexact_base_contr (O : Modality@{u}) {F X Y : pType} `{Contr Y} (i : F ->* X) (f : X ->* Y) - `{IsExact@{_ _ _ u u u} O _ _ _ i f} + `{IsExact@{_ _ u u u} O _ _ _ i f} : IsConnMap O i - := conn_map_compose@{u _ u _} O (cxfib@{u u _ _ _} cx_isexact) pr1. + := conn_map_compose@{u _ u _} O (cxfib@{u u _ _} cx_isexact) pr1. (** Passage across homotopies preserves exactness. *) Definition isexact_homotopic_i n {F X Y : pType} @@ -217,7 +214,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 : h o* i' ==* i o* g) (f : X ->* Y) `{IsExact n F X Y i f} : IsExact n i' (f o* h). Proof. @@ -264,15 +261,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) - (p : Square g h i' i) (q : Square h k f' f) + (g : F' <~>* F) (h : X' <~>* X) (k : Y' <~>* Y) + (p : h o* i' ==* i o* g) (q : k o* f' ==* f o* h) `{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_cancelL i' f' k cx_isexact). - epose (e := (pequiv_pfiber (id_cate _) k (cat_idr (k $o f'))^$ + epose (e := (pequiv_pfiber pequiv_pmap_idmap k (pmap_precompose_idmap (k o* f'))^* : pfiber f' <~>* pfiber (k o* f'))). nrefine (cancelL_isequiv_conn_map n _ e). 1: apply pointed_isequiv. @@ -363,7 +360,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) @@ -442,7 +439,7 @@ Defined. (** It's useful to see [pfib_cxfib] as a degenerate square. *) Definition square_pfib_pequiv_cxfib {F X Y : pType} (i : F ->* X) (f : X ->* Y) `{IsExact purely F X Y i f} - : Square (pequiv_cxfib) (pequiv_pmap_idmap) i (pfib f). + : pequiv_pmap_idmap o* i ==* pfib f o* pequiv_cxfib. Proof. unfold Square. refine (pmap_postcompose_idmap _ @* _). diff --git a/theories/Pointed.v b/theories/Pointed.v index 8a8c3c8d2f2..53f7e65cbd2 100644 --- a/theories/Pointed.v +++ b/theories/Pointed.v @@ -5,6 +5,5 @@ Require Export Pointed.pFiber. Require Export Pointed.pEquiv. Require Export Pointed.pTrunc. Require Export Pointed.pModality. -Require Export Pointed.pHomotopy. Require Export Pointed.pSusp. Require Export Pointed.pSect. diff --git a/theories/Pointed/Core.v b/theories/Pointed/Core.v index e3cd2fc263b..bbb5fb1fdff 100644 --- a/theories/Pointed/Core.v +++ b/theories/Pointed/Core.v @@ -2,6 +2,8 @@ Require Import Basics Types. Require Import PathAny. Require Import WildCat. +Require Import Truncations.Core. +Require Import ReflectiveSubuniverse. Local Set Polymorphic Inductive Cumulativity. @@ -60,7 +62,6 @@ Arguments dpoint_eq {A P} f : rename. Arguments pointed_fun {A P} f : rename. Coercion pointed_fun : pForall >-> Funclass. - (** ** Pointed functions *) (** A pointed map is a map with a proof that it preserves the point. We define it as as a notation for a non-dependent version of [pForall]. *) @@ -86,20 +87,20 @@ Definition pmap_compose {A B C : pType} (g : B ->* C) (f : A ->* B) Infix "o*" := pmap_compose : pointed_scope. +(** The projections from a pointed product are pointed maps. *) Definition pfst {A B : pType} : A * B ->* A := Build_pMap (A * B) A fst idpath. Definition psnd {A B : pType} : A * B ->* B := Build_pMap (A * B) B snd idpath. - (** ** Pointed homotopies *) +(** A pointed homotopy is a homotopy with a proof that the presevation paths agree. We define it instead as a special case of a [pForall]. This means that we can define pointed homotopies between pointed homotopies. *) Definition pfam_phomotopy {A : pType} {P : pFam A} (f g : pForall A P) : pFam A := Build_pFam (fun x => f x = g x) (dpoint_eq f @ (dpoint_eq g)^). -(* A pointed homotopy is a homotopy with a proof that the presevation paths agree. We define it instead as a special case of a [pForall]. This means that we can define pointed homotopies between pointed homotopies. *) -Definition pHomotopy {A : pType} {P : pFam A} (f g : pForall A P) : Type +Definition pHomotopy {A : pType} {P : pFam A} (f g : pForall A P) := pForall A (pfam_phomotopy f g). Infix "==*" := pHomotopy : pointed_scope. @@ -124,26 +125,24 @@ Defined. (** ** Pointed equivalences *) -(* A pointed equivalence is a pointed map and a proof that it is - an equivalence *) +(** A pointed equivalence is a pointed map and a proof that it is an equivalence *) Record pEquiv (A B : pType) := { pointed_equiv_fun : pForall A (pfam_const B) ; pointed_isequiv : IsEquiv pointed_equiv_fun ; }. -(* TODO: It might be better behaved to define pEquiv as an equivalence and a proof that this equivalence is pointed. In pEquiv.v we have another constructor Build_pEquiv' which coq can infer faster than Build_pEquiv. *) +(** TODO: It might be better behaved to define pEquiv as an equivalence and a proof that this equivalence is pointed. In pEquiv.v we have another constructor Build_pEquiv' which coq can infer faster than Build_pEquiv. *) Infix "<~>*" := pEquiv : pointed_scope. -(* Note: because we define pMap as a special case of pForall, we must declare - all coercions into pForall, *not* into pMap. *) +(** Note: because we define pMap as a special case of pForall, we must declare all coercions into pForall, *not* into pMap. *) Coercion pointed_equiv_fun : pEquiv >-> pForall. Global Existing Instance pointed_isequiv. Coercion pointed_equiv_equiv {A B} (f : A <~>* B) : A <~> B := Build_Equiv A B f _. -(* The pointed identity is a pointed equivalence *) +(** The pointed identity is a pointed equivalence *) Definition pequiv_pmap_idmap {A} : A <~>* A := Build_pEquiv _ _ pmap_idmap _. @@ -151,7 +150,7 @@ Definition pequiv_pmap_idmap {A} : A <~>* A Definition psigma {A : pType} (P : pFam A) : pType := [sig P, (point A; dpoint P)]. -(** Pointed pi types, note that the domain is not pointed *) +(** Pointed pi types; note that the domain is not pointed *) Definition pproduct {A : Type} (F : A -> pType) : pType := [forall (a : A), pointed_type (F a), ispointed_type o F]. @@ -254,32 +253,45 @@ Defined. (** ** Various operations with pointed homotopies *) +(** For the following three instances, the typeclass (e.g. [Reflexive]) requires a third universe variable, the maximum of the universe of [A] and the universe of the values of [P]. Because of this, in each case we first prove a version not mentioning the typeclass, which avoids a stray universe variable. *) + (** [pHomotopy] is a reflexive relation *) -Global Instance phomotopy_reflexive {A : pType} {P : pFam A} +Definition phomotopy_reflexive {A : pType} {P : pFam A} (f : pForall A P) + : f ==* f + := Build_pHomotopy (fun x => 1) (concat_pV _)^. + +Global Instance phomotopy_reflexive' {A : pType} {P : pFam A} : Reflexive (@pHomotopy A P) - := fun X => Build_pHomotopy (fun x => 1) (concat_pV _)^. + := @phomotopy_reflexive A P. (** [pHomotopy] is a symmetric relation *) -Global Instance phomotopy_symmetric {A B} : Symmetric (@pHomotopy A B). +Definition phomotopy_symmetric {A P} {f g : pForall A P} (p : f ==* g) + : g ==* f. Proof. - intros f g p. snrefine (Build_pHomotopy _ _); cbn. 1: intros x; exact ((p x)^). by pelim p f g. Defined. -Notation "p ^*" := (phomotopy_symmetric _ _ p) : pointed_scope. +Global Instance phomotopy_symmetric' {A P} + : Symmetric (@pHomotopy A P) + := @phomotopy_symmetric A P. + +Notation "p ^*" := (phomotopy_symmetric p) : pointed_scope. (** [pHomotopy] is a transitive relation *) -Global Instance phomotopy_transitive {A B} : Transitive (@pHomotopy A B). +Definition phomotopy_transitive {A P} {f g h : pForall A P} (p : f ==* g) (q : g ==* h) + : f ==* h. Proof. - intros x y z p q. snrefine (Build_pHomotopy (fun x => p x @ q x) _). nrefine (dpoint_eq p @@ dpoint_eq q @ concat_pp_p _ _ _ @ _). nrapply whiskerL; nrapply concat_V_pp. Defined. -Notation "p @* q" := (phomotopy_transitive _ _ _ p q) : pointed_scope. +Global Instance phomotopy_transitive' {A P} : Transitive (@pHomotopy A P) + := @phomotopy_transitive A P. + +Notation "p @* q" := (phomotopy_transitive p q) : pointed_scope. (** ** Whiskering of pointed homotopies by pointed functions *) @@ -331,208 +343,6 @@ Proof. by pelim f. Defined. -(** ** Funext for pointed types and direct consequences. *) - -(** By funext pointed homotopies are equivalent to paths *) -Definition equiv_path_pforall `{Funext} {A : pType} - {P : pFam A} (f g : pForall A P) - : (f ==* g) <~> (f = g). -Proof. - refine (_ oE (issig_phomotopy f g)^-1). - revert f g; apply (equiv_path_issig_contr (issig_pforall A P)). - { intros [f feq]; cbn. - exists (fun a => 1%path). - exact (concat_pV _)^. } - intros [f feq]; cbn. - contr_sigsig f (fun a:A => idpath (f a)); cbn. - refine (contr_equiv' {feq' : f (point A) = dpoint P & feq = feq'} _). - refine (equiv_functor_sigma' (equiv_idmap _) _); intros p. - refine (_^-1 oE equiv_path_inverse _ _). - apply equiv_moveR_1M. -Defined. - -Definition path_pforall `{Funext} {A : pType} {P : pFam A} {f g : pForall A P} - : (f ==* g) -> (f = g) := equiv_path_pforall f g. - -(** Here is the inverse map without assuming funext *) -Definition phomotopy_path {A : pType} {P : pFam A} {f g : pForall A P} - : (f = g) -> (f ==* g) := ltac:(by intros []). - -(** And we prove that it agrees with the inverse of [equiv_path_pforall] *) -Definition path_equiv_path_pforall_phomotopy_path `{Funext} {A : pType} - {P : pFam A} {f g : pForall A P} - : phomotopy_path (f:=f) (g:=g) = (equiv_path_pforall f g)^-1%equiv - := ltac:(by funext []). - -(* We note that the inverse of [path_pmap] computes definitionally on reflexivity, and hence [path_pmap] itself computes typally so. *) -Definition equiv_inverse_path_pforall_1 `{Funext} {A : pType} {P : pFam A} (f : pForall A P) - : (equiv_path_pforall f f)^-1%equiv 1%path = reflexivity f - := 1. - -Definition path_pforall_1 `{Funext} {A : pType} {P : pFam A} {f : pForall A P} - : equiv_path_pforall _ _ (reflexivity f) = 1%path - := moveR_equiv_M _ _ (equiv_inverse_path_pforall_1 f)^. - -Definition equiv_path_pmap_1 `{Funext} {A B} {f : A ->* B} - : path_pforall (reflexivity f) = 1%path - := path_pforall_1. - -(** Since pointed homotopies are equivalent to equalities, we can act as if - they are paths and define a path induction for them *) -Definition phomotopy_ind `{H0 : Funext} {A : pType} {P : pFam A} - {k : pForall A P} (Q : forall (k' : pForall A P), (k ==* k') -> Type) - (q : Q k (reflexivity k)) (k' : pForall A P) - : forall (H : k ==* k'), Q k' H. -Proof. - equiv_intro (equiv_path_pforall k k')^-1%equiv p. - induction p. - exact q. -Defined. - -(** Sometimes you have a goal with both a pointed homotopy [H] and [path_pforall H]. - This is an induction principle that allows us to replace both of them by reflexivity - at the same time. *) -Definition phomotopy_ind' `{H0 : Funext} {A : pType} {P : pFam A} - {k : pForall A P} (Q : forall (k' : pForall A P), (k ==* k') -> (k = k') -> Type) - (q : Q k (reflexivity k) 1 % path) (k' : pForall A P) (H : k ==* k') - (p : k = k') (r : path_pforall H = p) - : Q k' H p. -Proof. - induction r. - revert k' H. - rapply phomotopy_ind. - exact (transport (Q _ (reflexivity _)) path_pforall_1^ q). -Defined. - -Definition phomotopy_ind_1 `{H0 : Funext} {A : pType} {P : pFam A} - {k : pForall A P} (Q : forall (k' : pForall A P), (k ==* k') -> Type) - (q : Q k (reflexivity k)) : - phomotopy_ind Q q k (reflexivity k) = q. -Proof. - change (reflexivity k) with ((equiv_path_pforall k k)^-1%equiv (idpath k)). - apply equiv_ind_comp. -Defined. - -Definition phomotopy_ind_1' `{H0 : Funext} {A : pType} {P : pFam A} - {k : pForall A P} (Q : forall (k' : pForall A P), (k ==* k') -> (k = k') -> Type) - (q : Q k (reflexivity k) 1 % path) - : phomotopy_ind' Q q k (reflexivity k) (path_pforall (reflexivity k)) (1 % path) - = transport (Q k (reflexivity k)) path_pforall_1^ q. -Proof. - srapply phomotopy_ind_1. -Defined. - -(** Every homotopy between pointed maps of sets is a pointed homotopy. *) -Definition phomotopy_homotopy_hset {X Y : pType} `{IsHSet Y} {f g : X ->* Y} (h : f == g) - : f ==* g. -Proof. - apply (Build_pHomotopy h). - apply path_ishprop. -Defined. - -(** ** Operations on equivalences needed to make pType a wild category with equivalences *) - -(** The inverse equivalence of a pointed equivalence is again a pointed equivalence *) -Definition pequiv_inverse {A B} (f : A <~>* B) : B <~>* A. -Proof. - snrapply Build_pEquiv. - 1: apply (Build_pMap _ _ f^-1). - 1: apply moveR_equiv_V; symmetry; apply point_eq. - exact _. -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. -Proof. - srefine (Build_pHomotopy _ _). - 1: apply (eissect f). - simpl. unfold moveR_equiv_V. - pointed_reduce. - symmetry. - refine (concat_p1 _ @ concat_1p _ @ concat_1p _). -Defined. - -(* A pointed equivalence is a retraction of its inverse *) -Definition peisretr {A B : pType} (f : A <~>* B) - : f o* (pequiv_inverse f) ==* pmap_idmap. -Proof. - srefine (Build_pHomotopy _ _). - 1: apply (eisretr f). - pointed_reduce. - unfold moveR_equiv_V. - refine (eisadj f _ @ _). - symmetry. - exact (concat_p1 _ @ concat_p1 _ @ ap _ (concat_1p _)). -Defined. - -(** Univalence for pointed types *) -Definition equiv_path_ptype `{Univalence} (A B : pType) : A <~>* B <~> A = B. -Proof. - refine (equiv_path_from_contr A (fun C => A <~>* C) pequiv_pmap_idmap _ B). - nrapply (contr_equiv' { X : Type & { f : A <~> X & {x : X & f pt = x} }}). - 1: make_equiv. - rapply (contr_equiv' { X : Type & A <~> X }). - nrapply equiv_functor_sigma_id; intro X; symmetry. - rapply equiv_sigma_contr. - (** If you replace the type in the second line with { Xf : {X : Type & A <~> X} & {x : Xf.1 & Xf.2 pt = x} }, then the third line completes the proof, but that results in an extra universe variable. *) -Defined. - -Definition path_ptype `{Univalence} {A B : pType} : (A <~>* B) -> A = B - := equiv_path_ptype A B. - -(** The inverse map can be defined without Univalence. *) -Definition pequiv_path {A B : pType} (p : A = B) : (A <~>* B) - := match p with idpath => pequiv_pmap_idmap end. - -(** This just confirms that it is definitionally the inverse map. *) -Definition pequiv_path_equiv_path_ptype_inverse `{Univalence} {A B : pType} - : @pequiv_path A B = (equiv_path_ptype A B)^-1 - := idpath. - -Global Instance isequiv_pequiv_path `{Univalence} {A B : pType} - : IsEquiv (@pequiv_path A B) - := isequiv_inverse (equiv_path_ptype A B). - -(** Two pointed equivalences are equal if their underlying pointed functions are equal. This requires [Funext] for knowing that [IsEquiv] is an HProp. *) -Definition equiv_path_pequiv' `{Funext} {A B : pType} (f g : A <~>* B) - : (f = g :> (A ->* B)) <~> (f = g :> (A <~>* B)). -Proof. - refine ((equiv_ap' (issig_pequiv A B)^-1%equiv f g)^-1%equiv oE _); cbn. - match goal with |- _ <~> ?F = ?G => exact (equiv_path_sigma_hprop F G) end. -Defined. - -(** Two pointed equivalences are equal if their underlying pointed functions are pointed homotopic. *) -Definition equiv_path_pequiv `{Funext} {A B : pType} (f g : A <~>* B) - : (f ==* g) <~> (f = g) - := equiv_path_pequiv' f g oE equiv_path_pforall f g. - -Definition path_pequiv `{Funext} {A B : pType} (f g : A <~>* B) - : (f ==* g) -> (f = g) - := equiv_path_pequiv f g. - -(** Pointed types of pointed maps *) - -(** A family of pointed types gives rise to a [pFam]. *) -Definition pointed_fam {A : pType} (B : A -> pType) : pFam A - := Build_pFam (pointed_type o B) (point (B (point A))). - -(** The section of a family of pointed types *) -Definition point_pforall {A : pType} (B : A -> pType) : pForall A (pointed_fam B) - := Build_pForall A (pointed_fam B) (fun x => point (B x)) 1. - -(** The pointed type of pointed maps. For dependent pointed maps we need a family of pointed types, not just a family of types with a point over the basepoint of [A]. *) -Definition ppForall (A : pType) (B : A -> pType) : pType - := [pForall A (pointed_fam B), point_pforall B]. - -Definition ppMap (A B : pType) : pType - := ppForall A (fun _ => B). - -Infix "->**" := ppMap : pointed_scope. -Notation "'ppforall' x .. y , P" - := (ppForall _ (fun x => .. (ppForall _ (fun y => P)) ..)) - : pointed_scope. - (** ** 1-categorical properties of [pForall]. *) Definition phomotopy_postwhisker {A : pType} {P : pFam A} @@ -594,18 +404,30 @@ Proof. by pelim p f g. Defined. -Definition equiv_phomotopy_concat_l `{Funext} {A B : pType} - (f g h : A ->* B) (K : g ==* f) - : f ==* h <~> g ==* h. -Proof. - refine ((equiv_path_pforall _ _)^-1%equiv oE _ oE equiv_path_pforall _ _). - rapply equiv_concat_l. - apply equiv_path_pforall. - exact K. -Defined. - (** ** The pointed category structure of [pType] *) +(** Pointed types of pointed maps *) + +(** A family of pointed types gives rise to a [pFam]. *) +Definition pointed_fam {A : pType} (B : A -> pType) : pFam A + := Build_pFam (pointed_type o B) (point (B (point A))). + +(** The section of a family of pointed types *) +Definition point_pforall {A : pType} (B : A -> pType) : pForall A (pointed_fam B) + := Build_pForall A (pointed_fam B) (fun x => point (B x)) 1. + +(** The pointed type of pointed maps. For dependent pointed maps we need a family of pointed types, not just a family of types with a point over the basepoint of [A]. *) +Definition ppForall (A : pType) (B : A -> pType) : pType + := [pForall A (pointed_fam B), point_pforall B]. + +Definition ppMap (A B : pType) : pType + := ppForall A (fun _ => B). + +Infix "->**" := ppMap : pointed_scope. +Notation "'ppforall' x .. y , P" + := (ppForall _ (fun x => .. (ppForall _ (fun y => P)) ..)) + : pointed_scope. + (** The constant (zero) map *) Definition pconst {A B : pType} : A ->* B := point_pforall (fun _ => B). @@ -624,39 +446,41 @@ Proof. exact (concat_1p _)^. Defined. -(** * pType as a wild category *) +(** * pType and pForall as wild categories *) + +(** Note that the definitions for [pForall] are also used for the higher structure in [pType]. *) (** pType is a graph *) Global Instance isgraph_ptype : IsGraph pType := Build_IsGraph pType (fun X Y => X ->* Y). -(** pType is a 0-coherent 1-category *) -Global Instance is01cat_ptype : Is01Cat pType - := Build_Is01Cat pType _ (@pmap_idmap) (@pmap_compose). - (** pForall is a graph *) Global Instance isgraph_pforall (A : pType) (P : pFam A) : IsGraph (pForall A P) := Build_IsGraph _ pHomotopy. -Global Instance is2graph_ptype : Is2Graph pType := fun f g => _. - -Global Instance is2graph_pforall (A : pType) (P : pFam A) - : Is2Graph (pForall A P) - := fun f g => _. +(** pType is a 0-coherent 1-category *) +Global Instance is01cat_ptype : Is01Cat pType + := Build_Is01Cat pType _ (@pmap_idmap) (@pmap_compose). (** pForall is a 0-coherent 1-category *) Global Instance is01cat_pforall (A : pType) (P : pFam A) : Is01Cat (pForall A P). Proof. econstructor. - exact phomotopy_reflexive. - - intros a b c f g. exact (phomotopy_transitive _ _ _ g f). + - intros a b c f g. exact (g @* f). Defined. +Global Instance is2graph_ptype : Is2Graph pType := fun f g => _. + +Global Instance is2graph_pforall (A : pType) (P : pFam A) + : Is2Graph (pForall A P) + := fun f g => _. + (** pForall is a 0-coherent 1-groupoid *) Global Instance is0gpd_pforall (A : pType) (P : pFam A) : Is0Gpd (pForall A P). Proof. - srapply Build_Is0Gpd. intros ? ? h. exact (phomotopy_symmetric _ _ h). + srapply Build_Is0Gpd. intros ? ? h. exact h^*. Defined. (** pType is a 1-coherent 1-category *) @@ -674,57 +498,8 @@ Proof. - intros ? ? f; exact (pmap_precompose_idmap f). Defined. -(** Under funext, pType has morphism extensionality *) -Global Instance hasmorext_ptype `{Funext} : HasMorExt pType. -Proof. - srapply Build_HasMorExt; intros A B f g. - refine (isequiv_homotopic (equiv_path_pforall f g)^-1%equiv _). - intros []; reflexivity. -Defined. - -(** pType has equivalences *) -Global Instance hasequivs_ptype : HasEquivs pType. -Proof. - srapply ( - Build_HasEquivs _ _ _ _ _ pEquiv (fun A B f => IsEquiv f)); - intros A B f; cbn; intros. - - exact f. - - exact _. - - exact (Build_pEquiv _ _ f _). - - reflexivity. - - exact (pequiv_inverse f). - - apply peissect. - - cbn. refine (peisretr f). - - rapply (isequiv_adjointify f g). - + intros x; exact (r x). - + intros x; exact (s x). -Defined. - -Global Instance hasmorext_core_ptype `{Funext} : HasMorExt (core pType). -Proof. - snrapply Build_HasMorExt. - intros a b f g. - unfold GpdHom_path. - cbn in f, g. - (* [GpdHom_path] and the inverse of [equiv_path_pequiv] are not definitionally equal, but they compute to definitionally equal things on [idpath]. *) - apply (isequiv_homotopic (equiv_path_pequiv f g)^-1%equiv). - intro p; induction p; cbn. - reflexivity. -Defined. - -(** pType is a univalent 1-coherent 1-category *) -Global Instance isunivalent_ptype `{Univalence} : IsUnivalent1Cat pType. -Proof. - srapply Build_IsUnivalent1Cat; intros A B. - (* [cate_equiv_path] is almost definitionally equal to [pequiv_path]. Both are defined by path induction, sending [idpath A] to [id_cate A] and [pequiv_pmap_idmap A], respectively. [id_cate A] is almost definitionally equal to [pequiv_pmap_idmap A], except that the former uses [catie_adjointify], so the adjoint law is different. However, the underlying pointed maps are definitionally equal. *) - refine (isequiv_homotopic pequiv_path _). - intros []. - apply equiv_path_pequiv'. (* Change to equality as pointed functions. *) - reflexivity. -Defined. - -(** pType is a pointed category *) -Global Instance ispointedcat_ptype : IsPointedCat pType. +(** pType is a pointed category *) +Global Instance ispointedcat_ptype : IsPointedCat pType. Proof. snrapply Build_IsPointedCat. + exact pUnit. @@ -839,6 +614,274 @@ Proof. + intros. reflexivity. Defined. +(** Some higher homotopies *) + +(** Horizontal composition of homotopies. *) +Notation "p @@* q" := (p $@@ q). + +(** ** Funext for pointed types and direct consequences. *) + +(** By funext pointed homotopies are equivalent to paths *) +Definition equiv_path_pforall `{Funext} {A : pType} + {P : pFam A} (f g : pForall A P) + : (f ==* g) <~> (f = g). +Proof. + refine (_ oE (issig_phomotopy f g)^-1). + revert f g; apply (equiv_path_issig_contr (issig_pforall A P)). + { intros [f feq]; cbn. + exists (fun a => 1%path). + exact (concat_pV _)^. } + intros [f feq]; cbn. + contr_sigsig f (fun a:A => idpath (f a)); cbn. + refine (contr_equiv' {feq' : f (point A) = dpoint P & feq = feq'} _). + refine (equiv_functor_sigma' (equiv_idmap _) _); intros p. + refine (_^-1 oE equiv_path_inverse _ _). + apply equiv_moveR_1M. +Defined. + +Definition path_pforall `{Funext} {A : pType} {P : pFam A} {f g : pForall A P} + : (f ==* g) -> (f = g) := equiv_path_pforall f g. + +(** We note that the inverse of [path_pforall] computes definitionally on reflexivity, and hence [path_pforall] itself computes typally so. *) +Definition equiv_inverse_path_pforall_1 `{Funext} {A : pType} {P : pFam A} (f : pForall A P) + : (equiv_path_pforall f f)^-1%equiv 1%path = reflexivity f + := 1. + +Definition path_pforall_1 `{Funext} {A : pType} {P : pFam A} {f : pForall A P} + : equiv_path_pforall _ _ (reflexivity f) = 1%path + := moveR_equiv_M _ _ (equiv_inverse_path_pforall_1 f)^. + +(** Here is the inverse map without assuming funext *) +Definition phomotopy_path {A : pType} {P : pFam A} {f g : pForall A P} + : (f = g) -> (f ==* g) := ltac:(by intros []). + +(** And we prove that it agrees with the inverse of [equiv_path_pforall] *) +Definition path_equiv_path_pforall_phomotopy_path `{Funext} {A : pType} + {P : pFam A} {f g : pForall A P} + : phomotopy_path (f:=f) (g:=g) = (equiv_path_pforall f g)^-1%equiv + := ltac:(by funext []). + +(** TODO: The next few results could be proven for [GpdHom_path] in any WildCat. *) + +(** [phomotopy_path] sends concatenation to composition of pointed homotopies.*) +Definition phomotopy_path_pp {A : pType} {P : pFam A} + {f g h : pForall A P} (p : f = g) (q : g = h) + : phomotopy_path (p @ q) ==* phomotopy_path p @* phomotopy_path q. +Proof. + induction p. induction q. symmetry. apply phomotopy_compose_p1. +Defined. + +(** ** [phomotopy_path] respects 2-cells. *) +Definition phomotopy_path2 {A : pType} {P : pFam A} + {f g : pForall A P} {p p' : f = g} (q : p = p') + : phomotopy_path p ==* phomotopy_path p'. +Proof. + induction q. reflexivity. +Defined. + +(** [phomotopy_path] sends inverses to inverses.*) +Definition phomotopy_path_V {A : pType} {P : pFam A} + {f g : pForall A P} (p : f = g) + : phomotopy_path (p^) ==* (phomotopy_path p)^*. +Proof. + induction p. simpl. symmetry. exact gpd_rev_1. +Defined. + +(** Since pointed homotopies are equivalent to equalities, we can act as if they are paths and define a path induction for them. *) +Definition phomotopy_ind `{H0 : Funext} {A : pType} {P : pFam A} + {k : pForall A P} (Q : forall (k' : pForall A P), (k ==* k') -> Type) + (q : Q k (reflexivity k)) (k' : pForall A P) + : forall (H : k ==* k'), Q k' H. +Proof. + equiv_intro (equiv_path_pforall k k')^-1%equiv p. + induction p. + exact q. +Defined. + +(** Sometimes you have a goal with both a pointed homotopy [H] and [path_pforall H]. This is an induction principle that allows us to replace both of them by reflexivity at the same time. *) +Definition phomotopy_ind' `{H0 : Funext} {A : pType} {P : pFam A} + {k : pForall A P} (Q : forall (k' : pForall A P), (k ==* k') -> (k = k') -> Type) + (q : Q k (reflexivity k) 1 % path) (k' : pForall A P) (H : k ==* k') + (p : k = k') (r : path_pforall H = p) + : Q k' H p. +Proof. + induction r. + revert k' H. + rapply phomotopy_ind. + exact (transport (Q _ (reflexivity _)) path_pforall_1^ q). +Defined. + +Definition phomotopy_ind_1 `{H0 : Funext} {A : pType} {P : pFam A} + {k : pForall A P} (Q : forall (k' : pForall A P), (k ==* k') -> Type) + (q : Q k (reflexivity k)) : + phomotopy_ind Q q k (reflexivity k) = q. +Proof. + change (reflexivity k) with ((equiv_path_pforall k k)^-1%equiv (idpath k)). + apply equiv_ind_comp. +Defined. + +Definition phomotopy_ind_1' `{H0 : Funext} {A : pType} {P : pFam A} + {k : pForall A P} (Q : forall (k' : pForall A P), (k ==* k') -> (k = k') -> Type) + (q : Q k (reflexivity k) 1 % path) + : phomotopy_ind' Q q k (reflexivity k) (path_pforall (reflexivity k)) (1 % path) + = transport (Q k (reflexivity k)) path_pforall_1^ q. +Proof. + srapply phomotopy_ind_1. +Defined. + +(** Every homotopy between pointed maps of sets is a pointed homotopy. *) +Definition phomotopy_homotopy_hset {X Y : pType} `{IsHSet Y} {f g : X ->* Y} (h : f == g) + : f ==* g. +Proof. + apply (Build_pHomotopy h). + apply path_ishprop. +Defined. + +(** Pointed homotopies in a set form an HProp. *) +Global Instance ishprop_phomotopy_hset `{Funext} {X Y : pType} `{IsHSet Y} (f g : X ->* Y) + : IsHProp (f ==* g) + := inO_equiv_inO' (O:=Tr (-1)) _ (issig_phomotopy f g). + +(** ** Operations on equivalences needed to make pType a wild category with equivalences *) + +(** The inverse equivalence of a pointed equivalence is again a pointed equivalence *) +Definition pequiv_inverse {A B} (f : A <~>* B) : B <~>* A. +Proof. + snrapply Build_pEquiv. + 1: apply (Build_pMap _ _ f^-1). + 1: apply moveR_equiv_V; symmetry; apply point_eq. + exact _. +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. +Proof. + srefine (Build_pHomotopy _ _). + 1: apply (eissect f). + simpl. unfold moveR_equiv_V. + pointed_reduce. + symmetry. + refine (concat_p1 _ @ concat_1p _ @ concat_1p _). +Defined. + +(* A pointed equivalence is a retraction of its inverse *) +Definition peisretr {A B : pType} (f : A <~>* B) + : f o* (pequiv_inverse f) ==* pmap_idmap. +Proof. + srefine (Build_pHomotopy _ _). + 1: apply (eisretr f). + pointed_reduce. + unfold moveR_equiv_V. + refine (eisadj f _ @ _). + symmetry. + exact (concat_p1 _ @ concat_p1 _ @ ap _ (concat_1p _)). +Defined. + +(** Univalence for pointed types *) +Definition equiv_path_ptype `{Univalence} (A B : pType) : A <~>* B <~> A = B. +Proof. + refine (equiv_path_from_contr A (fun C => A <~>* C) pequiv_pmap_idmap _ B). + nrapply (contr_equiv' { X : Type & { f : A <~> X & {x : X & f pt = x} }}). + 1: make_equiv. + rapply (contr_equiv' { X : Type & A <~> X }). + nrapply equiv_functor_sigma_id; intro X; symmetry. + rapply equiv_sigma_contr. + (** If you replace the type in the second line with { Xf : {X : Type & A <~> X} & {x : Xf.1 & Xf.2 pt = x} }, then the third line completes the proof, but that results in an extra universe variable. *) +Defined. + +Definition path_ptype `{Univalence} {A B : pType} : (A <~>* B) -> A = B + := equiv_path_ptype A B. + +(** The inverse map can be defined without Univalence. *) +Definition pequiv_path {A B : pType} (p : A = B) : (A <~>* B) + := match p with idpath => pequiv_pmap_idmap end. + +(** This just confirms that it is definitionally the inverse map. *) +Definition pequiv_path_equiv_path_ptype_inverse `{Univalence} {A B : pType} + : @pequiv_path A B = (equiv_path_ptype A B)^-1 + := idpath. + +Global Instance isequiv_pequiv_path `{Univalence} {A B : pType} + : IsEquiv (@pequiv_path A B) + := isequiv_inverse (equiv_path_ptype A B). + +(** Two pointed equivalences are equal if their underlying pointed functions are equal. This requires [Funext] for knowing that [IsEquiv] is an [HProp]. *) +Definition equiv_path_pequiv' `{Funext} {A B : pType} (f g : A <~>* B) + : (f = g :> (A ->* B)) <~> (f = g :> (A <~>* B)). +Proof. + refine ((equiv_ap' (issig_pequiv A B)^-1%equiv f g)^-1%equiv oE _); cbn. + match goal with |- _ <~> ?F = ?G => exact (equiv_path_sigma_hprop F G) end. +Defined. + +(** Two pointed equivalences are equal if their underlying pointed functions are pointed homotopic. *) +Definition equiv_path_pequiv `{Funext} {A B : pType} (f g : A <~>* B) + : (f ==* g) <~> (f = g) + := equiv_path_pequiv' f g oE equiv_path_pforall f g. + +Definition path_pequiv `{Funext} {A B : pType} (f g : A <~>* B) + : (f ==* g) -> (f = g) + := equiv_path_pequiv f g. + +Definition equiv_phomotopy_concat_l `{Funext} {A B : pType} + (f g h : A ->* B) (K : g ==* f) + : f ==* h <~> g ==* h. +Proof. + refine ((equiv_path_pforall _ _)^-1%equiv oE _ oE equiv_path_pforall _ _). + rapply equiv_concat_l. + apply equiv_path_pforall. + exact K. +Defined. + +(** Under funext, pType has morphism extensionality *) +Global Instance hasmorext_ptype `{Funext} : HasMorExt pType. +Proof. + srapply Build_HasMorExt; intros A B f g. + refine (isequiv_homotopic (equiv_path_pforall f g)^-1%equiv _). + intros []; reflexivity. +Defined. + +(** pType has equivalences *) +Global Instance hasequivs_ptype : HasEquivs pType. +Proof. + srapply ( + Build_HasEquivs _ _ _ _ _ pEquiv (fun A B f => IsEquiv f)); + intros A B f; cbn; intros. + - exact f. + - exact _. + - exact (Build_pEquiv _ _ f _). + - reflexivity. + - exact (pequiv_inverse f). + - apply peissect. + - cbn. refine (peisretr f). + - rapply (isequiv_adjointify f g). + + intros x; exact (r x). + + intros x; exact (s x). +Defined. + +Global Instance hasmorext_core_ptype `{Funext} : HasMorExt (core pType). +Proof. + snrapply Build_HasMorExt. + intros a b f g. + unfold GpdHom_path. + cbn in f, g. + (* [GpdHom_path] and the inverse of [equiv_path_pequiv] are not definitionally equal, but they compute to definitionally equal things on [idpath]. *) + apply (isequiv_homotopic (equiv_path_pequiv f g)^-1%equiv). + intro p; induction p; cbn. + reflexivity. +Defined. + +(** pType is a univalent 1-coherent 1-category *) +Global Instance isunivalent_ptype `{Univalence} : IsUnivalent1Cat pType. +Proof. + srapply Build_IsUnivalent1Cat; intros A B. + (* [cate_equiv_path] is almost definitionally equal to [pequiv_path]. Both are defined by path induction, sending [idpath A] to [id_cate A] and [pequiv_pmap_idmap A], respectively. [id_cate A] is almost definitionally equal to [pequiv_pmap_idmap A], except that the former uses [catie_adjointify], so the adjoint law is different. However, the underlying pointed maps are definitionally equal. *) + refine (isequiv_homotopic pequiv_path _). + intros []. + apply equiv_path_pequiv'. (* Change to equality as pointed functions. *) + reflexivity. +Defined. + (** The free base point added to a type. This is in fact a functor and left adjoint to the forgetful functor pType to Type. *) Definition pointify (S : Type) : pType := [S + Unit, inr tt]. diff --git a/theories/Pointed/pFiber.v b/theories/Pointed/pFiber.v index 189ccf533ad..92558e3cff7 100644 --- a/theories/Pointed/pFiber.v +++ b/theories/Pointed/pFiber.v @@ -8,15 +8,13 @@ Local Open Scope pointed_scope. (** ** Pointed fibers *) -Definition pfiber {A B : pType} (f : A ->* B) : pType. -Proof. - nrefine ([hfiber f (point B), _]). - exists (point A). - apply point_eq. -Defined. +Global Instance ispointed_fiber {A B : pType} (f : A ->* B) : IsPointed (hfiber f (point B)) + := (point A; point_eq f). + +Definition pfiber {A B : pType} (f : A ->* B) : pType := [hfiber f (point B), _]. Definition pfib {A B : pType} (f : A ->* B) : pfiber f ->* A - := (Build_pMap (pfiber f) A pr1 1). + := Build_pMap (pfiber f) A pr1 1. (** The double fiber object is equivalent to loops on the base. *) Definition pfiber2_loops {A B : pType} (f : A ->* B) diff --git a/theories/Pointed/pHomotopy.v b/theories/Pointed/pHomotopy.v deleted file mode 100644 index ff24a875381..00000000000 --- a/theories/Pointed/pHomotopy.v +++ /dev/null @@ -1,72 +0,0 @@ -Require Import Basics. -Require Import Types. -Require Import Pointed.Core. -Require Import WildCat. - -Local Open Scope pointed_scope. - -(** Some higher homotopies *) - -Definition phomotopy_inverse_1 {A : pType} {P : pFam A} {f : pForall A P} - : (phomotopy_reflexive f)^* ==* phomotopy_reflexive f. -Proof. - srapply Build_pHomotopy. - + reflexivity. - + pointed_reduce. reflexivity. -Defined. - -(** [phomotopy_path] sends concatenation to composition of pointed homotopies.*) -Definition phomotopy_path_pp {A : pType} {P : pFam A} - {f g h : pForall A P} (p : f = g) (q : g = h) - : phomotopy_path (p @ q) ==* phomotopy_path p @* phomotopy_path q. -Proof. - induction p. induction q. symmetry. apply phomotopy_compose_p1. -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. -Proof. - 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. -Proof. - exact (p $@R f). -Defined. - -(** ** [phomotopy_path] respects 2-cells. *) -Definition phomotopy_path2 {A : pType} {P : pFam A} - {f g : pForall A P} {p p' : f = g} (q : p = p') - : phomotopy_path p ==* phomotopy_path p'. -Proof. - induction q. reflexivity. -Defined. - -(** [phomotopy_path] sends inverses to inverses.*) -Definition phomotopy_path_V {A : pType} {P : pFam A} - {f g : pForall A P} (p : f = g) - : phomotopy_path (p^) ==* (phomotopy_path p)^*. -Proof. - induction p. simpl. symmetry. apply phomotopy_inverse_1. -Defined. - -(* TODO: Remove [Funext] when whiskering is reproven without it. *) -Definition phomotopy_hcompose `{Funext} {A : pType} {P : pFam A} {f g h : pForall A P} - {p p' : f ==* g} {q q' : g ==* h} (r : p ==* p') (s : q ==* q') : - p @* q ==* p' @* q'. -Proof. - exact ((s $@R p) $@ (q' $@L r)). -Defined. - -Notation "p @@* q" := (phomotopy_hcompose p q). - -(** Pointed homotopies in a set form an HProp. *) -Global Instance ishprop_phomotopy_hset `{Univalence} {X Y : pType} `{IsHSet Y} (f g : X ->* Y) - : IsHProp (f ==* g). -Proof. - rapply (transport IsHProp (x := {p : f == g & p (point X) = dpoint_eq f @ (dpoint_eq g)^})). - apply path_universe_uncurried; issig. -Defined. diff --git a/theories/Pointed/pMap.v b/theories/Pointed/pMap.v index 76952bae182..9b8c2243abc 100644 --- a/theories/Pointed/pMap.v +++ b/theories/Pointed/pMap.v @@ -1,6 +1,5 @@ Require Import Basics Types. Require Import Pointed.Core. -Require Import Pointed.pHomotopy. Local Open Scope pointed_scope.