From 07d228d59f2e1c24f3fa874cc9b5e712b02dc33f Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Mon, 25 Sep 2023 12:05:30 -0400
Subject: [PATCH 1/8] Abelianization: correct name of IsSurjInj field

---
 theories/Algebra/AbGroups/Abelianization.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/Algebra/AbGroups/Abelianization.v b/theories/Algebra/AbGroups/Abelianization.v
index 41ac5b900a7..84b39d88c25 100644
--- a/theories/Algebra/AbGroups/Abelianization.v
+++ b/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).
 

From 98321d01ec979c6891eb9914388232f1a3188116 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Mon, 25 Sep 2023 12:06:11 -0400
Subject: [PATCH 2/8] WildCat/Prod: reuse equiv_prod_symm instead of redefining
 it

---
 theories/WildCat/Prod.v | 20 ++++++--------------
 1 file changed, 6 insertions(+), 14 deletions(-)

diff --git a/theories/WildCat/Prod.v b/theories/WildCat/Prod.v
index f5d8fab339a..93b06f6d5bc 100644
--- a/theories/WildCat/Prod.v
+++ 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.

From 8a6e237492fd8a5caecd88dbdd19be9fc89fda31 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Mon, 25 Sep 2023 12:08:55 -0400
Subject: [PATCH 3/8] WildCat/ZeroGroupoid: minor additions

---
 theories/WildCat/ZeroGroupoid.v | 29 +++++++++++++++++++++--------
 1 file changed, 21 insertions(+), 8 deletions(-)

diff --git a/theories/WildCat/ZeroGroupoid.v b/theories/WildCat/ZeroGroupoid.v
index 4d2e4e6634b..0b1ad514fd5 100644
--- a/theories/WildCat/ZeroGroupoid.v
+++ b/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.

From d9897e9b1ab9d56eefc0dea444b552be4c07f9d6 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Mon, 25 Sep 2023 13:01:26 -0400
Subject: [PATCH 4/8] WildCat: equiv_precompose_cat_equiv follows from
 is1functor_opyon

---
 theories/WildCat/Equiv.v  | 50 ---------------------------------------
 theories/WildCat/Yoneda.v | 11 +++++++++
 2 files changed, 11 insertions(+), 50 deletions(-)

diff --git a/theories/WildCat/Equiv.v b/theories/WildCat/Equiv.v
index 9c53a6dc556..46a10079d57 100644
--- a/theories/WildCat/Equiv.v
+++ b/theories/WildCat/Equiv.v
@@ -331,56 +331,6 @@ Proof.
   - apply cate_isretr.
 Defined.
 
-(** ** Pre/post-composition with equivalences *)
-
-(** Precomposition with a cat_equiv is an equivalence between the homs *)
-Definition equiv_precompose_cat_equiv {A : Type} `{HasEquivs A} `{!HasMorExt A}
-  {x y z : A} (f : x $<~> y)
-  : (y $-> z) <~> (x $-> z).
-Proof.
-  snrapply equiv_adjointify.
-  1: exact (fun g => g $o f).
-  1: exact (fun h => h $o f^-1$).
-  { intros h.
-    apply path_hom.
-    refine (cat_assoc _ _ _ $@ _).
-    refine (_ $@ _).
-    { rapply cat_postwhisker.
-      apply cate_issect. }
-    apply cat_idr. }
-  intros g.
-  apply path_hom.
-  refine (cat_assoc _ _ _ $@ _).
-  refine (_ $@ _).
-  { rapply cat_postwhisker.
-    apply cate_isretr. }
-  apply cat_idr.
-Defined.
-
-(** Postcomposition with a cat_equiv is an equivalence between the homs *)
-Definition equiv_postcompose_cat_equiv {A : Type} `{HasEquivs A} `{!HasMorExt A}
-  {x y z : A} (f : y $<~> z)
-  : (x $-> y) <~> (x $-> z).
-Proof.
-  snrapply equiv_adjointify.
-  1: exact (fun g => f $o g).
-  1: exact (fun h => f^-1$ $o h).
-  { intros h.
-    apply path_hom.
-    refine ((cat_assoc _ _ _)^$ $@ _).
-    refine (_ $@ _).
-    { rapply cat_prewhisker.
-      apply cate_isretr. }
-    apply cat_idl. }
-  intros g.
-  apply path_hom.
-  refine ((cat_assoc _ _ _)^$ $@ _).
-  refine (_ $@ _).
-  { rapply cat_prewhisker.
-    apply cate_issect. }
-  apply cat_idl.
-Defined.
-
 (** * Initial objects and terminal objects are all respectively equivalent. *)
 
 Lemma cate_isinitial A `{HasEquivs A} (x y : A)
diff --git a/theories/WildCat/Yoneda.v b/theories/WildCat/Yoneda.v
index 8dba5391920..fc99316cfc7 100644
--- a/theories/WildCat/Yoneda.v
+++ b/theories/WildCat/Yoneda.v
@@ -76,6 +76,17 @@ Proof.
     apply cat_assoc.
 Defined.
 
+(** We record these corollaries here, since we use them below. *)
+Definition equiv_postcompose_cat_equiv {A : Type} `{HasEquivs A} `{!HasMorExt A}
+  {x y z : A} (f : y $<~> z)
+  : (x $-> y) <~> (x $-> z)
+  := emap (opyon x) f.
+
+Definition equiv_precompose_cat_equiv {A : Type} `{HasEquivs A} `{!HasMorExt A}
+  {x y z : A} (f : x $<~> y)
+  : (y $-> z) <~> (x $-> z)
+  := @equiv_postcompose_cat_equiv A^op _ _ _ _ _ _ z y x f.
+
 Definition opyoneda {A : Type} `{Is01Cat A} (a : A)
            (F : A -> Type) {ff : Is0Functor F}
   : F a -> (opyon a $=> F).

