From 8b57d0b87525eb96f72df02a5719b5ca28e01f60 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Sat, 30 Dec 2023 11:19:54 -0500
Subject: [PATCH 01/11] Pointed/Core: get rid of stray universe variable in
 pHomotopy

---
 theories/Algebra/AbSES/SixTerm.v  | 2 +-
 theories/Homotopy/ExactSequence.v | 4 ++--
 theories/Pointed/Core.v           | 2 +-
 3 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/theories/Algebra/AbSES/SixTerm.v b/theories/Algebra/AbSES/SixTerm.v
index 856e3f0a52e..ebff6bc1063 100644
--- a/theories/Algebra/AbSES/SixTerm.v
+++ b/theories/Algebra/AbSES/SixTerm.v
@@ -194,7 +194,7 @@ Local Definition isexact_ext_cyclic_ab_iii@{u v w | u < v, v < w} `{Univalence}
 (* 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}
   (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))
          o* (pequiv_groupisomorphism (equiv_Z1_hom A))^-1*).
diff --git a/theories/Homotopy/ExactSequence.v b/theories/Homotopy/ExactSequence.v
index f39f0032148..b2b2c9a2757 100644
--- a/theories/Homotopy/ExactSequence.v
+++ b/theories/Homotopy/ExactSequence.v
@@ -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}
diff --git a/theories/Pointed/Core.v b/theories/Pointed/Core.v
index e3cd2fc263b..96c39777ff4 100644
--- a/theories/Pointed/Core.v
+++ b/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.

From e995adb437312afd9cde53b0c9fd1082bdfa96ee Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Sat, 30 Dec 2023 11:20:24 -0500
Subject: [PATCH 02/11] Adjust pmap_(pre/post)whisker in pHomotopy.v

---
 theories/Pointed/pHomotopy.v | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/theories/Pointed/pHomotopy.v b/theories/Pointed/pHomotopy.v
index ff24a875381..16ba549c9e9 100644
--- a/theories/Pointed/pHomotopy.v
+++ b/theories/Pointed/pHomotopy.v
@@ -25,16 +25,18 @@ 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 : pType@{u1}} {B : pType@{u2}} {C : pType@{u3}}
+  {f g : A ->* B} (h : B ->* C) (p : f ==* g)
+  : h o* f ==* h o* g.
 Proof.
-  exact (h $@L p).
+  exact (cat_postwhisker (A:=pType@{v}) h 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 : pType@{u1}} {B : pType@{u2}} {C : pType@{u3}}
+  (f : A ->* B) {g h : B ->* C} (p : g $== h)
+  : g o* f ==* h o* f.
 Proof.
-  exact (p $@R f).
+  exact (cat_prewhisker (A:=pType@{v}) p f).
 Defined.
 
 (** ** [phomotopy_path] respects 2-cells. *)

From 838b936c3eb0688738cbf3e04586bf345b9544df Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Sat, 30 Dec 2023 15:02:25 -0500
Subject: [PATCH 03/11] pHomotopy: remove redundant pmap_postwhisker/prewhisker

---
 theories/Algebra/AbSES/SixTerm.v |  7 +++----
 theories/Pointed/pHomotopy.v     | 16 ----------------
 2 files changed, 3 insertions(+), 20 deletions(-)

diff --git a/theories/Algebra/AbSES/SixTerm.v b/theories/Algebra/AbSES/SixTerm.v
index ebff6bc1063..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} (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/Pointed/pHomotopy.v b/theories/Pointed/pHomotopy.v
index 16ba549c9e9..fa65bca86a0 100644
--- a/theories/Pointed/pHomotopy.v
+++ b/theories/Pointed/pHomotopy.v
@@ -23,22 +23,6 @@ Proof.
   induction p. induction q. symmetry. apply phomotopy_compose_p1.
 Defined.
 
-(** ** Whiskering of pointed homotopies by pointed functions *)
-
-Definition pmap_postwhisker {A : pType@{u1}} {B : pType@{u2}} {C : pType@{u3}}
-  {f g : A ->* B} (h : B ->* C) (p : f ==* g)
-  : h o* f ==* h o* g.
-Proof.
-  exact (cat_postwhisker (A:=pType@{v}) h p).
-Defined.
-
-Definition pmap_prewhisker {A : pType@{u1}} {B : pType@{u2}} {C : pType@{u3}}
-  (f : A ->* B) {g h : B ->* C} (p : g $== h)
-  : g o* f ==* h o* f.
-Proof.
-  exact (cat_prewhisker (A:=pType@{v}) p 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')

From 5c0c5279b294cb89808c4fa1729d214f3f3ddd03 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Sat, 30 Dec 2023 15:07:05 -0500
Subject: [PATCH 04/11] pHomotopy: remove Funext in phomotopy_hcompose

---
 theories/Pointed/pHomotopy.v | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/theories/Pointed/pHomotopy.v b/theories/Pointed/pHomotopy.v
index fa65bca86a0..e3f62413b6f 100644
--- a/theories/Pointed/pHomotopy.v
+++ b/theories/Pointed/pHomotopy.v
@@ -39,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).
 

From 395db1e30d594a69eb29f7a9be35ec6d766d65cd Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Sat, 30 Dec 2023 15:08:24 -0500
Subject: [PATCH 05/11] pFiber: minor clean-up to main definition

---
 theories/Pointed/pFiber.v | 12 +++++-------
 1 file changed, 5 insertions(+), 7 deletions(-)

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)

From bd5717dc9be5c47c09dc63fe77a75caf50a3d326 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Sat, 30 Dec 2023 15:15:52 -0500
Subject: [PATCH 06/11] Pointed/Core: remove stray univ var from
 phomotopy_refl/symm/trans

---
 theories/Pointed/Core.v | 33 +++++++++++++++++++++++----------
 1 file changed, 23 insertions(+), 10 deletions(-)

diff --git a/theories/Pointed/Core.v b/theories/Pointed/Core.v
index 96c39777ff4..1b14aaf47ec 100644
--- a/theories/Pointed/Core.v
+++ b/theories/Pointed/Core.v
@@ -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 *)

From 8d5039dcb90d5f6a451be1c70471d314f8d1ddbe Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Sat, 30 Dec 2023 15:16:56 -0500
Subject: [PATCH 07/11] ExactSequence: avoid some WildCat notation to improve
 univ vars

This avoids stray universe variables, and also allows the universe
variables of the input types to be free.
---
 theories/Homotopy/ExactSequence.v | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/theories/Homotopy/ExactSequence.v b/theories/Homotopy/ExactSequence.v
index b2b2c9a2757..de10df4761a 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).
@@ -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 _ @* _).

From ed723f1adbe00deed974f3b0623cded6b693465f Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Mon, 1 Jan 2024 12:38:50 -0500
Subject: [PATCH 08/11] pHomotopy: rm unneeded results; make
 ishprop_phomotopy_hset only use Funext

---
 theories/Pointed/pHomotopy.v | 28 +++++++---------------------
 1 file changed, 7 insertions(+), 21 deletions(-)

diff --git a/theories/Pointed/pHomotopy.v b/theories/Pointed/pHomotopy.v
index e3f62413b6f..65d9eed90c0 100644
--- a/theories/Pointed/pHomotopy.v
+++ b/theories/Pointed/pHomotopy.v
@@ -2,19 +2,13 @@ Require Import Basics.
 Require Import Types.
 Require Import Pointed.Core.
 Require Import WildCat.
+Require Import Truncations.Core.
+Require Import ReflectiveSubuniverse.
 
 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)
@@ -36,20 +30,12 @@ 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.
+  induction p. simpl. symmetry. exact gpd_rev_1.
 Defined.
 
-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'
-  := cat_comp2 (A:=pForall A P) r s.
-
-Notation "p @@* q" := (phomotopy_hcompose p q).
+Notation "p @@* q" := (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.
+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).

From eb5c4a1911788eb9f53c2826c05ad6186fa1df10 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Mon, 1 Jan 2024 12:40:02 -0500
Subject: [PATCH 09/11] Pointed/Core: rm unneeded equiv_path_pmap_1; update
 comments

---
 theories/Pointed/Core.v | 30 ++++++++++++------------------
 1 file changed, 12 insertions(+), 18 deletions(-)

diff --git a/theories/Pointed/Core.v b/theories/Pointed/Core.v
index 1b14aaf47ec..5dc046ffd40 100644
--- a/theories/Pointed/Core.v
+++ b/theories/Pointed/Core.v
@@ -60,7 +60,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,19 +85,19 @@ 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)
   := pForall A (pfam_phomotopy f g).
 
@@ -124,26 +123,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 +148,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].
 
@@ -377,7 +374,7 @@ Definition path_equiv_path_pforall_phomotopy_path `{Funext} {A : pType}
   : 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. *)
