From f3a2f1dfab31268a407c62b0094ee59f29fbd488 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Sat, 2 Sep 2023 08:06:19 -0400
Subject: [PATCH 01/13] Add WildCat/ZeroGroupoid.v

---
 theories/WildCat.v              |   1 +
 theories/WildCat/EquivGpd.v     |   2 +
 theories/WildCat/ZeroGroupoid.v | 131 ++++++++++++++++++++++++++++++++
 3 files changed, 134 insertions(+)
 create mode 100644 theories/WildCat/ZeroGroupoid.v

diff --git a/theories/WildCat.v b/theories/WildCat.v
index 2ed8c94bb6d..639dd183114 100644
--- a/theories/WildCat.v
+++ b/theories/WildCat.v
@@ -23,6 +23,7 @@ Require Export WildCat.Prod.
 Require Export WildCat.Sum.
 Require Export WildCat.Forall.
 Require Export WildCat.Sigma.
+Require Export WildCat.ZeroGroupoid.
 
 (* Higher categories *)
 Require Export WildCat.TwoOneCat.
diff --git a/theories/WildCat/EquivGpd.v b/theories/WildCat/EquivGpd.v
index d513732f029..67fa677c2f4 100644
--- a/theories/WildCat/EquivGpd.v
+++ b/theories/WildCat/EquivGpd.v
@@ -7,6 +7,8 @@ Require Import WildCat.Sigma.
 
 (** * Equivalences of 0-groupoids, and split essentially surjective functors *)
 