From 7dc8ef4876e6ad1ddc48d4c1fd2edbe1f917683d Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Mon, 25 Sep 2023 17:36:23 -0400
Subject: [PATCH 5/8] WildCat: add equiv_pre/postcompose_core_cat_equiv with
 slick proof

---
 theories/Pointed/Core.v     | 12 ++++++++++++
 theories/Types/Equiv.v      | 10 ++++++++++
 theories/WildCat/Equiv.v    | 22 ++++++++++++++++++++++
 theories/WildCat/Universe.v | 14 +++++++++++++-
 theories/WildCat/Yoneda.v   | 23 ++++++++++++++++++++++-
 5 files changed, 79 insertions(+), 2 deletions(-)

diff --git a/theories/Pointed/Core.v b/theories/Pointed/Core.v
index 14fcf7a21ae..e85755b1266 100644
--- a/theories/Pointed/Core.v
+++ b/theories/Pointed/Core.v
@@ -712,6 +712,18 @@ Proof.
     + intros x; exact (s x).
 Defined.
 
+Global Instance hasmorext_core_ptype `{Funext} : HasMorExt (core pType).
+Proof.
+  snrapply Build_HasMorExt.
+  intros a b f g.
+  unfold GpdHom_path.
+  cbn in f, g.
+  (* [GpdHom_path] and the inverse of [equiv_path_pequiv] are not definitionally equal, but they compute to definitionally equal things on [idpath]. *)
+  apply (isequiv_homotopic (equiv_path_pequiv f g)^-1%equiv).
+  intro p; induction p; cbn.
+  reflexivity.
+Defined.
+
 (** pType is a univalent 1-coherent 1-category *)
 Global Instance isunivalent_ptype `{Univalence} : IsUnivalent1Cat pType.
 Proof.
