diff --git a/theories/Algebra/AbGroups/Abelianization.v b/theories/Algebra/AbGroups/Abelianization.v
index 203d1b82270..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.
@@ -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/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.
diff --git a/theories/Homotopy/Suspension.v b/theories/Homotopy/Suspension.v
index a0143603bee..53fda42df6f 100644
--- a/theories/Homotopy/Suspension.v
+++ b/theories/Homotopy/Suspension.v
@@ -248,8 +248,8 @@ Section UnivProp.
       exact (dp_apD_nat p (merid x)).
   Defined.
 
-  (** And now we can prove that it's an equivalence. *)
-  Definition equiv0gpd_Susp_ind_inv : IsEquiv0Gpd Susp_ind_inv.
+  (** 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.
     - 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)). }
@@ -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.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/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/EquivGpd.v b/theories/WildCat/EquivGpd.v
index d513732f029..11dbc347be6 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 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 [$==]. *)
 
 Class SplEssSurj {A B : Type} `{Is0Gpd A, Is0Gpd B}
@@ -15,48 +17,50 @@ 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}
+(** 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} :=
 {
-  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.
 
@@ -71,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.
@@ -101,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)}
@@ -158,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.
@@ -170,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.
@@ -187,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.
@@ -199,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. *)
@@ -235,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/Yoneda.v b/theories/WildCat/Yoneda.v
index d350fdc33e3..8dba5391920 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 *)
 
@@ -133,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.
@@ -153,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.
@@ -163,24 +164,94 @@ Proof.
   - rapply is1natural_opyoneda.
 Defined.
 
+(** 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.
+  - intro b.
+    rapply (Build_ZeroGpd (opyon a b)).
+  - snrapply Build_Is0Functor.
+    intros b c f; cbn beta.
+    snrapply Build_Morphism_0Gpd; 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.
+  (* 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 _.
+    exact (cat_eissect (f a) (Id a)).
+  - pose proof (fn := is1natural_natequiv _ _ f).
+    refine ((isnat (alnat:=fn) ft gb (Id a))^$ $@ _).
+    refine (fmap (ft b) (cat_idr gb) $@ _).
+    1: rapply is0functor_fun_0gpd.
+    1: exact _.
+    exact (cat_eisretr (f b) (Id b)).
+  (* 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_Morphism_0Gpd.
+    1: exact (cat_precomp z f).
+    exact _.
+  - snrapply Build_Morphism_0Gpd.
+    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. *)
 
 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}
@@ -190,17 +261,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}
@@ -209,24 +280,37 @@ 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).
+
+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).
diff --git a/theories/WildCat/ZeroGroupoid.v b/theories/WildCat/ZeroGroupoid.v
new file mode 100644
index 00000000000..4d2e4e6634b
--- /dev/null
+++ b/theories/WildCat/ZeroGroupoid.v
@@ -0,0 +1,121 @@
+Require Import Basics.Overture Basics.Tactics.
+Require Import WildCat.Core WildCat.Equiv WildCat.EquivGpd.
+
+(** * 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.
+
+(* 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;
+}.
+
+Global Existing Instance is0functor_fun_0gpd.
+
+(** 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.
+  exact Morphism_0Gpd.
+Defined.
+
+Global Instance is01cat_0gpd : Is01Cat ZeroGpd.
+Proof.
+  srapply Build_Is01Cat.
+  - intro G.
+    exact (Build_Morphism_0Gpd G G idmap _).
+  - intros G H K f g.
+    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.
+  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. (* Associativity. *)
+  - reflexivity. (* Left identity. *)
+  - reflexivity. (* Right identity. *)
+Defined.
+
+(** 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. *)
+
+Global Instance hasequivs_0gpd : HasEquivs ZeroGpd
+  := cat_hasequivs ZeroGpd.
+
+(** 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. *)
+
+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. *)
+
+(** 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 (equiv_fun_0gpd f).
+Proof.
+  set (finv := equiv_fun_0gpd f^-1$).
+  econstructor.
+  - intro y.
+    exists (finv y).
+    rapply cat_eisretr.
+  - intros x1 x2 m.
+    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}
+  : Cat_IsBiInv F.
+Proof.
+  destruct e as [e0 e1]; unfold SplEssSurj in e0.
+  srapply catie_adjointify.
+  - 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.  apply e0.
+  - cbn.  intro x.
+    apply e1.
+    apply e0.
+Defined.