+(** For an alternate definition of equivalences of 0-groupoids, see ZeroGroupoid.v. *)
+
 (** We could define these similarly for more general categories too, but we'd need to use [HasEquivs] and [$<~>] instead of [$==]. *)
 
 Class SplEssSurj {A B : Type} `{Is0Gpd A, Is0Gpd B}
diff --git a/theories/WildCat/ZeroGroupoid.v b/theories/WildCat/ZeroGroupoid.v
new file mode 100644
index 00000000000..497622ff922
--- /dev/null
+++ b/theories/WildCat/ZeroGroupoid.v
@@ -0,0 +1,131 @@
+Require Import Basics.Overture Basics.Tactics.
+Require Import WildCat.Core WildCat.Equiv.
+
+(** * The wild 1-category of 0-groupoids. *)
+
+(** Here we define a wild 1-category structure on the type of 0-groupoids.  We think of the 1-cells [g $== h] in a 0-groupoid [G] as a substitute for the paths [g = h], and so we closely follow the definitions used for the 1-category of types with [=] replaced by [$==].  In fact, the 1-category structure on types should be the pullback of the 1-category structure on 0-groupoids along a natural map [Type -> ZeroGpd] which sends [A] to [A] equipped with its path types.  A second motivating example is the 0-groupoid with underlying type [A -> B] and homotopies as the 1-cells.  The definitions chosen here exactly make the Yoneda lemma [opyon_equiv_0gpd] go through. *)
+
+Record ZeroGpd := {
+  carrier :> Type;
+  isgraph_carrier : IsGraph carrier;
+  is01cat_carrier : Is01Cat carrier;
+  is0gpd_carrier : Is0Gpd carrier;  
+}.
+
+Global Existing Instance isgraph_carrier.
+Global Existing Instance is01cat_carrier.
+Global Existing Instance is0gpd_carrier.
+
+Record ZeroGpdMorphism (G H : ZeroGpd) := {
+  zerogpd_fun :> carrier G -> carrier H;
+  is0functor_zerogpd_fun : Is0Functor zerogpd_fun;
+}.
+
+Global Existing Instance is0functor_zerogpd_fun.
+
+Global Instance isgraph_0gpd : IsGraph ZeroGpd.
+Proof.
+  apply Build_IsGraph.
+  exact ZeroGpdMorphism.
+Defined.
+
+Global Instance is01cat_0gpd : Is01Cat ZeroGpd.
+Proof.
+  srapply Build_Is01Cat.
+  - intro G.
+    snrapply Build_ZeroGpdMorphism.
+    1: exact idmap.
+    snrapply Build_Is0Functor.
+    intros g1 g2.
+    exact idmap.
+  - intros G H K f g.
+    snrapply Build_ZeroGpdMorphism.
+    1: exact (f o g).
+    snrapply Build_Is0Functor; cbn beta.
+    intros g1 g2 p.
+    apply is0functor_zerogpd_fun, is0functor_zerogpd_fun, p.
+Defined.
+
+Global Instance is2graph_0gpd : Is2Graph ZeroGpd.
+Proof.
+  intros G H.
+  snrapply Build_IsGraph.
+  intros f g.
+  exact (forall x : G, f x $== g x).
+Defined.
+
+Global Instance is1cat_0gpd : Is1Cat ZeroGpd.
+Proof.
+  snrapply Build_Is1Cat.
+  - intros G H.
+    srapply Build_Is01Cat.
+    + intro f. exact (fun x => Id (f x)).
+    + intros f g h p q. exact (fun x => q x $@ p x).
+  - intros G H.
+    srapply Build_Is0Gpd.
+    intros f g p. exact (fun x => (p x)^$).
+  - intros G H K f.
+    srapply Build_Is0Functor.
+    intros g h p x.
+    cbn.
+    exact (fmap f (p x)).
+  - intros G H K f.
+    srapply Build_Is0Functor.
+    intros g h p x.
+    cbn.
+    exact (p (f x)).
+  - reflexivity.
+  - reflexivity.
+  - reflexivity.
+Defined.
+
+(** We define equivalences of 0-groupoids.  Note that this differs from [IsEquiv0Gpd] in [EquivGpd.v].  It is chosen to provide what is needed for the Yoneda lemma, and to match the concept for types, with paths replaced by 1-cells.  We are able to match the biinvertible definition.  The half-adjoint definition doesn't work, as we can prove adjointification.  We would need to be in a 1-groupoid for that to be possible.  We could also use the "wrong" definition, without the eisadj condition, and things would go through, but it wouldn't match the definition for types. *)
+Class ZeroGpdIsEquiv {G H : ZeroGpd} (f : G $-> H) := {
+  zerogpd_equiv_inv : H $-> G;
+  zerogpd_eisretr : f $o zerogpd_equiv_inv $== Id H;
+  zerogpd_equiv_inv' : H $-> G;
+  zerogpd_eissect' : zerogpd_equiv_inv' $o f $== Id G;
+}.
+
+Arguments zerogpd_equiv_inv {G H}%type_scope f {_}.
+Arguments zerogpd_eisretr {G H}%type_scope f {_} _.
+Arguments zerogpd_equiv_inv' {G H}%type_scope f {_}.
+Arguments zerogpd_eissect' {G H}%type_scope f {_} _.
+
+Definition zerogpd_inverses_homotopic {G H : ZeroGpd} (f : G $-> H) `{ZeroGpdIsEquiv _ _ f}
+  : zerogpd_equiv_inv f $== zerogpd_equiv_inv' f.
+Proof.
+  set (g := zerogpd_equiv_inv f).
+  set (g' := zerogpd_equiv_inv' f).
+  intro x.
+  refine ((zerogpd_eissect' f (g x))^$ $@ _); cbn.
+  refine (fmap g' _).
+  rapply zerogpd_eisretr.
+Defined.
+
+Definition zerogpd_eissect {G H : ZeroGpd} (f : G $-> H) `{ZeroGpdIsEquiv _ _ f}
+  : zerogpd_equiv_inv f $o f $== Id G
+  := (zerogpd_inverses_homotopic f $@R f) $@ zerogpd_eissect' f.
+
+Record ZeroGpdEquiv (G H : ZeroGpd) := {
+  zerogpd_equiv_fun :> ZeroGpdMorphism G H;
+  zerogpd_isequiv_equiv : ZeroGpdIsEquiv zerogpd_equiv_fun;
+}.
+
+Global Instance hasequivs_zerogpd : HasEquivs ZeroGpd.
+Proof.
+  srapply Build_HasEquivs; intros G H.
+  1: exact (ZeroGpdEquiv G H).
+  all:intros f.
+  - exact (ZeroGpdIsEquiv f).
+  - exact f.
+  - cbn. exact (zerogpd_isequiv_equiv _ _ f).
+  - apply Build_ZeroGpdEquiv.
+  - intros; reflexivity.
+  - exact (@zerogpd_equiv_inv _ _ f (zerogpd_isequiv_equiv _ _ f)).
+  - cbn. apply zerogpd_eissect.
+  - cbn. apply zerogpd_eisretr.
+  - intros g r s; cbn beta.
+    exact (Build_ZeroGpdIsEquiv _ _ f g r g s).
+Defined.
+

From 88412cbc30694bd9eae570c9713f3ca87414b7ae Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Sat, 2 Sep 2023 08:06:50 -0400
Subject: [PATCH 02/13] WildCat/Yoneda: use 0-groupoids to avoid FunExt,
 IsStrong

---
 theories/WildCat/Yoneda.v | 70 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 70 insertions(+)

diff --git a/theories/WildCat/Yoneda.v b/theories/WildCat/Yoneda.v
index d350fdc33e3..c21f30ae706 100644
--- a/theories/WildCat/Yoneda.v
+++ b/theories/WildCat/Yoneda.v
@@ -8,6 +8,7 @@ Require Import WildCat.Opposite.
 Require Import WildCat.FunctorCat.
 Require Import WildCat.NatTrans.
 Require Import WildCat.Prod.
+Require Import WildCat.ZeroGroupoid.
 
 (** ** Two-variable hom-functors *)
 
@@ -163,6 +164,75 @@ Proof.
   - rapply is1natural_opyoneda.
 Defined.
 
+(** We define a version of [opyon] that lands in 0-groupoids, which we regard as setoids. *)
+Definition opyon_0gpd {A : Type} `{Is1Cat A} (a : A) : Fun01 A ZeroGpd.
+Proof.
+  snrapply Build_Fun01.
+  - intro b.
+    rapply (Build_ZeroGpd (opyon a b)).
+  - snrapply Build_Is0Functor.
+    intros b c f; cbn beta.
+    snrapply Build_ZeroGpdMorphism; cbn.
+    + exact (fmap (opyon a) f).
+    + apply is0functor_postcomp.
+Defined.
+
+(** A version of the covariant Yoneda lemma which regards [opyon] as a functor taking values in 0-groupoids, using the 1-category structure on [ZeroGpd] in [ZeroGroupoid.v].  Instead of assuming that each [f c : (a $-> c) -> (b $-> c)] is an equivalence of types, it only needs to be an equivalence of 0-groupoids.  For example, this means that we have a map [g c : (b $-> c) -> (a $-> c)] such that for each [k : a $-> c], [g c (f c k) $== k], rather than [g c (f c k) = k] as the version with types requires.  Similarly, the naturality is up to 2-cells, instead of up to paths.  This allows us to avoid [Funext] and [HasMorExt] when using this result.  As a side benefit, we also don't require that [A] is strong. *)
+Definition opyon_equiv_0gpd {A : Type} `{HasEquivs A}
+  {a b : A} (f : opyon_0gpd a $<~> opyon_0gpd b)
+  : b $<~> a.
+Proof.
+  set (g := f^-1$).
+  srapply (cate_adjointify (f a (Id a)) (g b (Id b))).
+  - pose proof (gn := is1natural_natequiv _ _ g).
+    refine ((isnat (alnat:=gn) g (f a (Id a)) (Id b))^$ $@ _).
+    refine (fmap (g a) (cat_idr (f a (Id a))) $@ _).
+    1: rapply is0functor_zerogpd_fun.
+    1: exact _.
+    rapply zerogpd_eissect.
+  - pose proof (fn := is1natural_natequiv _ _ f).
+    refine ((isnat (alnat:=fn) f (g b (Id b)) (Id a))^$ $@ _).
+    refine (fmap (f b) (cat_idr (g b (Id b))) $@ _).
+    1: rapply is0functor_zerogpd_fun.
+    1: exact _.
+    rapply zerogpd_eisretr.
+  (* Not sure why typeclass inference doesn't find [is1natural_natequiv] and [is0functor_zerogpd_fun] above. *)
+Defined.
+
+(** Precomposition with a [cat_equiv] is an equivalence between the hom 0-groupoids. Note that we do not require [HasMorExt], as [equiv_precompose_cat_equiv] does. *)
+Definition equiv_precompose_cat_equiv_0gpd {A : Type} `{HasEquivs A}
+  {x y z : A} (f : x $<~> y)
+  : opyon_0gpd y z $<~> opyon_0gpd x z.
+Proof.
+  snrapply cate_adjointify.
+  - snrapply Build_ZeroGpdMorphism.
+    1: exact (cat_precomp z f).
+    exact _.
+  - snrapply Build_ZeroGpdMorphism.
+    1: exact (cat_precomp z f^-1$).
+    exact _.
+  - cbn.
+    intro g.
+    unfold cat_precomp.
+    apply compose_hV_h.
+  - cbn.
+    intro g.
+    unfold cat_precomp.
+    apply compose_hh_V.
+Defined.
+
+(** A converse to [opyon_equiv_0gpd].  Together, we get a logical equivalence between [b $<~> a] and [opyon_0gpd a $<~> opyon_0gpd b].  Note again that the converse requires [HasMorExt] when using [opyon1]. *)
+Definition natequiv_opyon_equiv_0gpd {A : Type} `{HasEquivs A}
+  {a b : A} (e : b $<~> a)
+  : opyon_0gpd a $<~> opyon_0gpd b.
+Proof.
+  snrapply Build_NatEquiv.
+  - intro c; exact (equiv_precompose_cat_equiv_0gpd e).
+  - intros c d f g; cbn.
+    unfold cat_precomp.
+    apply cat_assoc.
+Defined.
+
 (** ** The contravariant Yoneda lemma *)
 
 (** We can deduce this from the covariant version with some boilerplate. *)

From b85c246a59c68e57a6e8ffa0f91b521bb6e91ab1 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Sat, 2 Sep 2023 14:59:17 -0400
Subject: [PATCH 03/13] WildCat/Yoneda: cleanups to old proofs, e.g. (A:=A^op)
 instead of @

---
 theories/WildCat/Yoneda.v | 34 +++++++++++++++-------------------
 1 file changed, 15 insertions(+), 19 deletions(-)

diff --git a/theories/WildCat/Yoneda.v b/theories/WildCat/Yoneda.v
index c21f30ae706..7743e38073a 100644
--- a/theories/WildCat/Yoneda.v
+++ b/theories/WildCat/Yoneda.v
@@ -134,7 +134,7 @@ Defined.
 
 (** We can also deduce "full-faithfulness" on equivalences. *)
 Definition opyon_equiv {A : Type} `{HasEquivs A} `{!Is1Cat_Strong A}
-           (a b : A)
+           {a b : A}
   : (opyon1 a $<~> opyon1 b) -> (b $<~> a).
 Proof.
   intros f.
@@ -154,7 +154,7 @@ Proof.
 Defined.
 
 Definition natequiv_opyon_equiv {A : Type} `{HasEquivs A}
-  `{!HasMorExt A} (a b : A)
+  `{!HasMorExt A} {a b : A}
   : (b $<~> a) -> (opyon1 a $<~> opyon1 b).
 Proof.
   intro e.
@@ -238,19 +238,15 @@ Defined.
 (** We can deduce this from the covariant version with some boilerplate. *)
 
 Definition yon {A : Type} `{IsGraph A} (a : A) : A^op -> Type
-  := @opyon (A^op) _ a.
+  := opyon (A:=A^op) a.
 
 Global Instance is0functor_yon {A : Type} `{H : Is01Cat A} (a : A)
-  : Is0Functor (yon a).
-Proof.
-  apply is0functor_opyon.
-Defined.
+  : Is0Functor (yon a)
+  := is0functor_opyon (A:=A^op) a.
 
 Global Instance is1functor_yon {A : Type} `{H : Is1Cat A} `{!HasMorExt A} (a : A)
-  : Is1Functor (yon a).
-Proof.
-  rapply is1functor_opyon.
-Defined.
+  : Is1Functor (yon a)
+  := is1functor_opyon (A:=A^op) a.
 
 Definition yoneda {A : Type} `{Is01Cat A} (a : A)
            (F : A^op -> Type) `{!Is0Functor F}
@@ -260,17 +256,17 @@ Definition yoneda {A : Type} `{Is01Cat A} (a : A)
 Definition un_yoneda {A : Type} `{Is01Cat A} (a : A)
            (F : A^op -> Type) `{!Is0Functor F}
   : (yon a $=> F) -> F a
-  := @un_opyoneda (A^op) _ _ a F _.
+  := un_opyoneda (A:=A^op) a F.
 
 Global Instance is1natural_yoneda {A : Type} `{Is1Cat A} (a : A)
        (F : A^op -> Type) `{!Is0Functor F, !Is1Functor F} (x : F a)
   : Is1Natural (yon a) F (yoneda a F x)
-  := @is1natural_opyoneda (A^op) _ _ _ _ a F _ _ x.
+  := is1natural_opyoneda (A:=A^op) a F x.
 
 Definition yoneda_issect {A : Type} `{Is1Cat A} (a : A)
            (F : A^op -> Type) `{!Is0Functor F, !Is1Functor F} (x : F a)
   : un_yoneda a F (yoneda a F x) = x
-  := @opyoneda_issect (A^op) _ _ _ _ a F _ _ x.
+  := opyoneda_issect (A:=A^op) a F x.
 
 Definition yoneda_isretr {A : Type} `{Is1Cat_Strong A} (a : A)
            (F : A^op -> Type) `{!Is0Functor F}
@@ -279,24 +275,24 @@ Definition yoneda_isretr {A : Type} `{Is1Cat_Strong A} (a : A)
            (alpha : yon a $=> F) {alnat : Is1Natural (yon a) F alpha}
            (b : A)
   : yoneda a F (un_yoneda a F alpha) b $== alpha b
-  := @opyoneda_isretr A^op _ _ _ (is1cat_strong_op A) a F _ _ alpha alnat b.
+  := opyoneda_isretr (A:=A^op) a F alpha b.
 
 Definition yon_cancel {A : Type} `{Is01Cat A} (a b : A)
   : (yon a $=> yon b) -> (a $-> b)
   := un_yoneda a (yon b).
 
 Definition yon1 {A : Type} `{Is01Cat A} (a : A) : Fun01 A^op Type
-  := @opyon1 A^op _ _ a.
+  := opyon1 (A:=A^op) a.
 
 Definition yon11 {A : Type} `{Is1Cat A} `{!HasMorExt A} (a : A) : Fun11 A^op Type
-  := @opyon11 A^op _ _ _ _ _ a.
+  := opyon11 (A:=A^op) a.
 
 Definition yon_equiv {A : Type} `{HasEquivs A} `{!Is1Cat_Strong A}
            (a b : A)
   : (yon1 a $<~> yon1 b) -> (a $<~> b)
-  := (@opyon_equiv A^op _ _ _ _ _ _ a b).
+  := opyon_equiv (A:=A^op).
 
 Definition natequiv_yon_equiv {A : Type} `{HasEquivs A}
   `{!HasMorExt A} (a b : A)
   : (a $<~> b) -> (yon1 a $<~> yon1 b)
-  := (@natequiv_opyon_equiv A^op _ _ _ _ _ _ a b).
+  := natequiv_opyon_equiv (A:=A^op).

From c3d562058dd227cdb9b0ef8f4926f2293d700066 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Sat, 2 Sep 2023 14:59:54 -0400
Subject: [PATCH 04/13] WildCat/Yoneda: add dual of Funext-free Yoneda lemma

---
 theories/WildCat/Yoneda.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/theories/WildCat/Yoneda.v b/theories/WildCat/Yoneda.v
index 7743e38073a..546829111e2 100644
--- a/theories/WildCat/Yoneda.v
+++ b/theories/WildCat/Yoneda.v
@@ -296,3 +296,16 @@ Definition natequiv_yon_equiv {A : Type} `{HasEquivs A}
   `{!HasMorExt A} (a b : A)
   : (a $<~> b) -> (yon1 a $<~> yon1 b)
   := natequiv_opyon_equiv (A:=A^op).
+
+Definition yon_0gpd {A : Type} `{Is1Cat A} (a : A) : Fun01 A^op ZeroGpd
+  := opyon_0gpd (A:=A^op) a.
+
+Definition yon_equiv_0gpd {A : Type} `{HasEquivs A}
+  {a b : A}
+  : yon_0gpd a $<~> yon_0gpd b -> a $<~> b
+  := opyon_equiv_0gpd (A:=A^op).
+
+Definition natequiv_yon_equiv_0gpd {A : Type} `{HasEquivs A}
+  {a b : A}
+  : a $<~> b -> yon_0gpd a $<~> yon_0gpd b
+  := natequiv_opyon_equiv_0gpd (A:=A^op).

From b4764e70992b3826fd772dd52ba1358f3755ca6a Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Sat, 2 Sep 2023 15:09:10 -0400
Subject: [PATCH 05/13] Homotopy/ClassifyingSpace: adjust for changes to
 Yoneda.v

---
 theories/Homotopy/ClassifyingSpace.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/Homotopy/ClassifyingSpace.v b/theories/Homotopy/ClassifyingSpace.v
index 51a9097f182..bb9fdc6efa3 100644
--- a/theories/Homotopy/ClassifyingSpace.v
+++ b/theories/Homotopy/ClassifyingSpace.v
@@ -565,11 +565,11 @@ Lemma natequiv_bg_pi1_adjoint `{Univalence} (X : pType) `{IsConnected 0 X}
   : NatEquiv (opyon (Pi1 X)) (opyon X o B).
 Proof.
   nrefine (natequiv_compose (G := opyon (Pi1 (pTr 1 X))) _ _).
-  2: exact (natequiv_opyon_equiv (Pi1 X) _ (grp_iso_pi1_Tr _)).
+  2: exact (natequiv_opyon_equiv (A:=Group) (grp_iso_pi1_Tr _)).
   refine (natequiv_compose _ (natequiv_grp_homo_pmap_bg _)).
   refine (natequiv_compose (G := opyon (pTr 1 X) o B) _ _); revgoals.
   { refine (natequiv_prewhisker _ _).
-    refine (natequiv_opyon_equiv _ _ _^-1$).
+    refine (natequiv_opyon_equiv _^-1$).
     rapply pequiv_pclassifyingspace_pi1. }
   snrapply Build_NatEquiv.
   1: intro; exact equiv_ptr_rec.

From da850fb2ba49372520a26bc795e4dcd420865c42 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Sun, 3 Sep 2023 13:22:36 -0400
Subject: [PATCH 06/13] WildCat/ZeroGroupoid and EquivGpd: show that the defns
 are logically equivalent

---
 theories/WildCat/EquivGpd.v     |  2 +-
 theories/WildCat/ZeroGroupoid.v | 41 ++++++++++++++++++++++++++++++++-
 2 files changed, 41 insertions(+), 2 deletions(-)

diff --git a/theories/WildCat/EquivGpd.v b/theories/WildCat/EquivGpd.v
index 67fa677c2f4..c108fe36972 100644
--- a/theories/WildCat/EquivGpd.v
+++ b/theories/WildCat/EquivGpd.v
@@ -7,7 +7,7 @@ Require Import WildCat.Sigma.
 
 (** * Equivalences of 0-groupoids, and split essentially surjective functors *)
 
-(** For an alternate definition of equivalences of 0-groupoids, see ZeroGroupoid.v. *)
+(** For a logically equivalent definition of equivalences of 0-groupoids, see ZeroGroupoid.v. *)
 
 (** We could define these similarly for more general categories too, but we'd need to use [HasEquivs] and [$<~>] instead of [$==]. *)
 
diff --git a/theories/WildCat/ZeroGroupoid.v b/theories/WildCat/ZeroGroupoid.v
index 497622ff922..260ba21adfe 100644
--- a/theories/WildCat/ZeroGroupoid.v
+++ b/theories/WildCat/ZeroGroupoid.v
@@ -79,7 +79,7 @@ Proof.
   - reflexivity.
 Defined.
 
-(** We define equivalences of 0-groupoids.  Note that this differs from [IsEquiv0Gpd] in [EquivGpd.v].  It is chosen to provide what is needed for the Yoneda lemma, and to match the concept for types, with paths replaced by 1-cells.  We are able to match the biinvertible definition.  The half-adjoint definition doesn't work, as we can prove adjointification.  We would need to be in a 1-groupoid for that to be possible.  We could also use the "wrong" definition, without the eisadj condition, and things would go through, but it wouldn't match the definition for types. *)
+(** We define equivalences of 0-groupoids.  The definition is chosen to provide what is needed for the Yoneda lemma, and to match the concept for types, with paths replaced by 1-cells.  We are able to match the biinvertible definition.  The half-adjoint definition doesn't work, as we can't prove adjointification.  We would need to be in a 1-groupoid for that to be possible.  We could also use the "wrong" definition, without the eisadj condition, and things would go through, but it wouldn't match the definition for types. *)
 Class ZeroGpdIsEquiv {G H : ZeroGpd} (f : G $-> H) := {
   zerogpd_equiv_inv : H $-> G;
   zerogpd_eisretr : f $o zerogpd_equiv_inv $== Id H;
@@ -129,3 +129,42 @@ Proof.
     exact (Build_ZeroGpdIsEquiv _ _ f g r g s).
 Defined.
 
+(* In fact, being an equivalence in the sense above is logically equivalent to being an equivalence in the sense of EquivGpd. *)
+
+(* This is just a rough draft showing this.  Some further work is required to reorganize this. *)
+
+Require Import WildCat.EquivGpd.
+
+Definition IsEquiv0Gpd_ZeroGpdEquiv {G H : ZeroGpd} (f : G $<~> H)
+  : IsEquiv0Gpd f.
+Proof.
+  econstructor.
+  - intro y.
+    exists (f^-1$ y).
+    rapply zerogpd_eisretr.
+  - intros x1 x2 m.
+    refine ((zerogpd_eissect f x1)^$ $@ _ $@ zerogpd_eissect f x2).
+    exact (fmap f^-1$ m).
+Defined.
+
+Definition ZeroGpdEquiv_IsEquiv0Gpd {G H : ZeroGpd} (f : G -> H) `{!Is0Functor f}
+  (e : IsEquiv0Gpd f)
+  : G $<~> H.
+Proof.
+  destruct e as [e0 e1]; unfold SplEssSurj in e0.
+  snrapply cate_adjointify.
+  - exact (Build_ZeroGpdMorphism _ _ f _).
+  - snrapply Build_ZeroGpdMorphism.
+    1: exact (fun y => (e0 y).1).
+    snrapply Build_Is0Functor; cbn beta.
+    intros y1 y2 m.
+    apply e1.
+    exact ((e0 y1).2 $@ m $@ ((e0 y2).2)^$).
+  - cbn.
+    intro y.
+    apply e0.
+  - cbn.
+    intro x.
+    apply e1.
+    apply e0.
+Defined.

From 2569d62a894aa3459a46421cbda5aa5de00bb062 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Mon, 4 Sep 2023 13:14:00 -0400
Subject: [PATCH 07/13] WildCat/ZeroGroupoid and Yoneda: change naming
 convention

---
 theories/WildCat/Yoneda.v       | 14 ++---
 theories/WildCat/ZeroGroupoid.v | 91 ++++++++++++++++-----------------
 2 files changed, 52 insertions(+), 53 deletions(-)

diff --git a/theories/WildCat/Yoneda.v b/theories/WildCat/Yoneda.v
index 546829111e2..0f846c18955 100644
--- a/theories/WildCat/Yoneda.v
+++ b/theories/WildCat/Yoneda.v
@@ -172,7 +172,7 @@ Proof.
     rapply (Build_ZeroGpd (opyon a b)).
   - snrapply Build_Is0Functor.
     intros b c f; cbn beta.
-    snrapply Build_ZeroGpdMorphism; cbn.
+    snrapply Build_Morphism_0Gpd; cbn.
     + exact (fmap (opyon a) f).
     + apply is0functor_postcomp.
 Defined.
@@ -187,15 +187,15 @@ Proof.
   - pose proof (gn := is1natural_natequiv _ _ g).
     refine ((isnat (alnat:=gn) g (f a (Id a)) (Id b))^$ $@ _).
     refine (fmap (g a) (cat_idr (f a (Id a))) $@ _).
-    1: rapply is0functor_zerogpd_fun.
+    1: rapply is0functor_fun_0gpd.
     1: exact _.
-    rapply zerogpd_eissect.
+    rapply eissect_0gpd.
   - pose proof (fn := is1natural_natequiv _ _ f).
     refine ((isnat (alnat:=fn) f (g b (Id b)) (Id a))^$ $@ _).
     refine (fmap (f b) (cat_idr (g b (Id b))) $@ _).
-    1: rapply is0functor_zerogpd_fun.
+    1: rapply is0functor_fun_0gpd.
     1: exact _.
-    rapply zerogpd_eisretr.
+    rapply eisretr_0gpd.
   (* Not sure why typeclass inference doesn't find [is1natural_natequiv] and [is0functor_zerogpd_fun] above. *)
 Defined.
 
@@ -205,10 +205,10 @@ Definition equiv_precompose_cat_equiv_0gpd {A : Type} `{HasEquivs A}
   : opyon_0gpd y z $<~> opyon_0gpd x z.
 Proof.
   snrapply cate_adjointify.
-  - snrapply Build_ZeroGpdMorphism.
+  - snrapply Build_Morphism_0Gpd.
     1: exact (cat_precomp z f).
     exact _.
-  - snrapply Build_ZeroGpdMorphism.
+  - snrapply Build_Morphism_0Gpd.
     1: exact (cat_precomp z f^-1$).
     exact _.
   - cbn.
diff --git a/theories/WildCat/ZeroGroupoid.v b/theories/WildCat/ZeroGroupoid.v
index 260ba21adfe..ad412581726 100644
--- a/theories/WildCat/ZeroGroupoid.v
+++ b/theories/WildCat/ZeroGroupoid.v
@@ -16,34 +16,35 @@ Global Existing Instance isgraph_carrier.
 Global Existing Instance is01cat_carrier.
 Global Existing Instance is0gpd_carrier.
 
-Record ZeroGpdMorphism (G H : ZeroGpd) := {
-  zerogpd_fun :> carrier G -> carrier H;
-  is0functor_zerogpd_fun : Is0Functor zerogpd_fun;
+Record Morphism_0Gpd (G H : ZeroGpd) := {
+  fun_0gpd :> carrier G -> carrier H;
+  is0functor_fun_0gpd : Is0Functor fun_0gpd;
 }.
 
-Global Existing Instance is0functor_zerogpd_fun.
+Global Existing Instance is0functor_fun_0gpd.
 
+(** Now we show that the type [ZeroGpd] of 0-groupoids is itself a 1-category. *)
 Global Instance isgraph_0gpd : IsGraph ZeroGpd.
 Proof.
   apply Build_IsGraph.
-  exact ZeroGpdMorphism.
+  exact Morphism_0Gpd.
 Defined.
 
 Global Instance is01cat_0gpd : Is01Cat ZeroGpd.
 Proof.
   srapply Build_Is01Cat.
   - intro G.
-    snrapply Build_ZeroGpdMorphism.
+    snrapply Build_Morphism_0Gpd.
     1: exact idmap.
     snrapply Build_Is0Functor.
     intros g1 g2.
     exact idmap.
   - intros G H K f g.
-    snrapply Build_ZeroGpdMorphism.
+    snrapply Build_Morphism_0Gpd.
     1: exact (f o g).
     snrapply Build_Is0Functor; cbn beta.
     intros g1 g2 p.
-    apply is0functor_zerogpd_fun, is0functor_zerogpd_fun, p.
+    apply is0functor_fun_0gpd, is0functor_fun_0gpd, p.
 Defined.
 
 Global Instance is2graph_0gpd : Is2Graph ZeroGpd.
@@ -80,53 +81,53 @@ Proof.
 Defined.
 
 (** We define equivalences of 0-groupoids.  The definition is chosen to provide what is needed for the Yoneda lemma, and to match the concept for types, with paths replaced by 1-cells.  We are able to match the biinvertible definition.  The half-adjoint definition doesn't work, as we can't prove adjointification.  We would need to be in a 1-groupoid for that to be possible.  We could also use the "wrong" definition, without the eisadj condition, and things would go through, but it wouldn't match the definition for types. *)
-Class ZeroGpdIsEquiv {G H : ZeroGpd} (f : G $-> H) := {
-  zerogpd_equiv_inv : H $-> G;
-  zerogpd_eisretr : f $o zerogpd_equiv_inv $== Id H;
-  zerogpd_equiv_inv' : H $-> G;
-  zerogpd_eissect' : zerogpd_equiv_inv' $o f $== Id G;
+Class IsEquiv_0Gpd {G H : ZeroGpd} (f : G $-> H) := {
+  equiv_inv_0gpd : H $-> G;
+  eisretr_0gpd : f $o equiv_inv_0gpd $== Id H;
+  equiv_inv_0gpd' : H $-> G;
+  eissect_0gpd' : equiv_inv_0gpd' $o f $== Id G;
 }.
 
-Arguments zerogpd_equiv_inv {G H}%type_scope f {_}.
-Arguments zerogpd_eisretr {G H}%type_scope f {_} _.
-Arguments zerogpd_equiv_inv' {G H}%type_scope f {_}.
-Arguments zerogpd_eissect' {G H}%type_scope f {_} _.
+Arguments equiv_inv_0gpd {G H}%type_scope f {_}.
+Arguments eisretr_0gpd {G H}%type_scope f {_} _.
+Arguments equiv_inv_0gpd' {G H}%type_scope f {_}.
+Arguments eissect_0gpd' {G H}%type_scope f {_} _.
 
-Definition zerogpd_inverses_homotopic {G H : ZeroGpd} (f : G $-> H) `{ZeroGpdIsEquiv _ _ f}
-  : zerogpd_equiv_inv f $== zerogpd_equiv_inv' f.
+Definition inverses_homotopic_0gpd {G H : ZeroGpd} (f : G $-> H) `{IsEquiv_0Gpd _ _ f}
+  : equiv_inv_0gpd f $== equiv_inv_0gpd' f.
 Proof.
-  set (g := zerogpd_equiv_inv f).
-  set (g' := zerogpd_equiv_inv' f).
+  set (g := equiv_inv_0gpd f).
+  set (g' := equiv_inv_0gpd' f).
   intro x.
-  refine ((zerogpd_eissect' f (g x))^$ $@ _); cbn.
+  refine ((eissect_0gpd' f (g x))^$ $@ _); cbn.
   refine (fmap g' _).
-  rapply zerogpd_eisretr.
+  rapply eisretr_0gpd.
 Defined.
 
-Definition zerogpd_eissect {G H : ZeroGpd} (f : G $-> H) `{ZeroGpdIsEquiv _ _ f}
-  : zerogpd_equiv_inv f $o f $== Id G
-  := (zerogpd_inverses_homotopic f $@R f) $@ zerogpd_eissect' f.
+Definition eissect_0gpd {G H : ZeroGpd} (f : G $-> H) `{IsEquiv_0Gpd _ _ f}
+  : equiv_inv_0gpd f $o f $== Id G
+  := (inverses_homotopic_0gpd f $@R f) $@ eissect_0gpd' f.
 
-Record ZeroGpdEquiv (G H : ZeroGpd) := {
-  zerogpd_equiv_fun :> ZeroGpdMorphism G H;
-  zerogpd_isequiv_equiv : ZeroGpdIsEquiv zerogpd_equiv_fun;
+Record Equiv_0Gpd (G H : ZeroGpd) := {
+  equiv_fun_0gpd :> Morphism_0Gpd G H;
+  isequiv_equiv_0gpd : IsEquiv_0Gpd equiv_fun_0gpd;
 }.
 
-Global Instance hasequivs_zerogpd : HasEquivs ZeroGpd.
+Global Instance hasequivs_0gpd : HasEquivs ZeroGpd.
 Proof.
   srapply Build_HasEquivs; intros G H.
-  1: exact (ZeroGpdEquiv G H).
+  1: exact (Equiv_0Gpd G H).
   all:intros f.
-  - exact (ZeroGpdIsEquiv f).
+  - exact (IsEquiv_0Gpd f).
   - exact f.
-  - cbn. exact (zerogpd_isequiv_equiv _ _ f).
-  - apply Build_ZeroGpdEquiv.
+  - cbn. exact (isequiv_equiv_0gpd _ _ f).
+  - apply Build_Equiv_0Gpd.
   - intros; reflexivity.
-  - exact (@zerogpd_equiv_inv _ _ f (zerogpd_isequiv_equiv _ _ f)).
-  - cbn. apply zerogpd_eissect.
-  - cbn. apply zerogpd_eisretr.
+  - exact (@equiv_inv_0gpd _ _ f (isequiv_equiv_0gpd _ _ f)).
+  - cbn. apply eissect_0gpd.
+  - cbn. apply eisretr_0gpd.
   - intros g r s; cbn beta.
-    exact (Build_ZeroGpdIsEquiv _ _ f g r g s).
+    exact (Build_IsEquiv_0Gpd _ _ f g r g s).
 Defined.
 
 (* In fact, being an equivalence in the sense above is logically equivalent to being an equivalence in the sense of EquivGpd. *)
@@ -135,33 +136,31 @@ Defined.
 
 Require Import WildCat.EquivGpd.
 
-Definition IsEquiv0Gpd_ZeroGpdEquiv {G H : ZeroGpd} (f : G $<~> H)
+Definition IsEquiv0Gpd_Equiv_0Gpd {G H : ZeroGpd} (f : G $<~> H)
   : IsEquiv0Gpd f.
 Proof.
   econstructor.
   - intro y.
     exists (f^-1$ y).
-    rapply zerogpd_eisretr.
+    rapply eisretr_0gpd.
   - intros x1 x2 m.
-    refine ((zerogpd_eissect f x1)^$ $@ _ $@ zerogpd_eissect f x2).
-    exact (fmap f^-1$ m).
+    exact ((eissect_0gpd f x1)^$ $@ fmap f^-1$ m $@ eissect_0gpd f x2).
 Defined.
 
-Definition ZeroGpdEquiv_IsEquiv0Gpd {G H : ZeroGpd} (f : G -> H) `{!Is0Functor f}
+Definition Equiv_0Gpd_IsEquiv0Gpd {G H : ZeroGpd} (f : G -> H) `{!Is0Functor f}
   (e : IsEquiv0Gpd f)
   : G $<~> H.
 Proof.
   destruct e as [e0 e1]; unfold SplEssSurj in e0.
   snrapply cate_adjointify.
-  - exact (Build_ZeroGpdMorphism _ _ f _).
-  - snrapply Build_ZeroGpdMorphism.
+  - exact (Build_Morphism_0Gpd _ _ f _).
+  - snrapply Build_Morphism_0Gpd.
     1: exact (fun y => (e0 y).1).
     snrapply Build_Is0Functor; cbn beta.
     intros y1 y2 m.
     apply e1.
     exact ((e0 y1).2 $@ m $@ ((e0 y2).2)^$).
   - cbn.
-    intro y.
     apply e0.
   - cbn.
     intro x.

From 07c8b168b65896b6e0b2c82c25857887bcbe8fb1 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Mon, 4 Sep 2023 13:54:02 -0400
Subject: [PATCH 08/13] WildCat/Yoneda and ZeroGroupoid: update comments,
 simplify some proofs

---
 theories/WildCat/Yoneda.v       |  2 +-
 theories/WildCat/ZeroGroupoid.v | 54 +++++++++++++++------------------
 2 files changed, 26 insertions(+), 30 deletions(-)

diff --git a/theories/WildCat/Yoneda.v b/theories/WildCat/Yoneda.v
index 0f846c18955..0812a438238 100644
--- a/theories/WildCat/Yoneda.v
+++ b/theories/WildCat/Yoneda.v
@@ -164,7 +164,7 @@ Proof.
   - rapply is1natural_opyoneda.
 Defined.
 
-(** We define a version of [opyon] that lands in 0-groupoids, which we regard as setoids. *)
+(** We define a version of [opyon] that lands in 0-groupoids. *)
 Definition opyon_0gpd {A : Type} `{Is1Cat A} (a : A) : Fun01 A ZeroGpd.
 Proof.
   snrapply Build_Fun01.
diff --git a/theories/WildCat/ZeroGroupoid.v b/theories/WildCat/ZeroGroupoid.v
index ad412581726..2f4a6bcea82 100644
--- a/theories/WildCat/ZeroGroupoid.v
+++ b/theories/WildCat/ZeroGroupoid.v
@@ -16,6 +16,7 @@ Global Existing Instance isgraph_carrier.
 Global Existing Instance is01cat_carrier.
 Global Existing Instance is0gpd_carrier.
 
+(* The morphisms of 0-groupoids are the 0-functors.  This is the same as [Fun01], but we put a different graph and 01-category structure on it, so we give this a custom name. *)
 Record Morphism_0Gpd (G H : ZeroGpd) := {
   fun_0gpd :> carrier G -> carrier H;
   is0functor_fun_0gpd : Is0Functor fun_0gpd;
@@ -23,7 +24,7 @@ Record Morphism_0Gpd (G H : ZeroGpd) := {
 
 Global Existing Instance is0functor_fun_0gpd.
 
-(** Now we show that the type [ZeroGpd] of 0-groupoids is itself a 1-category. *)
+(** Now we show that the type [ZeroGpd] of 0-groupoids is itself a 1-category, with morphisms the 0-functors. *)
 Global Instance isgraph_0gpd : IsGraph ZeroGpd.
 Proof.
   apply Build_IsGraph.
@@ -34,19 +35,12 @@ Global Instance is01cat_0gpd : Is01Cat ZeroGpd.
 Proof.
   srapply Build_Is01Cat.
   - intro G.
-    snrapply Build_Morphism_0Gpd.
-    1: exact idmap.
-    snrapply Build_Is0Functor.
-    intros g1 g2.
-    exact idmap.
+    exact (Build_Morphism_0Gpd G G idmap _).
   - intros G H K f g.
-    snrapply Build_Morphism_0Gpd.
-    1: exact (f o g).
-    snrapply Build_Is0Functor; cbn beta.
-    intros g1 g2 p.
-    apply is0functor_fun_0gpd, is0functor_fun_0gpd, p.
+    exact (Build_Morphism_0Gpd _ _ (f o g) _).
 Defined.
 
+(* The 2-cells are unnatural transformations, and are analogous to homotopies. *)
 Global Instance is2graph_0gpd : Is2Graph ZeroGpd.
 Proof.
   intros G H.
@@ -75,9 +69,9 @@ Proof.
     intros g h p x.
     cbn.
     exact (p (f x)).
-  - reflexivity.
-  - reflexivity.
-  - reflexivity.
+  - reflexivity. (* Associativity. *)
+  - reflexivity. (* Left identity. *)
+  - reflexivity. (* Right identity. *)
 Defined.
 
 (** We define equivalences of 0-groupoids.  The definition is chosen to provide what is needed for the Yoneda lemma, and to match the concept for types, with paths replaced by 1-cells.  We are able to match the biinvertible definition.  The half-adjoint definition doesn't work, as we can't prove adjointification.  We would need to be in a 1-groupoid for that to be possible.  We could also use the "wrong" definition, without the eisadj condition, and things would go through, but it wouldn't match the definition for types. *)
@@ -93,6 +87,14 @@ Arguments eisretr_0gpd {G H}%type_scope f {_} _.
 Arguments equiv_inv_0gpd' {G H}%type_scope f {_}.
 Arguments eissect_0gpd' {G H}%type_scope f {_} _.
 
+Record Equiv_0Gpd (G H : ZeroGpd) := {
+  equiv_fun_0gpd :> Morphism_0Gpd G H;
+  equiv_isequiv_0gpd : IsEquiv_0Gpd equiv_fun_0gpd;
+}.
+
+Global Existing Instance equiv_isequiv_0gpd.
+
+(** The two inverses are necessarily homotopic. *)
 Definition inverses_homotopic_0gpd {G H : ZeroGpd} (f : G $-> H) `{IsEquiv_0Gpd _ _ f}
   : equiv_inv_0gpd f $== equiv_inv_0gpd' f.
 Proof.
@@ -104,29 +106,25 @@ Proof.
   rapply eisretr_0gpd.
 Defined.
 
+(** Therefore we can prove [eissect] for the first inverse as well. *)
 Definition eissect_0gpd {G H : ZeroGpd} (f : G $-> H) `{IsEquiv_0Gpd _ _ f}
   : equiv_inv_0gpd f $o f $== Id G
   := (inverses_homotopic_0gpd f $@R f) $@ eissect_0gpd' f.
 
-Record Equiv_0Gpd (G H : ZeroGpd) := {
-  equiv_fun_0gpd :> Morphism_0Gpd G H;
-  isequiv_equiv_0gpd : IsEquiv_0Gpd equiv_fun_0gpd;
-}.
-
 Global Instance hasequivs_0gpd : HasEquivs ZeroGpd.
 Proof.
   srapply Build_HasEquivs; intros G H.
   1: exact (Equiv_0Gpd G H).
-  all:intros f.
+  all:intros f; cbn beta in *.
   - exact (IsEquiv_0Gpd f).
   - exact f.
-  - cbn. exact (isequiv_equiv_0gpd _ _ f).
+  - exact _.
   - apply Build_Equiv_0Gpd.
   - intros; reflexivity.
-  - exact (@equiv_inv_0gpd _ _ f (isequiv_equiv_0gpd _ _ f)).
-  - cbn. apply eissect_0gpd.
-  - cbn. apply eisretr_0gpd.
-  - intros g r s; cbn beta.
+  - exact (equiv_inv_0gpd f).
+  - apply eissect_0gpd.
+  - apply eisretr_0gpd.
+  - intros g r s.
     exact (Build_IsEquiv_0Gpd _ _ f g r g s).
 Defined.
 
@@ -160,10 +158,8 @@ Proof.
     intros y1 y2 m.
     apply e1.
     exact ((e0 y1).2 $@ m $@ ((e0 y2).2)^$).
-  - cbn.
-    apply e0.
-  - cbn.
-    intro x.
+  - cbn.  apply e0.
+  - cbn.  intro x.
     apply e1.
     apply e0.
 Defined.

From 8341715896a676456f36145f4cb9eb9533ad4502 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Mon, 4 Sep 2023 17:42:43 -0400
Subject: [PATCH 09/13] WildCat/ZeroGroupoid: minor cleanups, mainly to
 comments

---
 theories/WildCat/EquivGpd.v     |  2 ++
 theories/WildCat/ZeroGroupoid.v | 19 +++++++++----------
 2 files changed, 11 insertions(+), 10 deletions(-)

diff --git a/theories/WildCat/EquivGpd.v b/theories/WildCat/EquivGpd.v
index c108fe36972..490dc2789bd 100644
--- a/theories/WildCat/EquivGpd.v
+++ b/theories/WildCat/EquivGpd.v
@@ -31,6 +31,8 @@ Arguments essinj0 {A B _ _ _ _ _ _} F {_ _ x y} f.
 Definition equiv0gpd_inv {A B : Type} (F : A -> B) `{IsEquiv0Gpd A B F} : B -> A
   := fun b => (esssurj F b).1.
 
+(** Some of the results below also follow from the logical equivalence with [IsEquiv_0Gpd] and the fact that [ZeroGpd] satisfies [HasEquivs].  But it is sometimes awkward to deduce the results this way, mostly because [ZeroGpd] requires bundled objects rather than typeclass instances. *)
+
 (** Equivalences have inverses *)
 
 Global Instance is0functor_equiv0gpd_inv
diff --git a/theories/WildCat/ZeroGroupoid.v b/theories/WildCat/ZeroGroupoid.v
index 2f4a6bcea82..92a94401b76 100644
--- a/theories/WildCat/ZeroGroupoid.v
+++ b/theories/WildCat/ZeroGroupoid.v
@@ -1,5 +1,5 @@
 Require Import Basics.Overture Basics.Tactics.
-Require Import WildCat.Core WildCat.Equiv.
+Require Import WildCat.Core WildCat.Equiv WildCat.EquivGpd.
 
 (** * The wild 1-category of 0-groupoids. *)
 
@@ -128,12 +128,11 @@ Proof.
     exact (Build_IsEquiv_0Gpd _ _ f g r g s).
 Defined.
 
-(* In fact, being an equivalence in the sense above is logically equivalent to being an equivalence in the sense of EquivGpd. *)
+(** * We now give a different characterization of the equivalences of 0-groupoids, as the injective split essentially surjective 0-functors which are defined in EquivGpd. *)
 
-(* This is just a rough draft showing this.  Some further work is required to reorganize this. *)
-
-Require Import WildCat.EquivGpd.
+(** Advantages of this logically equivalent formulation are that it tends to be easier to prove in examples and in some cases it is definitionally equal to [ExtensionAlong], which is convenient.  See Homotopy/Suspension.v and Algebra/AbGroups/Abelianization for examples. Advantages of the bi-invertible definition are that it reproduces a definition that is equivalent to [IsEquiv] when applied to types, assuming [Funext].  It also makes the proof of [HasEquivs] above easy. *)
 
+(** Every equivalence is injective and essentially surjective. *)
 Definition IsEquiv0Gpd_Equiv_0Gpd {G H : ZeroGpd} (f : G $<~> H)
   : IsEquiv0Gpd f.
 Proof.
@@ -145,13 +144,13 @@ Proof.
     exact ((eissect_0gpd f x1)^$ $@ fmap f^-1$ m $@ eissect_0gpd f x2).
 Defined.
 
-Definition Equiv_0Gpd_IsEquiv0Gpd {G H : ZeroGpd} (f : G -> H) `{!Is0Functor f}
-  (e : IsEquiv0Gpd f)
-  : G $<~> H.
+(** Conversely, every injective essentially surjective 0-functor is an equivalence. *)
+Global Instance IsEquiv_0Gpd_IsEquiv0Gpd {G H : ZeroGpd} (F : G $-> H)
+  {e : IsEquiv0Gpd F}
+  : IsEquiv_0Gpd F.
 Proof.
   destruct e as [e0 e1]; unfold SplEssSurj in e0.
-  snrapply cate_adjointify.
-  - exact (Build_Morphism_0Gpd _ _ f _).
+  srapply catie_adjointify.
   - snrapply Build_Morphism_0Gpd.
     1: exact (fun y => (e0 y).1).
     snrapply Build_Is0Functor; cbn beta.

From 40c644190d9d08d5cc154c8e73140aad36afb603 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Mon, 4 Sep 2023 18:28:23 -0400
Subject: [PATCH 10/13] WildCat/ZeroGroupoid: add "split" before "essentially
 surjective"

---
 theories/WildCat/ZeroGroupoid.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/WildCat/ZeroGroupoid.v b/theories/WildCat/ZeroGroupoid.v
index 92a94401b76..6277016dc6d 100644
--- a/theories/WildCat/ZeroGroupoid.v
+++ b/theories/WildCat/ZeroGroupoid.v
@@ -132,7 +132,7 @@ Defined.
 
 (** Advantages of this logically equivalent formulation are that it tends to be easier to prove in examples and in some cases it is definitionally equal to [ExtensionAlong], which is convenient.  See Homotopy/Suspension.v and Algebra/AbGroups/Abelianization for examples. Advantages of the bi-invertible definition are that it reproduces a definition that is equivalent to [IsEquiv] when applied to types, assuming [Funext].  It also makes the proof of [HasEquivs] above easy. *)
 
-(** Every equivalence is injective and essentially surjective. *)
+(** Every equivalence is injective and split essentially surjective. *)
 Definition IsEquiv0Gpd_Equiv_0Gpd {G H : ZeroGpd} (f : G $<~> H)
   : IsEquiv0Gpd f.
 Proof.
@@ -144,7 +144,7 @@ Proof.
     exact ((eissect_0gpd f x1)^$ $@ fmap f^-1$ m $@ eissect_0gpd f x2).
 Defined.
 
-(** Conversely, every injective essentially surjective 0-functor is an equivalence. *)
+(** Conversely, every injective split essentially surjective 0-functor is an equivalence. *)
 Global Instance IsEquiv_0Gpd_IsEquiv0Gpd {G H : ZeroGpd} (F : G $-> H)
   {e : IsEquiv0Gpd F}
   : IsEquiv_0Gpd F.

From 7367f8acaf1d50dfcf54171b14e379b90ce8ead8 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Tue, 5 Sep 2023 19:20:43 -0400
Subject: [PATCH 11/13] WildCat/EquivGpd + dependencies: use IsSurjInj and
 similar naming

---
 theories/Algebra/AbGroups/Abelianization.v |  10 +-
 theories/Homotopy/Suspension.v             |   8 +-
 theories/WildCat/EquivGpd.v                | 106 ++++++++++-----------
 theories/WildCat/ZeroGroupoid.v            |   8 +-
 4 files changed, 66 insertions(+), 66 deletions(-)

diff --git a/theories/Algebra/AbGroups/Abelianization.v b/theories/Algebra/AbGroups/Abelianization.v
index 203d1b82270..44374d03c85 100644
--- a/theories/Algebra/AbGroups/Abelianization.v
+++ b/theories/Algebra/AbGroups/Abelianization.v
@@ -18,7 +18,7 @@ Definition group_precomp {a b} := @cat_precomp Group _ _ a b.
 Class IsAbelianization {G : Group} (G_ab : AbGroup)
       (eta : GroupHomomorphism G G_ab)
   := isequiv0gpd_isabel : forall (A : AbGroup),
-      IsEquiv0Gpd (group_precomp A eta).
+      IsSurjInj (group_precomp A eta).
 Global Existing Instance isequiv0gpd_isabel.
 
 (** Here we define abelianization as a HIT. Specifically as a set-coequalizer of the following two maps: (a, b, c) |-> a (b c) and (a, b, c) |-> a (c b).
@@ -323,13 +323,13 @@ Proof.
   destruct (esssurj (group_precomp A eta2) eta1) as [b bc].
   srapply (Build_GroupIsomorphism _ _ a).
   srapply (isequiv_adjointify _ b).
-  { refine (essinj0 (group_precomp B eta2)
-                    (x := a $o b) (y := Id (A := Group) B) _).
+  { refine (essinj (group_precomp B eta2)
+                   (x := a $o b) (y := Id (A := Group) B) _).
     intros x; cbn in *.
     refine (_ @ ac x).
     apply ap, bc. }
-  { refine (essinj0 (group_precomp A eta1)
-                    (x := b $o a) (y := Id (A := Group) A) _).
+  { refine (essinj (group_precomp A eta1)
+                   (x := b $o a) (y := Id (A := Group) A) _).
     intros x; cbn in *.
     refine (_ @ bc x).
     apply ap, ac. }
diff --git a/theories/Homotopy/Suspension.v b/theories/Homotopy/Suspension.v
index a0143603bee..dfc485b8f7e 100644
--- a/theories/Homotopy/Suspension.v
+++ b/theories/Homotopy/Suspension.v
@@ -249,7 +249,7 @@ Section UnivProp.
   Defined.
 
   (** And now we can prove that it's an equivalence. *)
-  Definition equiv0gpd_Susp_ind_inv : IsEquiv0Gpd Susp_ind_inv.
+  Definition issurjinj_Susp_ind_inv : IsSurjInj Susp_ind_inv.
   Proof.
     constructor.
     - intros [[n s] g].
@@ -336,8 +336,8 @@ Section UnivPropNat.
   Defined.
 
   (** And therefore a fiberwise equivalence of 0-groupoids. *)
-  Local Instance isequiv0gpd_functor_Susp_ind_data' NS
-    : IsEquiv0Gpd (functor_Susp_ind_data' NS).
+  Local Instance issurjinj_functor_Susp_ind_data' NS
+    : IsSurjInj (functor_Susp_ind_data' NS).
   Proof.
     constructor.
     - intros g.
@@ -402,7 +402,7 @@ Section UnivPropNat.
     { reflexivity. }
     etransitivity.
     { refine (isesssurj_iff_commsq Susp_ind_inv_nat); try exact _.
-      all:apply equiv0gpd_Susp_ind_inv. }
+      all:apply issurjinj_Susp_ind_inv. }
     etransitivity.
     { refine (isesssurj_iff_sigma _ _ 
                 (fun NS => functor_Susp_ind_data' NS o functor_Susp_ind_data'' NS)). }
diff --git a/theories/WildCat/EquivGpd.v b/theories/WildCat/EquivGpd.v
index 490dc2789bd..86a2bc0322b 100644
--- a/theories/WildCat/EquivGpd.v
+++ b/theories/WildCat/EquivGpd.v
@@ -18,49 +18,49 @@ Class SplEssSurj {A B : Type} `{Is0Gpd A, Is0Gpd B}
 Arguments esssurj {A B _ _ _ _ _ _} F {_ _} b.
 
 (** A 0-functor between 0-groupoids is an equivalence if it is essentially surjective and reflects the existence of morphisms.  This is "surjective and injective" in setoid-language.  (To define essential surjectivity for non-groupoids, we would need [HasEquivs] from [WildCat.Equiv]. *)
-Class IsEquiv0Gpd {A B : Type} `{Is0Gpd A, Is0Gpd B}
+Class IsSurjInj {A B : Type} `{Is0Gpd A, Is0Gpd B}
       (F : A -> B) `{!Is0Functor F} :=
 {
-  esssurj_isequiv0gpd : SplEssSurj F ;
-  essinj0 : forall (x y:A), (F x $== F y) -> (x $== y) ;
+  esssurj_issurjinj : SplEssSurj F ;
+  essinj : forall (x y:A), (F x $== F y) -> (x $== y) ;
 }.
 
-Global Existing Instance esssurj_isequiv0gpd.
-Arguments essinj0 {A B _ _ _ _ _ _} F {_ _ x y} f.
+Global Existing Instance esssurj_issurjinj.
+Arguments essinj {A B _ _ _ _ _ _} F {_ _ x y} f.
 
-Definition equiv0gpd_inv {A B : Type} (F : A -> B) `{IsEquiv0Gpd A B F} : B -> A
+Definition surjinj_inv {A B : Type} (F : A -> B) `{IsSurjInj A B F} : B -> A
   := fun b => (esssurj F b).1.
 
 (** Some of the results below also follow from the logical equivalence with [IsEquiv_0Gpd] and the fact that [ZeroGpd] satisfies [HasEquivs].  But it is sometimes awkward to deduce the results this way, mostly because [ZeroGpd] requires bundled objects rather than typeclass instances. *)
 
 (** Equivalences have inverses *)
 
-Global Instance is0functor_equiv0gpd_inv
-       {A B : Type} (F : A -> B) `{IsEquiv0Gpd A B F}
-  : Is0Functor (equiv0gpd_inv F).
+Global Instance is0functor_surjinj_inv
+       {A B : Type} (F : A -> B) `{IsSurjInj A B F}
+  : Is0Functor (surjinj_inv F).
 Proof.
   constructor; intros x y f.
   pose (p := (esssurj F x).2).
   pose (q := (esssurj F y).2).
   cbn in *.
   pose (f' := p $@ f $@ q^$).
-  exact (essinj0 F f').
+  exact (essinj F f').
 Defined.
 
 (** The inverse is an inverse, up to unnatural transformations *)
 
-Definition eisretr0gpd_inv {A B : Type} (F : A -> B) `{IsEquiv0Gpd A B F}
-  : F o equiv0gpd_inv F $=> idmap.
+Definition eisretr0gpd_inv {A B : Type} (F : A -> B) `{IsSurjInj A B F}
+  : F o surjinj_inv F $=> idmap.
 Proof.
   intros b.
   exact ((esssurj F b).2).
 Defined.
 
-Definition eissect0gpd_inv {A B : Type} (F : A -> B) `{IsEquiv0Gpd A B F}
-  : equiv0gpd_inv F o F $=> idmap.
+Definition eissect0gpd_inv {A B : Type} (F : A -> B) `{IsSurjInj A B F}
+  : surjinj_inv F o F $=> idmap.
 Proof.
   intros a.
-  apply (essinj0 F).
+  apply (essinj F).
   apply eisretr0gpd_inv.
 Defined.
 
@@ -75,14 +75,14 @@ Proof.
   apply alpha.
 Defined.
 
-Definition isequiv0gpd_transf {A B : Type} {F : A -> B} {G : A -> B}
-           `{IsEquiv0Gpd A B F} `{!Is0Functor G} (alpha : G $=> F)
-  : IsEquiv0Gpd G.
+Definition issurjinj_transf {A B : Type} {F : A -> B} {G : A -> B}
+           `{IsSurjInj A B F} `{!Is0Functor G} (alpha : G $=> F)
+  : IsSurjInj G.
 Proof.
   constructor.
   - apply (isesssurj_transf alpha).
   - intros x y f.
-    apply (essinj0 F).
+    apply (essinj F).
     refine (_ $@ f $@ _).
     + symmetry; apply alpha.
     + apply alpha.
@@ -105,47 +105,47 @@ Section ComposeAndCancel.
     apply (esssurj F).
   Defined.
 
-  Global Instance isequiv0gpd_compose
-         `{!IsEquiv0Gpd G, !IsEquiv0Gpd F}
-    : IsEquiv0Gpd (G o F).
+  Global Instance issurjinj_compose
+         `{!IsSurjInj G, !IsSurjInj F}
+    : IsSurjInj (G o F).
   Proof.
     constructor.
     - exact _.
     - intros x y f.
-      apply (essinj0 F).
-      exact (essinj0 G f).
+      apply (essinj F).
+      exact (essinj G f).
   Defined.
 
   Definition cancelL_isesssurj
-             `{!IsEquiv0Gpd G, !SplEssSurj (G o F)}
+             `{!IsSurjInj G, !SplEssSurj (G o F)}
     : SplEssSurj F.
   Proof.
     intros b.
     exists ((esssurj (G o F) (G b)).1).
-    apply (essinj0 G).
+    apply (essinj G).
     exact ((esssurj (G o F) (G b)).2).
   Defined.
 
-  Definition iffL_isesssurj `{!IsEquiv0Gpd G}
+  Definition iffL_isesssurj `{!IsSurjInj G}
     : SplEssSurj (G o F) <-> SplEssSurj F.
   Proof.
     split; [ apply @cancelL_isesssurj | apply @isesssurj_compose ]; exact _.
   Defined.
 
-  Definition cancelL_isequiv0gpd
-             `{!IsEquiv0Gpd G, !IsEquiv0Gpd (G o F)}
-    : IsEquiv0Gpd F.
+  Definition cancelL_issurjinj
+             `{!IsSurjInj G, !IsSurjInj (G o F)}
+    : IsSurjInj F.
   Proof.
     constructor.
     - apply cancelL_isesssurj.
     - intros x y f.
-      exact (essinj0 (G o F) (fmap G f)).
+      exact (essinj (G o F) (fmap G f)).
   Defined.
 
-  Definition iffL_isequiv0gpd `{!IsEquiv0Gpd G}
-    : IsEquiv0Gpd (G o F) <-> IsEquiv0Gpd F.
+  Definition iffL_issurjinj `{!IsSurjInj G}
+    : IsSurjInj (G o F) <-> IsSurjInj F.
   Proof.
-    split; [ apply @cancelL_isequiv0gpd | apply @isequiv0gpd_compose ]; exact _.
+    split; [ apply @cancelL_issurjinj | apply @issurjinj_compose ]; exact _.
   Defined.
 
   Definition cancelR_isesssurj `{!SplEssSurj (G o F)}
@@ -162,9 +162,9 @@ Section ComposeAndCancel.
     split; [ apply @cancelR_isesssurj | intros; apply @isesssurj_compose ]; exact _.
   Defined.
 
-  Definition cancelR_isequiv0gpd
-             `{!IsEquiv0Gpd F, !IsEquiv0Gpd (G o F)}
-    : IsEquiv0Gpd G.
+  Definition cancelR_issurjinj
+             `{!IsSurjInj F, !IsSurjInj (G o F)}
+    : IsSurjInj G.
   Proof.
     constructor.
     - apply cancelR_isesssurj.
@@ -174,16 +174,16 @@ Section ComposeAndCancel.
       cbn in *.
       refine (p^$ $@ _ $@ q).
       apply (fmap F).
-      apply (essinj0 (G o F)).
+      apply (essinj (G o F)).
       refine (_ $@ f $@ _).
       + exact (fmap G p).
       + exact (fmap G q^$).
   Defined.
 
-  Definition iffR_isequiv0gpd `{!IsEquiv0Gpd F}
-    : IsEquiv0Gpd (G o F) <-> IsEquiv0Gpd G.
+  Definition iffR_issurjinj `{!IsSurjInj F}
+    : IsSurjInj (G o F) <-> IsSurjInj G.
   Proof.
-    split; [ apply @cancelR_isequiv0gpd | intros; apply @isequiv0gpd_compose ]; exact _.
+    split; [ apply @cancelR_issurjinj | intros; apply @issurjinj_compose ]; exact _.
   Defined.
 
 End ComposeAndCancel.
@@ -191,7 +191,7 @@ End ComposeAndCancel.
 (** In particular, essential surjectivity and being an equivalence transfer across commutative squares of functors. *)
 Definition isesssurj_iff_commsq {A B C D : Type}
            {F : A -> B} {G : C -> D} {H : A -> C} {K : B -> D}
-           `{IsEquiv0Gpd A C H} `{IsEquiv0Gpd B D K}
+           `{IsSurjInj A C H} `{IsSurjInj B D K}
            `{!Is0Functor F} `{!Is0Functor G}
            (p : K o F $=> G o H)
   : SplEssSurj F <-> SplEssSurj G.
@@ -203,18 +203,18 @@ Proof.
     apply (isesssurj_transf p).
 Defined.
 
-Definition isequiv0gpd_iff_commsq {A B C D : Type}
+Definition issurjinj_iff_commsq {A B C D : Type}
            {F : A -> B} {G : C -> D} {H : A -> C} {K : B -> D}
-           `{IsEquiv0Gpd A C H} `{IsEquiv0Gpd B D K}
+           `{IsSurjInj A C H} `{IsSurjInj B D K}
            `{!Is0Functor F} `{!Is0Functor G}
            (p : K o F $=> G o H)
-  : IsEquiv0Gpd F <-> IsEquiv0Gpd G.
+  : IsSurjInj F <-> IsSurjInj G.
 Proof.
   split; intros ?.
-  - srapply (cancelR_isequiv0gpd G H); try exact _.
-    apply (isequiv0gpd_transf (fun a => (p a)^$)).
-  - srapply (cancelL_isequiv0gpd K F); try exact _.
-    apply (isequiv0gpd_transf p).
+  - srapply (cancelR_issurjinj G H); try exact _.
+    apply (issurjinj_transf (fun a => (p a)^$)).
+  - srapply (cancelL_issurjinj K F); try exact _.
+    apply (issurjinj_transf p).
 Defined.
 
 (** Equivalences and essential surjectivity are preserved by sigmas (for now, just over constant bases), and essential surjectivity at least is also reflected. *)
@@ -239,17 +239,17 @@ Proof.
     exact ((esssurj (F a) c).2).
 Defined.
 
-Definition isequiv0gpd_sigma {A : Type} (B C : A -> Type)
+Definition issurjinj_sigma {A : Type} (B C : A -> Type)
  `{forall a, IsGraph (B a)} `{forall a, Is01Cat (B a)} `{forall a, Is0Gpd (B a)}
  `{forall a, IsGraph (C a)} `{forall a, Is01Cat (C a)} `{forall a, Is0Gpd (C a)}
   (F : forall a, B a -> C a)
-  `{forall a, Is0Functor (F a)} `{forall a, IsEquiv0Gpd (F a)}
-  : IsEquiv0Gpd (fun (x:sig B) => (x.1 ; F x.1 x.2)).
+  `{forall a, Is0Functor (F a)} `{forall a, IsSurjInj (F a)}
+  : IsSurjInj (fun (x:sig B) => (x.1 ; F x.1 x.2)).
 Proof.
   constructor.
   - apply isesssurj_iff_sigma; exact _.
   - intros [a1 b1] [a2 b2] [p f]; cbn in *.
     destruct p; cbn in *.
     exists idpath; cbn.
-    exact (essinj0 (F a1) f).
+    exact (essinj (F a1) f).
 Defined.
diff --git a/theories/WildCat/ZeroGroupoid.v b/theories/WildCat/ZeroGroupoid.v
index 6277016dc6d..ac3876cf461 100644
--- a/theories/WildCat/ZeroGroupoid.v
+++ b/theories/WildCat/ZeroGroupoid.v
@@ -133,8 +133,8 @@ Defined.
 (** Advantages of this logically equivalent formulation are that it tends to be easier to prove in examples and in some cases it is definitionally equal to [ExtensionAlong], which is convenient.  See Homotopy/Suspension.v and Algebra/AbGroups/Abelianization for examples. Advantages of the bi-invertible definition are that it reproduces a definition that is equivalent to [IsEquiv] when applied to types, assuming [Funext].  It also makes the proof of [HasEquivs] above easy. *)
 
 (** Every equivalence is injective and split essentially surjective. *)
-Definition IsEquiv0Gpd_Equiv_0Gpd {G H : ZeroGpd} (f : G $<~> H)
-  : IsEquiv0Gpd f.
+Definition IsSurjInj_Equiv_0Gpd {G H : ZeroGpd} (f : G $<~> H)
+  : IsSurjInj f.
 Proof.
   econstructor.
   - intro y.
@@ -145,8 +145,8 @@ Proof.
 Defined.
 
 (** Conversely, every injective split essentially surjective 0-functor is an equivalence. *)
-Global Instance IsEquiv_0Gpd_IsEquiv0Gpd {G H : ZeroGpd} (F : G $-> H)
-  {e : IsEquiv0Gpd F}
+Global Instance IsEquiv_0Gpd_IsSurjInj {G H : ZeroGpd} (F : G $-> H)
+  {e : IsSurjInj F}
   : IsEquiv_0Gpd F.
 Proof.
   destruct e as [e0 e1]; unfold SplEssSurj in e0.

From 763450824eac603ef0a3f45c05e133862d9328ae Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Tue, 5 Sep 2023 19:29:49 -0400
Subject: [PATCH 12/13] WildCat/EquivGpd + dependencies: update comments as
 well

---
 theories/Algebra/AbGroups/Abelianization.v | 2 +-
 theories/Homotopy/Suspension.v             | 4 ++--
 theories/WildCat/EquivGpd.v                | 2 +-
 3 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/theories/Algebra/AbGroups/Abelianization.v b/theories/Algebra/AbGroups/Abelianization.v
index 44374d03c85..41ac5b900a7 100644
--- a/theories/Algebra/AbGroups/Abelianization.v
+++ b/theories/Algebra/AbGroups/Abelianization.v
@@ -10,7 +10,7 @@ Local Open Scope wc_iso_scope.
 
 (** Definition of Abelianization.
 
-  A "unit" homomorphism [eta : G -> G_ab], with [G_ab] abelian, is considered an abelianization if and only if for all homomorphisms [G -> A], where [A] is abelian, there exists a unique [g : G_ab -> A] such that [h == g o eta X].   We express this in funext-free form by saying that precomposition with [eta] in the wild 1-category [Group] induces an equivalence of hom 0-groupoids.
+  A "unit" homomorphism [eta : G -> G_ab], with [G_ab] abelian, is considered an abelianization if and only if for all homomorphisms [G -> A], where [A] is abelian, there exists a unique [g : G_ab -> A] such that [h == g o eta X].   We express this in funext-free form by saying that precomposition with [eta] in the wild 1-category [Group] induces an equivalence of hom 0-groupoids, in the sense of WildCat/EquivGpd.
 
   Unfortunately, if [eta : GroupHomomorphism G G_ab] and we write [cat_precomp A eta] then Coq is unable to guess that the relevant 1-category is [Group].  Even writing [cat_precomp (A := Group) A eta] isn't good enough, I guess because the typeclass inference that finds the instance [is01cat_group] doesn't happen until after the type of [eta] would have to be resolved to a [Hom] in some wild category.  However, with the following auxiliary definition we can force the typeclass inference to happen first.  (It would be worth thinking about whether the design of the wild categories library could be improved to avoid this.)  *)
 Definition group_precomp {a b} := @cat_precomp Group _ _ a b.
diff --git a/theories/Homotopy/Suspension.v b/theories/Homotopy/Suspension.v
index dfc485b8f7e..53fda42df6f 100644
--- a/theories/Homotopy/Suspension.v
+++ b/theories/Homotopy/Suspension.v
@@ -248,7 +248,7 @@ Section UnivProp.
       exact (dp_apD_nat p (merid x)).
   Defined.
 
-  (** And now we can prove that it's an equivalence. *)
+  (** And now we can prove that it's an equivalence of 0-groupoids, using the definition from WildCat/EquivGpd. *)
   Definition issurjinj_Susp_ind_inv : IsSurjInj Susp_ind_inv.
   Proof.
     constructor.
@@ -423,7 +423,7 @@ Definition extendable_iff_functor_susp
     <-> (forall NS, ExtendableAlong n f (fun x => DPath P (merid x) (fst NS) (snd NS))).
 Proof.
   revert P. induction n as [|n IHn]; intros P; [ split; intros; exact tt | ].
-  (** It would be nice to be able to do this proof by chaining logcal equivalences too, especially since the two parts seem very similar.  But I haven't managed to make that work. *)
+  (** It would be nice to be able to do this proof by chaining logical equivalences too, especially since the two parts seem very similar.  But I haven't managed to make that work. *)
   split.
   - intros [e1 en] [N S]; split.
     + apply extension_iff_functor_susp.
diff --git a/theories/WildCat/EquivGpd.v b/theories/WildCat/EquivGpd.v
index 86a2bc0322b..11dbc347be6 100644
--- a/theories/WildCat/EquivGpd.v
+++ b/theories/WildCat/EquivGpd.v
@@ -17,7 +17,7 @@ Class SplEssSurj {A B : Type} `{Is0Gpd A, Is0Gpd B}
 
 Arguments esssurj {A B _ _ _ _ _ _} F {_ _} b.
 
-(** A 0-functor between 0-groupoids is an equivalence if it is essentially surjective and reflects the existence of morphisms.  This is "surjective and injective" in setoid-language.  (To define essential surjectivity for non-groupoids, we would need [HasEquivs] from [WildCat.Equiv]. *)
+(** A 0-functor between 0-groupoids is an "equivalence" if it is essentially surjective and reflects the existence of morphisms.  This is "surjective and injective" in setoid-language, so we use the name [IsSurjInj].  (To define essential surjectivity for non-groupoids, we would need [HasEquivs] from [WildCat.Equiv]. *)
 Class IsSurjInj {A B : Type} `{Is0Gpd A, Is0Gpd B}
       (F : A -> B) `{!Is0Functor F} :=
 {

From c374bf4c1c4aba313213e5eabde2d8e78ec65fdd Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Mon, 11 Sep 2023 16:16:41 -0400
Subject: [PATCH 13/13] WildCat: define HasEquivs for any 1-category, and use
 it for ZeroGpd

---
 theories/WildCat/Equiv.v        | 61 +++++++++++++++++++++++++++-
 theories/WildCat/Yoneda.v       | 23 ++++++-----
 theories/WildCat/ZeroGroupoid.v | 71 +++++++--------------------------
 3 files changed, 88 insertions(+), 67 deletions(-)

diff --git a/theories/WildCat/Equiv.v b/theories/WildCat/Equiv.v
index f146f458449..9c53a6dc556 100644
--- a/theories/WildCat/Equiv.v
+++ b/theories/WildCat/Equiv.v
@@ -8,7 +8,7 @@ Declare Scope wc_iso_scope.
 
 (** * Equivalences in wild categories *)
 
-(** We could define equivalences in any wild 2-category as bi-invertible maps, or in a wild 3-category as half-adjoint equivalences.  However, in concrete cases there is often an equivalent definition of equivalences that we want to use instead, and the important property we need is that it's logically equivalent to (quasi-)isomorphism. *)
+(** We could define equivalences in any wild 1-category as bi-invertible maps, or in a wild 2-category as half-adjoint equivalences.  However, in concrete cases there is often an equivalent definition of equivalences that we want to use instead, and the important property we need is that it's logically equivalent to (quasi-)isomorphism. In [cat_hasequivs] below, we show that bi-invertible maps do provide a [HasEquivs] structure for any wild 1-category. *)
 
 Class HasEquivs (A : Type) `{Is1Cat A} :=
 {
@@ -422,3 +422,62 @@ Proof.
   refine (_ $@L _).
   exact ((tex z).2 _).
 Defined.
+
+(** * There is a default notion of equivalence for a 1-category, namely bi-invertibility. *)
+
+(** We do not use the half-adjoint definition, since we can't prove adjointification for that definition. *)
+
+Class Cat_IsBiInv {A} `{Is1Cat A} {x y : A} (f : x $-> y) := {
+  cat_equiv_inv : y $-> x;
+  cat_eisretr : f $o cat_equiv_inv $== Id y;
+  cat_equiv_inv' : y $-> x;
+  cat_eissect' : cat_equiv_inv' $o f $== Id x;
+}.
+
+Arguments cat_equiv_inv {A}%type_scope { _ _ _ _ x y} f {_}.
+Arguments cat_eisretr {A}%type_scope { _ _ _ _ x y} f {_}.
+Arguments cat_equiv_inv' {A}%type_scope { _ _ _ _ x y} f {_}.
+Arguments cat_eissect' {A}%type_scope { _ _ _ _ x y} f {_}.
+
+Arguments Build_Cat_IsBiInv {A}%type_scope {_ _ _ _ x y f} cat_equiv_inv cat_eisretr cat_equiv_inv' cat_eissect'.
+
+Record Cat_BiInv A `{Is1Cat A} (x y : A) := {
+  cat_equiv_fun :> x $-> y;
+  cat_equiv_isequiv : Cat_IsBiInv cat_equiv_fun;
+}.
+
+Global Existing Instance cat_equiv_isequiv.
+
+(** The two inverses are necessarily homotopic. *)
+Definition cat_inverses_homotopic {A} `{Is1Cat A} {x y : A} (f : x $-> y) {bif : Cat_IsBiInv f}
+  : cat_equiv_inv f $== cat_equiv_inv' f.
+Proof.
+  refine ((cat_idl _)^$ $@ _).
+  refine (cat_prewhisker (cat_eissect' f)^$ _ $@ _).
+  refine (cat_assoc _ _ _ $@ _).
+  refine (cat_postwhisker _ (cat_eisretr f) $@ _).
+  apply cat_idr.
+Defined.
+
+(** Therefore we can prove [eissect] for the first inverse as well. *)
+Definition cat_eissect {A} `{Is1Cat A} {x y : A} (f : x $-> y) {bif : Cat_IsBiInv f}
+  : cat_equiv_inv f $o f $== Id x
+  := (cat_inverses_homotopic f $@R f) $@ cat_eissect' f.
+
+(** This shows that any 1-category satisfies [HasEquivs].  We do not make it an instance, since we may want to use a different [HasEquivs] structure in particular cases. *)
+Definition cat_hasequivs A `{Is1Cat A} : HasEquivs A.
+Proof.
+  srapply Build_HasEquivs; intros x y.
+  1: exact (Cat_BiInv _ x y).
+  all:intros f; cbn beta in *.
+  - exact (Cat_IsBiInv f).
+  - exact f.
+  - exact _.
+  - apply Build_Cat_BiInv.
+  - intros; reflexivity.
+  - exact (cat_equiv_inv f).
+  - apply cat_eissect.
+  - apply cat_eisretr.
+  - intros g r s.
+    exact (Build_Cat_IsBiInv g r g s).
+Defined.
diff --git a/theories/WildCat/Yoneda.v b/theories/WildCat/Yoneda.v
index 0812a438238..8dba5391920 100644
--- a/theories/WildCat/Yoneda.v
+++ b/theories/WildCat/Yoneda.v
@@ -182,20 +182,25 @@ Definition opyon_equiv_0gpd {A : Type} `{HasEquivs A}
   {a b : A} (f : opyon_0gpd a $<~> opyon_0gpd b)
   : b $<~> a.
 Proof.
-  set (g := f^-1$).
-  srapply (cate_adjointify (f a (Id a)) (g b (Id b))).
-  - pose proof (gn := is1natural_natequiv _ _ g).
-    refine ((isnat (alnat:=gn) g (f a (Id a)) (Id b))^$ $@ _).
-    refine (fmap (g a) (cat_idr (f a (Id a))) $@ _).
+  (* Coq can't find the composite Coercion from equivalences of 0-groupoids to Funclass, so we make names for the underlying natural transformations of [f] and its inverse. *)
+  set (ft := cate_fun f).
+  set (gt := cate_fun f^-1$).
+  (* These are the maps that will define the desired equivalence: *)
+  set (fa := (ft a) (Id a)).
+  set (gb := (gt b) (Id b)).
+  srapply (cate_adjointify fa gb).
+  - pose proof (gn := is1natural_nattrans _ _ gt).
+    refine ((isnat (alnat:=gn) gt fa (Id b))^$ $@ _).
+    refine (fmap (gt a) (cat_idr fa) $@ _).
     1: rapply is0functor_fun_0gpd.
     1: exact _.
-    rapply eissect_0gpd.
+    exact (cat_eissect (f a) (Id a)).
   - pose proof (fn := is1natural_natequiv _ _ f).
-    refine ((isnat (alnat:=fn) f (g b (Id b)) (Id a))^$ $@ _).
-    refine (fmap (f b) (cat_idr (g b (Id b))) $@ _).
+    refine ((isnat (alnat:=fn) ft gb (Id a))^$ $@ _).
+    refine (fmap (ft b) (cat_idr gb) $@ _).
     1: rapply is0functor_fun_0gpd.
     1: exact _.
-    rapply eisretr_0gpd.
+    exact (cat_eisretr (f b) (Id b)).
   (* Not sure why typeclass inference doesn't find [is1natural_natequiv] and [is0functor_zerogpd_fun] above. *)
 Defined.
 
diff --git a/theories/WildCat/ZeroGroupoid.v b/theories/WildCat/ZeroGroupoid.v
index ac3876cf461..4d2e4e6634b 100644
--- a/theories/WildCat/ZeroGroupoid.v
+++ b/theories/WildCat/ZeroGroupoid.v
@@ -74,80 +74,37 @@ Proof.
   - reflexivity. (* Right identity. *)
 Defined.
 
-(** We define equivalences of 0-groupoids.  The definition is chosen to provide what is needed for the Yoneda lemma, and to match the concept for types, with paths replaced by 1-cells.  We are able to match the biinvertible definition.  The half-adjoint definition doesn't work, as we can't prove adjointification.  We would need to be in a 1-groupoid for that to be possible.  We could also use the "wrong" definition, without the eisadj condition, and things would go through, but it wouldn't match the definition for types. *)
-Class IsEquiv_0Gpd {G H : ZeroGpd} (f : G $-> H) := {
-  equiv_inv_0gpd : H $-> G;
-  eisretr_0gpd : f $o equiv_inv_0gpd $== Id H;
-  equiv_inv_0gpd' : H $-> G;
-  eissect_0gpd' : equiv_inv_0gpd' $o f $== Id G;
-}.
-
-Arguments equiv_inv_0gpd {G H}%type_scope f {_}.
-Arguments eisretr_0gpd {G H}%type_scope f {_} _.
-Arguments equiv_inv_0gpd' {G H}%type_scope f {_}.
-Arguments eissect_0gpd' {G H}%type_scope f {_} _.
+(** We define equivalences of 0-groupoids as the bi-invertible maps, using [Cat_BiInv] and [Cat_IsBiInv].  This definition is chosen to provide what is needed for the Yoneda lemma, and because it specializes to one of the correct definitions for types. *)
 
-Record Equiv_0Gpd (G H : ZeroGpd) := {
-  equiv_fun_0gpd :> Morphism_0Gpd G H;
-  equiv_isequiv_0gpd : IsEquiv_0Gpd equiv_fun_0gpd;
-}.
+Global Instance hasequivs_0gpd : HasEquivs ZeroGpd
+  := cat_hasequivs ZeroGpd.
 
-Global Existing Instance equiv_isequiv_0gpd.
+(** Coq can't find the composite of the coercions [cate_fun : G $<~> H >-> G $-> H] and [fun_0gpd : Morphism_0Gpd G H >-> G -> H], probably because it passes through the definitional equality of [G $-> H] and [Morphism_0Gpd G H].  I couldn't find a solution, so instead here is a helper function to manually do the coercion when needed. *)
 
-(** The two inverses are necessarily homotopic. *)
-Definition inverses_homotopic_0gpd {G H : ZeroGpd} (f : G $-> H) `{IsEquiv_0Gpd _ _ f}
-  : equiv_inv_0gpd f $== equiv_inv_0gpd' f.
-Proof.
-  set (g := equiv_inv_0gpd f).
-  set (g' := equiv_inv_0gpd' f).
-  intro x.
-  refine ((eissect_0gpd' f (g x))^$ $@ _); cbn.
-  refine (fmap g' _).
-  rapply eisretr_0gpd.
-Defined.
-
-(** Therefore we can prove [eissect] for the first inverse as well. *)
-Definition eissect_0gpd {G H : ZeroGpd} (f : G $-> H) `{IsEquiv_0Gpd _ _ f}
-  : equiv_inv_0gpd f $o f $== Id G
-  := (inverses_homotopic_0gpd f $@R f) $@ eissect_0gpd' f.
-
-Global Instance hasequivs_0gpd : HasEquivs ZeroGpd.
-Proof.
-  srapply Build_HasEquivs; intros G H.
-  1: exact (Equiv_0Gpd G H).
-  all:intros f; cbn beta in *.
-  - exact (IsEquiv_0Gpd f).
-  - exact f.
-  - exact _.
-  - apply Build_Equiv_0Gpd.
-  - intros; reflexivity.
-  - exact (equiv_inv_0gpd f).
-  - apply eissect_0gpd.
-  - apply eisretr_0gpd.
-  - intros g r s.
-    exact (Build_IsEquiv_0Gpd _ _ f g r g s).
-Defined.
+Definition equiv_fun_0gpd {G H : ZeroGpd} (f : G $<~> H) : G -> H
+  := fun_0gpd _ _ (cate_fun f).
 
-(** * We now give a different characterization of the equivalences of 0-groupoids, as the injective split essentially surjective 0-functors which are defined in EquivGpd. *)
+(** * We now give a different characterization of the equivalences of 0-groupoids, as the injective split essentially surjective 0-functors, which are defined in EquivGpd. *)
 
-(** Advantages of this logically equivalent formulation are that it tends to be easier to prove in examples and in some cases it is definitionally equal to [ExtensionAlong], which is convenient.  See Homotopy/Suspension.v and Algebra/AbGroups/Abelianization for examples. Advantages of the bi-invertible definition are that it reproduces a definition that is equivalent to [IsEquiv] when applied to types, assuming [Funext].  It also makes the proof of [HasEquivs] above easy. *)
+(** Advantages of this logically equivalent formulation are that it tends to be easier to prove in examples and that in some cases it is definitionally equal to [ExtensionAlong], which is convenient.  See Homotopy/Suspension.v and Algebra/AbGroups/Abelianization for examples. Advantages of the bi-invertible definition are that it reproduces a definition that is equivalent to [IsEquiv] when applied to types, assuming [Funext].  It also works in any 1-category. *)
 
 (** Every equivalence is injective and split essentially surjective. *)
 Definition IsSurjInj_Equiv_0Gpd {G H : ZeroGpd} (f : G $<~> H)
-  : IsSurjInj f.
+  : IsSurjInj (equiv_fun_0gpd f).
 Proof.
+  set (finv := equiv_fun_0gpd f^-1$).
   econstructor.
   - intro y.
-    exists (f^-1$ y).
-    rapply eisretr_0gpd.
+    exists (finv y).
+    rapply cat_eisretr.
   - intros x1 x2 m.
-    exact ((eissect_0gpd f x1)^$ $@ fmap f^-1$ m $@ eissect_0gpd f x2).
+    exact ((cat_eissect f x1)^$ $@ fmap finv m $@ cat_eissect f x2).
 Defined.
 
 (** Conversely, every injective split essentially surjective 0-functor is an equivalence. *)
 Global Instance IsEquiv_0Gpd_IsSurjInj {G H : ZeroGpd} (F : G $-> H)
   {e : IsSurjInj F}
-  : IsEquiv_0Gpd F.
+  : Cat_IsBiInv F.
 Proof.
   destruct e as [e0 e1]; unfold SplEssSurj in e0.
   srapply catie_adjointify.