Wildcat improvements

theories/Algebra/AbGroups/Abelianization.v

@@ -17,9 +17,9 @@ 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),
+  := issurjinj_isabel : forall (A : AbGroup),
       IsSurjInj (group_precomp A eta).
-Global Existing Instance isequiv0gpd_isabel.
+Global Existing Instance issurjinj_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).
 

theories/WildCat/Prod.v

@@ -158,28 +158,20 @@ Defined.
 
 (** Swap functor *)
 
-Definition prod_swap {A B : Type} : A * B -> B * A
-  := fun '(a , b) => (b , a).
-
-Global Instance isequiv_prod_swap {A B}
-  : IsEquiv (@prod_swap A B)
-  := Build_IsEquiv _ _ prod_swap prod_swap
-    (fun _ => idpath) (fun _ => idpath) (fun _ => idpath).
-
-Global Instance is0functor_prod_swap {A B : Type} `{IsGraph A, IsGraph B}
-  : Is0Functor (@prod_swap A B).
+Global Instance is0functor_equiv_prod_symm {A B : Type} `{IsGraph A, IsGraph B}
+  : Is0Functor (equiv_prod_symm A B).
 Proof.
   snrapply Build_Is0Functor.
   intros a b.
-  apply prod_swap.
+  apply equiv_prod_symm.
 Defined.
 
-Global Instance is1functor_prod_swap {A B : Type} `{Is1Cat A, Is1Cat B}
-  : Is1Functor (@prod_swap A B).
+Global Instance is1functor_equiv_prod_symm {A B : Type} `{Is1Cat A, Is1Cat B}
+  : Is1Functor (equiv_prod_symm A B).
 Proof.
   snrapply Build_Is1Functor.
   - intros a b f g.
-    apply prod_swap.
+    apply equiv_prod_symm.
   - intros a.
     reflexivity.
   - reflexivity.

theories/WildCat/ZeroGroupoid.v

@@ -82,27 +82,40 @@ Global Instance hasequivs_0gpd : 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).
+  := fun_0gpd _ _ (cat_equiv_fun _ _ _ f).
+
+(** * Some tools for manipulating equivalences of 0-groupoids.  Even though the proofs are easy, in certain contexts Coq gets confused about [$==] vs [$->], which makes it hard to prove this inline.  So we record them here. *)
+
+(** Every equivalence is injective. *)
+Definition isinj_equiv_0gpd {G H : ZeroGpd} (f : G $<~> H)
+  {x y : G} (h : equiv_fun_0gpd f x $== equiv_fun_0gpd f y)
+  : x $== y.
+Proof.
+  exact ((cat_eissect f x)^$ $@ fmap (equiv_fun_0gpd f^-1$) h $@ cat_eissect f y).
+Defined.
+
+(** This is one example of many things that could be ported from Basics/Equivalences.v. *)
+Definition moveR_equiv_V_0gpd {G H : ZeroGpd} (f : G $<~> H) (x : H) (y : G) (p : x $== equiv_fun_0gpd f y)
+  : equiv_fun_0gpd f^-1$ x $== y
+  := fmap (equiv_fun_0gpd f^-1$) p $@ cat_eissect f y.
 
 (** * 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)
+Global Instance 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).
+    exists (equiv_fun_0gpd f^-1$ y).
     rapply cat_eisretr.
-  - intros x1 x2 m.
-    exact ((cat_eissect f x1)^$ $@ fmap finv m $@ cat_eissect f x2).
+  - apply isinj_equiv_0gpd.
 Defined.
 
-(** Conversely, every injective split essentially surjective 0-functor is an equivalence. *)
-Global Instance IsEquiv_0Gpd_IsSurjInj {G H : ZeroGpd} (F : G $-> H)
+(** Conversely, every injective split essentially surjective 0-functor is an equivalence.  In practice, this is often the easiest way to prove that a functor is an equivalence. *)
+Definition isequiv_0gpd_issurjinj {G H : ZeroGpd} (F : G $-> H)
   {e : IsSurjInj F}
   : Cat_IsBiInv F.
 Proof.