diff --git a/theories/Types/Equiv.v b/theories/Types/Equiv.v
index 81723746b53..e2fbe6cc708 100644
--- a/theories/Types/Equiv.v
+++ b/theories/Types/Equiv.v
@@ -107,6 +107,16 @@ Section AssumeFunext.
     (* Coq can find this instance by itself, but it's slow. *)
     := equiv_isequiv (equiv_path_equiv e1 e2).
 
+  (** The inverse equivalence is homotopic to [ap equiv_fun], so that is also an equivalence. *)
+  Global Instance isequiv_ap_equiv_fun `{Funext} {A B : Type} (e1 e2 : A <~> B)
+    : IsEquiv (ap (x:=e1) (y:=e2) (@equiv_fun A B)).
+  Proof.
+    snrapply isequiv_homotopic.
+    - exact (equiv_path_equiv e1 e2)^-1%equiv.
+    - exact _.
+    - intro p. exact (ap_compose (fun v => (equiv_fun v; equiv_isequiv v)) pr1 p)^.
+  Defined.
+
   (** This implies that types of equivalences inherit truncation.  Note that we only state the theorem for [n.+1]-truncatedness, since it is not true for contractibility: if [B] is contractible but [A] is not, then [A <~> B] is not contractible because it is not inhabited.
 
    Don't confuse this lemma with [trunc_equiv], which says that if [A] is truncated and [A] is equivalent to [B], then [B] is truncated.  It would be nice to find a better pair of names for them. *)
diff --git a/theories/WildCat/Equiv.v b/theories/WildCat/Equiv.v
index 46a10079d57..3d370b5d206 100644
--- a/theories/WildCat/Equiv.v
+++ b/theories/WildCat/Equiv.v
@@ -242,6 +242,7 @@ Definition cat_path_equiv {A : Type} `{IsUnivalent1Cat A} (a b : A)
 
 Record core (A : Type) := { uncore : A }.
 Arguments uncore {A} c.
+Arguments Build_core {A} a : rename.
 
 Global Instance isgraph_core {A : Type} `{HasEquivs A}
   : IsGraph (core A).
@@ -331,6 +332,27 @@ Proof.
   - apply cate_isretr.
 Defined.
 
+Global Instance hasequivs_core {A : Type} `{HasEquivs A}
+  : HasEquivs (core A).
+Proof.
+  srapply Build_HasEquivs.
+  1: exact (fun a b => a $-> b).  (* In [core A], i.e. [CatEquiv' (uncore a) (uncore b)]. *)
+  all: intros a b f; cbn; intros.
+  - exact Unit.  (* Or [CatIsEquiv' (uncore a) (uncore b) (cate_fun f)]? *)
+  - exact f.
+  - exact tt.    (* Or [cate_isequiv' _ _ _]? *)
+  - exact f.
+  - reflexivity.
+  - exact f^-1$.
+  - refine (compose_cate_fun _ _ $@ _).
+    refine (cate_issect _ $@ _).
+    symmetry; apply id_cate_fun.
+  - refine (compose_cate_fun _ _ $@ _).
+    refine (cate_isretr _ $@ _).
+    symmetry; apply id_cate_fun.
+  - exact tt.
+Defined.
+
 (** * Initial objects and terminal objects are all respectively equivalent. *)
 
 Lemma cate_isinitial A `{HasEquivs A} (x y : A)
diff --git a/theories/WildCat/Universe.v b/theories/WildCat/Universe.v
index 5d2848a0d8b..0344606ea74 100644
--- a/theories/WildCat/Universe.v
+++ b/theories/WildCat/Universe.v
@@ -1,4 +1,4 @@
-Require Import Basics.Overture Basics.Tactics Basics.Equivalences.
+Require Import Basics.Overture Basics.Tactics Basics.Equivalences Types.Equiv.
 Require Import WildCat.Core.
 Require Import WildCat.Equiv.
 
@@ -76,6 +76,18 @@ Proof.
   - intros g r s; refine (isequiv_adjointify f g r s).
 Defined.
 
+Global Instance hasmorext_core_type `{Funext}: HasMorExt (core Type).
+Proof.
+  snrapply Build_HasMorExt.
+  intros A B f g; cbn in *.
+  snrapply isequiv_homotopic.
+  - exact (GpdHom_path o (ap (x:=f) (y:=g) equiv_fun)).
+  - nrapply isequiv_compose.
+    1: apply isequiv_ap_equiv_fun.
+    exact (isequiv_Htpy_path (uncore A) (uncore B) f g).
+  - intro p; by induction p.
+Defined.
+
 Definition catie_isequiv {A B : Type} {f : A $-> B}
        `{IsEquiv A B f} : CatIsEquiv f.
 Proof.
diff --git a/theories/WildCat/Yoneda.v b/theories/WildCat/Yoneda.v
index fc99316cfc7..ab948cd5eaa 100644
--- a/theories/WildCat/Yoneda.v
+++ b/theories/WildCat/Yoneda.v
@@ -76,7 +76,7 @@ Proof.
     apply cat_assoc.
 Defined.
 
-(** We record these corollaries here, since we use them below. *)
+(** We record these corollaries here, since we use some of them below. *)
 Definition equiv_postcompose_cat_equiv {A : Type} `{HasEquivs A} `{!HasMorExt A}
   {x y z : A} (f : y $<~> z)
   : (x $-> y) <~> (x $-> z)
@@ -87,6 +87,27 @@ Definition equiv_precompose_cat_equiv {A : Type} `{HasEquivs A} `{!HasMorExt A}
   : (y $-> z) <~> (x $-> z)
   := @equiv_postcompose_cat_equiv A^op _ _ _ _ _ _ z y x f.
 
+(* The following implicitly use [hasequivs_core].  Note that when [A] has morphism extensionality, it doesn't follow that [core A] does.  We'd need to know that being an equivalence is a proposition, and we don't assume that (since even for [Type] it requires [Funext], see [hasmorext_core_type]). So we need to assume this in the following results. *)
+
+(** Postcomposition with a cat_equiv is an equivalence between the types of equivalences. *)
+Definition equiv_postcompose_core_cat_equiv {A : Type} `{HasEquivs A} `{!HasMorExt (core A)}
+  {x y z : A} (f : y $<~> z)
+  : (x $<~> y) <~> (x $<~> z).
+Proof.
+  change ((Build_core x $-> Build_core y) <~> (Build_core x $-> Build_core z)).
+  refine (equiv_postcompose_cat_equiv (A := core A) _).
+  exact f.  (* It doesn't work to insert [f] on the previous line. *)
+Defined.
+
+Definition equiv_precompose_core_cat_equiv {A : Type} `{HasEquivs A} `{!HasMorExt (core A)}
+  {x y z : A} (f : x $<~> y)
+  : (y $<~> z) <~> (x $<~> z).
+Proof.
+  change ((Build_core y $-> Build_core z) <~> (Build_core x $-> Build_core z)).
+  refine (equiv_precompose_cat_equiv (A := core A) _).
+  exact f.  (* It doesn't work to insert [f] on the previous line. *)
+Defined.
+
 Definition opyoneda {A : Type} `{Is01Cat A} (a : A)
            (F : A -> Type) {ff : Is0Functor F}
   : F a -> (opyon a $=> F).

From b49706f5f345e5d49313f62cce031881bdfaf752 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Mon, 25 Sep 2023 19:24:07 -0400
Subject: [PATCH 6/8] WildCat: add and use compose_catie and Build_NatEquiv'

---
 theories/WildCat/Equiv.v    | 13 +++++++----
 theories/WildCat/NatTrans.v | 43 +++++++++++++++++--------------------
 2 files changed, 29 insertions(+), 27 deletions(-)

diff --git a/theories/WildCat/Equiv.v b/theories/WildCat/Equiv.v
index 3d370b5d206..2eb14784d56 100644
--- a/theories/WildCat/Equiv.v
+++ b/theories/WildCat/Equiv.v
@@ -71,7 +71,7 @@ Definition cate_adjointify {A} `{HasEquivs A} {a b : A}
            (f : a $-> b) (g : b $-> a)
            (r : f $o g $== Id b) (s : g $o f $== Id a)
   : a $<~> b
-  := @Build_CatEquiv _ _ _ _ _ _ a b f (catie_adjointify f g r s).
+  := Build_CatEquiv f (fe:=catie_adjointify f g r s).
 
 (** This one we define to construct the whole inverse equivalence. *)
 Definition cate_inv {A} `{HasEquivs A} {a b : A} (f : a $<~> b) : b $<~> a.
@@ -119,10 +119,11 @@ Global Instance symmetric_cate {A} `{HasEquivs A}
   := fun a b f => cate_inv f.
 
 (** Equivalences can be composed. *)
-Definition compose_cate {A} `{HasEquivs A} {a b c : A}
-  (g : b $<~> c) (f : a $<~> b) : a $<~> c.
+Global Instance compose_catie {A} `{HasEquivs A} {a b c : A}
+  (g : b $<~> c) (f : a $<~> b)
+  : CatIsEquiv (g $o f).
 Proof.
-  refine (cate_adjointify (g $o f) (f^-1$ $o g^-1$) _ _).
+  refine (catie_adjointify _ (f^-1$ $o g^-1$) _ _).
   - refine (cat_assoc _ _ _ $@ _).
     refine ((_ $@L cat_assoc_opp _ _ _) $@ _).
     refine ((_ $@L (cate_isretr _ $@R _)) $@ _).
@@ -135,6 +136,10 @@ Proof.
     apply cate_issect.
 Defined.
 
+Definition compose_cate {A} `{HasEquivs A} {a b c : A}
+  (g : b $<~> c) (f : a $<~> b) : a $<~> c
+  := Build_CatEquiv (g $o f).
+
 Notation "g $oE f" := (compose_cate g f).
 
 Definition compose_cate_fun {A} `{HasEquivs A}
diff --git a/theories/WildCat/NatTrans.v b/theories/WildCat/NatTrans.v
index f678a9379f9..50ebdd5fd01 100644
--- a/theories/WildCat/NatTrans.v
+++ b/theories/WildCat/NatTrans.v
@@ -192,42 +192,39 @@ Defined.
 Global Set Warnings "-ambiguous-paths".
 Coercion nattrans_natequiv : NatEquiv >-> NatTrans.
 
-Definition natequiv_compose {A B} {F G H : A -> B} `{IsGraph A} `{HasEquivs B}
-  `{!Is0Functor F, !Is0Functor G, !Is0Functor H}
-  : NatEquiv G H -> NatEquiv F G -> NatEquiv F H.
+Definition Build_NatEquiv' {A B : Type} `{IsGraph A} `{HasEquivs B}
+  {F G : A -> B} `{!Is0Functor F, !Is0Functor G}
+  (alpha : NatTrans F G) `{forall a, CatIsEquiv (alpha a)}
+  : NatEquiv F G.
 Proof.
-  intros alpha beta.
   snrapply Build_NatEquiv.
-  1: exact (fun a => alpha a $oE beta a).
-  hnf; intros x y f.
-  refine (cat_prewhisker (compose_cate_fun _ _) _ $@ _).
-  refine (_ $@ cat_postwhisker _ (compose_cate_fun _ _)^$).
-  revert x y f.
-  rapply is1natural_comp.
+  - intro a.
+    refine (Build_CatEquiv (alpha a)).
+  - intros a a' f.
+    refine (cate_buildequiv_fun _ $@R _ $@ _ $@ (_ $@L cate_buildequiv_fun _)^$).
+    apply (isnat alpha).
 Defined.
 
+Definition natequiv_compose {A B} {F G H : A -> B} `{IsGraph A} `{HasEquivs B}
+  `{!Is0Functor F, !Is0Functor G, !Is0Functor H}
+  (alpha : NatEquiv G H) (beta : NatEquiv F G)
+  : NatEquiv F H
+  := Build_NatEquiv' (nattrans_comp alpha beta).
+
 Definition natequiv_prewhisker {A B C} {H K : B -> C}
   `{IsGraph A, HasEquivs B, HasEquivs C, !Is0Functor H, !Is0Functor K}
   (alpha : NatEquiv H K) (F : A -> B) `{!Is0Functor F}
-  : NatEquiv (H o F) (K o F).
-Proof.
-  snrapply Build_NatEquiv.
-  1: exact (alpha o F).
-  exact (is1natural_prewhisker _ _).
-Defined.
+  : NatEquiv (H o F) (K o F)
+  := Build_NatEquiv' (nattrans_prewhisker alpha F).
 
 Definition natequiv_postwhisker {A B C} {F G : A -> B}
   `{IsGraph A, HasEquivs B, HasEquivs C, !Is0Functor F, !Is0Functor G}
    (K : B -> C) (alpha : NatEquiv F G) `{!Is0Functor K, !Is1Functor K}
   : NatEquiv (K o F) (K o G).
 Proof.
-  snrapply Build_NatEquiv.
-  1: exact (fun a => emap K (alpha a)).
-  hnf. intros x y f.
-  refine (cat_prewhisker (cate_buildequiv_fun _) _ $@ _).
-  refine (_ $@ cat_postwhisker _ (cate_buildequiv_fun _)^$).
-  revert x y f.
-  exact (is1natural_postwhisker _ _).
+  srefine (Build_NatEquiv' (nattrans_postwhisker K alpha)).
+  2: unfold nattrans_postwhisker, trans_postwhisker; cbn.
+  all: exact _.
 Defined.
 
 Definition natequiv_inverse {A B : Type} `{IsGraph A} `{HasEquivs B}

From 5633e937641c70cd6974bf1933370ec479930fd5 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Mon, 25 Sep 2023 20:01:01 -0400
Subject: [PATCH 7/8] Yoneda: expand 0gpd version, and simplify some things

---
 theories/WildCat/Yoneda.v | 158 ++++++++++++++++++++++++--------------
 1 file changed, 99 insertions(+), 59 deletions(-)

diff --git a/theories/WildCat/Yoneda.v b/theories/WildCat/Yoneda.v
index ab948cd5eaa..8c3e6bdbe57 100644
--- a/theories/WildCat/Yoneda.v
+++ b/theories/WildCat/Yoneda.v
@@ -196,78 +196,118 @@ 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.
+(** We repeat the above, regarding [opyon] as landing in 0-groupoids, using the 1-category structure on [ZeroGpd] in [ZeroGroupoid.v].  This has many advantages.  It avoids [HasMorExt], which means that we don't need [Funext] in many examples.  It also avoids [Is1Cat_Strong], which means the results all have the same hypotheses, namely that [A] is a 1-category.  This allows us to simplify the proof of [opyon_equiv_0gpd], making use of [opyoneda_isretr_0gpd]. *)
+
+Definition opyon_0gpd {A : Type} `{Is1Cat A} (a : A) : A -> ZeroGpd
+  := fun b => Build_ZeroGpd (a $-> b) _ _ _.
+
+Global Instance is0functor_opyon_0gpd {A : Type} `{Is1Cat A} (a : A)
+  : Is0Functor (opyon_0gpd a).
+Proof.
+  apply Build_Is0Functor.
+  intros b c f.
+  exact (Build_Morphism_0Gpd (opyon_0gpd a b) (opyon_0gpd a c) (cat_postcomp a f) _).
+Defined.
+
+Global Instance is1functor_opyon_0gpd {A : Type} `{Is1Cat A} (a : A)
+  : Is1Functor (opyon_0gpd a).
+Proof.
+  rapply Build_Is1Functor.
+  + intros x y f g p h.
+    apply (cat_prewhisker p).
+  + intros x h.
+    apply cat_idl.
+  + intros x y z f g h.
+    apply cat_assoc.
+Defined.
+
+Definition opyoneda_0gpd {A : Type} `{Is1Cat A} (a : A)
+           (F : A -> ZeroGpd) `{!Is0Functor F, !Is1Functor F}
+  : F a -> (opyon_0gpd a $=> F).
 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.
+  intros x b.
+  refine (Build_Morphism_0Gpd (opyon_0gpd a b) (F b) (fun f => fmap F f x) _).
+  rapply Build_Is0Functor.
+  intros f1 f2 h.
+  exact (fmap2 F h x).
 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)
+Definition un_opyoneda_0gpd {A : Type} `{Is1Cat A}
+  (a : A) (F : A -> ZeroGpd) {ff : Is0Functor F}
+  : (opyon_0gpd a $=> F) -> F a
+  := fun alpha => alpha a (Id a).
+
+Global Instance is1natural_opyoneda_0gpd {A : Type} `{Is1Cat A}
+  (a : A) (F : A -> ZeroGpd) `{!Is0Functor F, !Is1Functor F} (x : F a)
+  : Is1Natural (opyon_0gpd a) F (opyoneda_0gpd a F x).
+Proof.
+  unfold opyon_0gpd, opyoneda_0gpd; intros b c f g; cbn in *.
+  exact (fmap_comp F g f x).
+Defined.
+
+Definition opyoneda_issect_0gpd {A : Type} `{Is1Cat A} (a : A)
+           (F : A -> ZeroGpd) `{!Is0Functor F, !Is1Functor F}
+           (x : F a)
+  : un_opyoneda_0gpd a F (opyoneda_0gpd a F x) $== x
+  := fmap_id F a x.
+
+(** Note that we do not in general recover the witness of 1-naturality.  Indeed, if [A] is fully coherent, then a transformation of the form [opyoneda a F x] is always also fully coherently natural, so an incoherent witness of 1-naturality could not be recovered in this way.  *)
+Definition opyoneda_isretr_0gpd {A : Type} `{Is1Cat A} (a : A)
+           (F : A -> ZeroGpd) `{!Is0Functor F, !Is1Functor F}
+           (alpha : opyon_0gpd a $=> F) {alnat : Is1Natural (opyon_0gpd a) F alpha}
+           (b : A)
+  : opyoneda_0gpd a F (un_opyoneda_0gpd a F alpha) b $== alpha b.
+Proof.
+  unfold opyoneda, un_opyoneda, opyon; intros f.
+  refine ((isnat alpha f (Id a))^$ $@ _).
+  cbn.
+  apply (fmap (alpha b)).
+  exact (cat_idr f).
+Defined.
+
+(** Specialization to "full-faithfulness" of the Yoneda embedding.  (In quotes because, again, incoherence means we can't recover the witness of naturality.)  *)
+Definition opyon_0gpd_cancel {A : Type} `{Is1Cat A} (a b : A)
+  : (opyon_0gpd a $=> opyon_0gpd b) -> (b $-> a)
+  := un_opyoneda_0gpd a (opyon_0gpd b).
+
+(** Since no extra hypotheses are needed, we use the name with "1" for the [Fun11] version. *)
+Definition opyon1_0gpd {A : Type} `{Is1Cat A} (a : A) : Fun11 A ZeroGpd
+  := Build_Fun11 _ _ (opyon_0gpd a).
+
+(** We can also deduce "full-faithfulness" on equivalences.  We explain how this compares to [opyon_equiv] above.  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. The proof is also simpler, since we can re-use the work done in [opyoneda_isretr_0gpd]. *)
+Definition opyon_equiv_0gpd {A : Type} `{HasEquivs A} `{!Is1Cat A}
+  {a b : A} (f : opyon1_0gpd a $<~> opyon1_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)).
+  set (fa := (cate_fun f a) (Id a)).     (* Equivalently, [un_opyoneda_0gpd a _ f]. *)
+  set (gb := (cate_fun f^-1$ b) (Id b)). (* Equivalently, [un_opyoneda_0gpd b _ f^-1$]. *)
   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. *)
+  (* [opyoneda_0gpd] is defined by postcomposition, so [opyoneda_isretr_0gpd] simplifies both LHSs.*)
+  - exact (opyoneda_isretr_0gpd _ _ f^-1$ a fa $@ cat_eissect (f a) (Id a)).
+  - exact (opyoneda_isretr_0gpd _ _ f     b gb $@ cat_eisretr (f b) (Id b)).
 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. *)
+(** Since [opyon_0gpd] is a 1-functor, postcomposition with a [cat_equiv] is an equivalence between the hom 0-groupoids. Note that we do not require [HasMorExt], as [equiv_postcompose_cat_equiv] does. *)
+Definition equiv_postcompose_cat_equiv_0gpd {A : Type} `{HasEquivs A}
+  {x y z : A} (f : y $<~> z)
+  : opyon_0gpd x y $<~> opyon_0gpd x z
+  := emap (opyon_0gpd x) f.
+
+(** The dual result, which is used in the next result. *)
 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.
+  : opyon_0gpd y z $<~> opyon_0gpd x z
+  := @equiv_postcompose_cat_equiv_0gpd A^op _ _ _ _ _ z y x f.
 
-(** 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]. *)
+(** A converse to [opyon_equiv_0gpd].  Together, we get a logical equivalence between [b $<~> a] and [opyon_0gpd a $<~> opyon_0gpd b], without [HasMorExt]. *)
 Definition natequiv_opyon_equiv_0gpd {A : Type} `{HasEquivs A}
   {a b : A} (e : b $<~> a)
-  : opyon_0gpd a $<~> opyon_0gpd b.
+  : opyon1_0gpd a $<~> opyon1_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.
+  - rapply is1natural_opyoneda_0gpd.
 Defined.
 
 (** ** The contravariant Yoneda lemma *)
@@ -334,15 +374,15 @@ Definition natequiv_yon_equiv {A : Type} `{HasEquivs 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 yon1_0gpd {A : Type} `{Is1Cat A} (a : A) : Fun01 A^op ZeroGpd
+  := opyon1_0gpd (A:=A^op) a.
 
 Definition yon_equiv_0gpd {A : Type} `{HasEquivs A}
   {a b : A}
-  : yon_0gpd a $<~> yon_0gpd b -> a $<~> b
+  : yon1_0gpd a $<~> yon1_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
+  : a $<~> b -> yon1_0gpd a $<~> yon1_0gpd b
   := natequiv_opyon_equiv_0gpd (A:=A^op).

From 8294fa6451b9e962aa34e7d848a85f9cec900e1c Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Tue, 26 Sep 2023 13:43:50 -0400
Subject: [PATCH 8/8] WildCat/Equiv: add lots of lemmas

---
 theories/Basics/Notations.v |   1 +
 theories/WildCat/Core.v     |  20 ++---
 theories/WildCat/Equiv.v    | 148 ++++++++++++++++++++++++++++++++++++
 3 files changed, 160 insertions(+), 9 deletions(-)

diff --git a/theories/Basics/Notations.v b/theories/Basics/Notations.v
index 3bba75819ed..f88b7ded907 100644
--- a/theories/Basics/Notations.v
+++ b/theories/Basics/Notations.v
@@ -158,6 +158,7 @@ Reserved Infix "$o@" (at level 30).
 Reserved Infix "$@" (at level 30).
 Reserved Infix "$@L" (at level 30).
 Reserved Infix "$@R" (at level 30).
+Reserved Infix "$@@" (at level 30).
 Reserved Infix "$=>" (at level 99).
 Reserved Notation "T ^op" (at level 3, format "T ^op").
 Reserved Notation "f ^-1$" (at level 3, format "f '^-1$'").
diff --git a/theories/WildCat/Core.v b/theories/WildCat/Core.v
index 14b21db99fb..a5f5995f2b6 100644
--- a/theories/WildCat/Core.v
+++ b/theories/WildCat/Core.v
@@ -117,15 +117,7 @@ Definition cat_assoc_opp {A : Type} `{Is1Cat A}
   : h $o (g $o f) $== (h $o g) $o f
   := (cat_assoc f g h)^$.
 
-(*
-Definition Comp2 {A} `{Is1Cat A} {a b c : A}
-           {f g : a $-> b} {h k : b $-> c}
-           (q : h $-> k) (p : f $-> g)
-  : (h $o f $-> k $o g)
-  := ??
-
-Infix "$o@" := Comp2.
-*)
+(** Whiskering and horizontal composition of 2-cells. *)
 
 Definition cat_postwhisker {A} `{Is1Cat A} {a b c : A}
            {f g : a $-> b} (h : b $-> c) (p : f $== g)
@@ -139,6 +131,16 @@ Definition cat_prewhisker {A} `{Is1Cat A} {a b c : A}
   := fmap (cat_precomp c h) p.
 Notation "p $@R h" := (cat_prewhisker p h).
 
+Definition cat_comp2 {A} `{Is1Cat A} {a b c : A}
+  {f g : a $-> b} {h k : b $-> c}
+  (p : f $== g) (q : h $== k )
+  : h $o f $== k $o g
+  := (q $@R _) $@ (_ $@L p).
+
+Notation "q $@@ p" := (cat_comp2 q p).
+
+(** Monomorphisms and epimorphisms. *)
+
 Definition Monic {A} `{Is1Cat A} {b c: A} (f : b $-> c)
   := forall a (g h : a $-> b), f $o g $== f $o h -> g $== h.
 
diff --git a/theories/WildCat/Equiv.v b/theories/WildCat/Equiv.v
index 2eb14784d56..61ed7acdeb1 100644
--- a/theories/WildCat/Equiv.v
+++ b/theories/WildCat/Equiv.v
@@ -101,6 +101,39 @@ Proof.
   apply cate_buildequiv_fun'.
 Defined.
 
+(** If [g] is a section of an equivalence, then it is the inverse. *)
+Definition cate_inverse_sect {A} `{HasEquivs A} {a b} (f : a $<~> b)
+  (g : b $-> a) (p : f $o g $== Id b)
+  : cate_fun f^-1$ $== g.
+Proof.
+  refine ((cat_idr _)^$ $@ _).
+  refine ((_ $@L p^$) $@ _).
+  refine (cat_assoc_opp _ _ _ $@ _).
+  refine (cate_issect f $@R _ $@ _).
+  apply cat_idl.
+Defined.
+
+(** If [g] is a retraction of an equivalence, then it is the inverse. *)
+Definition cate_inverse_retr {A} `{HasEquivs A} {a b} (f : a $<~> b)
+  (g : b $-> a) (p : g $o f $== Id a)
+  : cate_fun f^-1$ $== g.
+Proof.
+  refine ((cat_idl _)^$ $@ _).
+  refine ((p^$ $@R _) $@ _).
+  refine (cat_assoc _ _ _ $@ _).
+  refine (_ $@L cate_isretr f $@ _).
+  apply cat_idr.
+Defined.
+
+(** It follows that the inverse of the equivalence you get by adjointification is homotopic to the inverse [g] provided. *)
+Definition cate_inv_adjointify {A} `{HasEquivs A} {a b : A}
+  (f : a $-> b) (g : b $-> a) (r : f $o g $== Id b) (s : g $o f $== Id a)
+  : cate_fun (cate_adjointify f g r s)^-1$ $== g.
+Proof.
+  apply cate_inverse_sect.
+  exact ((cate_buildequiv_fun f $@R _) $@ r).
+Defined.
+
 (** The identity morphism is an equivalence *)
 Global Instance catie_id {A} `{HasEquivs A} (a : A)
   : CatIsEquiv (Id a)
@@ -211,6 +244,81 @@ Definition compose_hV_h {A} `{HasEquivs A} {a b c : A} (f : b $-> c) (g : b $<~>
   (f $o g^-1$) $o g $== f :=
   cat_assoc _ _ _ $@ (f $@L cate_issect g) $@ cat_idr f.
 
+(** Equivalences are both monomorphisms and epimorphisms (but not the converse). *)
+
+Definition cate_monic_equiv {A} `{HasEquivs A} {a b : A} (e : a $<~> b)
+  : Monic e.
+Proof.
+  intros c f g p.
+  refine ((compose_V_hh e _)^$ $@ _ $@ compose_V_hh e _).
+  exact (_ $@L p).
+Defined.
+
+Definition cate_epic_equiv {A} `{HasEquivs A} {a b : A} (e : a $<~> b)
+  : Epic e.
+Proof.
+  intros c f g p.
+  refine ((compose_hh_V _ e)^$ $@ _ $@ compose_hh_V _ e).
+  exact (p $@R _).
+Defined.
+
+(** Some lemmas for moving equivalences around.  Naming based on EquivGroupoids.v.  More could be added. *)
+
+Definition cate_moveL_V1 {A} `{HasEquivs A} {a b : A} {e : a $<~> b} (f : b $-> a)
+  (p : e $o f $== Id _)
+  : f $== cate_fun e^-1$.
+Proof.
+  apply (cate_monic_equiv e).
+  exact (p $@ (cate_isretr e)^$).
+Defined.
+
+Definition cate_moveL_1V {A} `{HasEquivs A} {a b : A} {e : a $<~> b} (f : b $-> a)
+  (p : f $o e $== Id _)
+  : f $== cate_fun e^-1$.
+Proof.
+  apply (cate_epic_equiv e).
+  exact (p $@ (cate_issect e)^$).
+Defined.
+
+Definition cate_moveR_V1 {A} `{HasEquivs A} {a b : A} {e : a $<~> b} (f : b $-> a)
+  (p : Id _ $== e $o f)
+  : cate_fun e^-1$ $== f.
+Proof.
+  apply (cate_monic_equiv e).
+  exact (cate_isretr e $@ p).
+Defined.
+
+Definition cate_moveR_1V {A} `{HasEquivs A} {a b : A} {e : a $<~> b} (f : b $-> a)
+  (p : Id _ $== f $o e)
+  : cate_fun e^-1$ $== f.
+Proof.
+  apply (cate_epic_equiv e).
+  exact (cate_issect e $@ p).
+Defined.
+
+(** Lemmas about the underlying map of an equivalence. *)
+
+Definition cate_inv2 {A} `{HasEquivs A} {a b : A} {e f : a $<~> b} (p : cate_fun e $== cate_fun f)
+  : cate_fun e^-1$ $== cate_fun f^-1$.
+Proof.
+  apply cate_moveL_V1.
+  exact ((p^$ $@R _) $@ cate_isretr _).
+Defined.
+
+Definition cate_inv_compose {A} `{HasEquivs A} {a b c : A} (e : a $<~> b) (f : b $<~> c)
+  : cate_fun (f $oE e)^-1$ $== cate_fun (e^-1$ $oE f^-1$).
+Proof.
+  refine (_ $@ (compose_cate_fun _ _)^$).
+  apply cate_inv_adjointify.
+Defined.
+
+Definition cate_inv_V {A} `{HasEquivs A} {a b : A} (e : a $<~> b)
+  : cate_fun (e^-1$)^-1$ $== cate_fun e.
+Proof.
+  apply cate_moveR_V1.
+  symmetry; apply cate_issect.
+Defined.
+
 (** Any sufficiently coherent functor preserves equivalences.  *)
 Global Instance iemap {A B : Type} `{HasEquivs A} `{HasEquivs B}
        (F : A -> B) `{!Is0Functor F, !Is1Functor F}
@@ -228,6 +336,46 @@ Definition emap {A B : Type} `{HasEquivs A} `{HasEquivs B}
   : F a $<~> F b
   := Build_CatEquiv (fmap F f).
 
+Definition emap_id {A B : Type} `{HasEquivs A} `{HasEquivs B}
+  (F : A -> B) `{!Is0Functor F, !Is1Functor F} {a : A}
+  : cate_fun (emap F (id_cate a)) $== cate_fun (id_cate (F a)).
+Proof.
+  refine (cate_buildequiv_fun _ $@ _).
+  refine (fmap2 F (id_cate_fun a) $@ _ $@ (id_cate_fun (F a))^$).
+  rapply fmap_id.
+Defined.
+
+Definition emap_compose {A B : Type} `{HasEquivs A} `{HasEquivs B}
+  (F : A -> B) `{!Is0Functor F, !Is1Functor F}
+  {a b c : A} (f : a $<~> b) (g : b $<~> c)
+  : cate_fun (emap F (g $oE f)) $== fmap F (cate_fun g) $o fmap F (cate_fun f).
+Proof.
+  refine (cate_buildequiv_fun _ $@ _).
+  refine (fmap2 F (compose_cate_fun _ _) $@ _).
+  rapply fmap_comp.
+Defined.
+
+(** A variant. *)
+Definition emap_compose' {A B : Type} `{HasEquivs A} `{HasEquivs B}
+  (F : A -> B) `{!Is0Functor F, !Is1Functor F}
+  {a b c : A} (f : a $<~> b) (g : b $<~> c)
+  : cate_fun (emap F (g $oE f)) $== cate_fun ((emap F g) $oE (emap F f)).
+Proof.
+  refine (emap_compose F f g $@ _).
+  symmetry.
+  refine (compose_cate_fun _ _ $@ _).
+  exact (cate_buildequiv_fun _ $@@ cate_buildequiv_fun _).
+Defined.
+
+Definition emap_inv {A B : Type} `{HasEquivs A} `{HasEquivs B}
+  (F : A -> B) `{!Is0Functor F, !Is1Functor F}
+  {a b : A} (e : a $<~> b)
+  : cate_fun (emap F e)^-1$ $== cate_fun (emap F e^-1$).
+Proof.
+  refine (cate_inv_adjointify _ _ _ _ $@ _).
+  exact (cate_buildequiv_fun _)^$.
+Defined.
+
 (** When we have equivalences, we can define what it means for a category to be univalent. *)
 Definition cat_equiv_path {A : Type} `{HasEquivs A} (a b : A)
   : (a = b) -> (a $<~> b).