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/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).
@@ -182,9 +182,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 +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 : 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 +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)
-  (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 +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)
@@ -442,7 +442,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/Core.v

@@ -99,7 +99,7 @@ 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.
@@ -254,32 +254,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 *)
 
@@ -650,13 +663,13 @@ 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.
 
 (** 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 *)

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)

theories/Pointed/pHomotopy.v

@@ -23,20 +23,6 @@ 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')
@@ -53,13 +39,10 @@ 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}
+Definition phomotopy_hcompose {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.
+  p @* q ==* p' @* q'
+  := cat_comp2 (A:=pForall A P) r s.
 
 Notation "p @@* q" := (phomotopy_hcompose p q).