+(** 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.
@@ -386,12 +383,7 @@ 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 *)
+(** 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)
@@ -637,7 +629,9 @@ 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

From e6a719dffad9cb84e4d62bd695b653b578922679 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Mon, 1 Jan 2024 12:48:40 -0500
Subject: [PATCH 10/11] Pointed: merge pHomotopy into Core: lots of reordering
 of things

---
 theories/Pointed.v           |   1 -
 theories/Pointed/Core.v      | 570 +++++++++++++++++++----------------
 theories/Pointed/pHomotopy.v |  41 ---
 theories/Pointed/pMap.v      |   1 -
 4 files changed, 303 insertions(+), 310 deletions(-)
 delete mode 100644 theories/Pointed/pHomotopy.v

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 5dc046ffd40..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.
 
@@ -341,203 +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_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)^.
-
-(** 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}
@@ -599,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).
@@ -637,20 +454,14 @@ Defined.
 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).
@@ -660,6 +471,12 @@ Proof.
   - 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.
@@ -681,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.
@@ -846,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/pHomotopy.v b/theories/Pointed/pHomotopy.v
deleted file mode 100644
index 65d9eed90c0..00000000000
--- a/theories/Pointed/pHomotopy.v
+++ /dev/null
@@ -1,41 +0,0 @@
-Require Import Basics.
-Require Import Types.
-Require Import Pointed.Core.
-Require Import WildCat.
-Require Import Truncations.Core.
-Require Import ReflectiveSubuniverse.
-
-Local Open Scope pointed_scope.
-
-(** Some higher homotopies *)
-
-(** [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.
-
-Notation "p @@* q" := (p $@@ q).
-
-(** 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).
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.
 

From ab2543e206afa4b3cce0622eefabcb8af703c91c Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Mon, 1 Jan 2024 12:49:14 -0500
Subject: [PATCH 11/11] Remove three Local Instances that are already Global
 Instances

---
 theories/Algebra/Groups/ShortExactSequence.v | 3 ---
 theories/Homotopy/ExactSequence.v            | 3 ---
 2 files changed, 6 deletions(-)

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 de10df4761a..6c60c8c14e9 100644
--- a/theories/Homotopy/ExactSequence.v
+++ b/theories/Homotopy/ExactSequence.v
@@ -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.  *)