Yoneda lemma using 0-groupoids

theories/Algebra/AbGroups/Abelianization.v

@@ -10,15 +10,15 @@ 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.
 
 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. }

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.

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.

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.

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.