Merge pull request #1797 from jdchristensen/phomotopy

pHomotopy, pmap_postwhisker

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*

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.

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 _ @* _).

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.