From 63e3847b8aa47556fa710b7320c13a0d846bf83e Mon Sep 17 00:00:00 2001
From: gio256 <102917377+gio256@users.noreply.github.com>
Date: Thu, 7 Mar 2024 14:09:58 -0700
Subject: [PATCH 01/25] Move bifunctor coherence to Is1Bifunctor

---
 contrib/SetoidRewrite.v           |   4 +-
 theories/Algebra/AbGroups/AbHom.v |   9 +-
 theories/Algebra/AbSES/BaerSum.v  |  37 +++++---
 theories/Algebra/AbSES/Ext.v      |  17 ++--
 theories/Homotopy/Join/Core.v     |  21 ++++-
 theories/WildCat/Bifunctor.v      | 149 +++++++++++++++++++++++-------
 theories/WildCat/Monoidal.v       |   2 +-
 theories/WildCat/Products.v       |  22 ++---
 8 files changed, 181 insertions(+), 80 deletions(-)

diff --git a/contrib/SetoidRewrite.v b/contrib/SetoidRewrite.v
index c37b5d5f8f3..83fcfbbf3bb 100644
--- a/contrib/SetoidRewrite.v
+++ b/contrib/SetoidRewrite.v
@@ -122,9 +122,7 @@ Defined.
 #[export] Instance Is1Functor_uncurry_bifunctor {A B C : Type}
   `{Is1Cat A, Is1Cat B, Is1Cat C}
   (F : A -> B -> C)
-  `{!IsBifunctor F}
-  `{forall a, Is1Functor (F a)}
-  `{forall b, Is1Functor (flip F b)}
+  `{!Is0Bifunctor F, !Is1Bifunctor F}
   : Is1Functor (uncurry F).
 Proof.
   nrapply Build_Is1Functor.
diff --git a/theories/Algebra/AbGroups/AbHom.v b/theories/Algebra/AbGroups/AbHom.v
index 012e958a171..98e3da60140 100644
--- a/theories/Algebra/AbGroups/AbHom.v
+++ b/theories/Algebra/AbGroups/AbHom.v
@@ -63,13 +63,10 @@ Proof.
   by apply equiv_path_grouphomomorphism.
 Defined.
 
-Global Instance isbifunctor_ab_hom `{Funext}
-  : IsBifunctor (ab_hom : Group^op -> AbGroup -> AbGroup).
+Global Instance is0bifunctor_ab_hom `{Funext}
+  : Is0Bifunctor (ab_hom : Group^op -> AbGroup -> AbGroup).
 Proof.
-  snrapply Build_IsBifunctor.
-  1-2: exact _.
-  intros A A' f B B' g phi; cbn.
-  by apply equiv_path_grouphomomorphism.
+  rapply Build_Is0Bifunctor.
 Defined.
 
 (** ** Properties of [ab_hom] *)
diff --git a/theories/Algebra/AbSES/BaerSum.v b/theories/Algebra/AbSES/BaerSum.v
index 6e77c489d91..dae3f7f790d 100644
--- a/theories/Algebra/AbSES/BaerSum.v
+++ b/theories/Algebra/AbSES/BaerSum.v
@@ -51,11 +51,18 @@ Proof.
   apply abses_pushout_pullback_reorder'.
 Defined.
 
-Global Instance isbifunctor_abses' `{Univalence}
-  : IsBifunctor (AbSES' : AbGroup^op -> AbGroup -> Type).
+Global Instance is0bifunctor_abses' `{Univalence}
+  : Is0Bifunctor (AbSES' : AbGroup^op -> AbGroup -> Type).
 Proof.
-  eapply Build_IsBifunctor.
-  intros ? ? g ? ? f E; cbn.
+  rapply Build_Is0Bifunctor.
+Defined.
+
+Global Instance is1bifunctor_abses' `{Univalence}
+  : Is1Bifunctor (AbSES' : AbGroup^op -> AbGroup -> Type).
+Proof.
+  snrapply Build_Is1Bifunctor.
+  1,2: exact _.
+  - intros ? ? g ? ? f E; cbn.
   apply abses_pushout_pullback_reorder.
 Defined.
 
@@ -222,15 +229,21 @@ Proof.
   - intro; apply baer_sum_unit_r.
 Defined.
 
-Global Instance isbifunctor_abses `{Univalence}
-  : IsBifunctor (AbSES : AbGroup^op -> AbGroup -> pType).
+Global Instance is0bifunctor_abses `{Univalence}
+  : Is0Bifunctor (AbSES : AbGroup^op -> AbGroup -> pType).
 Proof.
-  econstructor.
-  intros ? ? f ? ? g.
-  rapply hspace_phomotopy_from_homotopy.
-  1: apply ishspace_abses.
-  intro E; cbn.
-  apply abses_pushout_pullback_reorder.
+  rapply Build_Is0Bifunctor.
+Defined.
+
+Global Instance is1bifunctor_abses `{Univalence}
+  : Is1Bifunctor (AbSES : AbGroup^op -> AbGroup -> Type).
+Proof.
+  snrapply Build_Is1Bifunctor.
+  (*TODO: why does typeclass search find is1functor_abses' lemmas here? *)
+  - intro; exact is1functor_abses'01.
+  - exact _.
+  - intros ? ? f ? ? g E; cbn.
+    apply abses_pushout_pullback_reorder.
 Defined.
 
 (** ** Pushouts and pullbacks respect the Baer sum *)
diff --git a/theories/Algebra/AbSES/Ext.v b/theories/Algebra/AbSES/Ext.v
index 5f937264e2a..a6b3d034dea 100644
--- a/theories/Algebra/AbSES/Ext.v
+++ b/theories/Algebra/AbSES/Ext.v
@@ -24,9 +24,9 @@ Defined.
 
 Definition Ext' (B A : AbGroup@{u}) := Tr 0 (AbSES' B A).
 
-Global Instance isbifunctor_ext'@{u v w | u < v, v < w} `{Univalence}
-  : IsBifunctor@{v v w u u v v} (Ext' : AbGroup@{u}^op -> AbGroup@{u} -> Type@{v})
-  := isbifunctor_compose _ _ (P:=isbifunctor_abses').
+Global Instance is0bifunctor_ext'@{u v w | u < v, v < w} `{Univalence}
+  : Is0Bifunctor@{v v w u u v} (Ext' : AbGroup@{u}^op -> AbGroup@{u} -> Type@{v})
+  := is0bifunctor_compose _ _ (bf:=isbifunctor_abses').
 
 (** [Ext B A] is an abelian group for any [A B : AbGroup]. The proof of commutativity is a bit faster if we separate out the proof that [Ext B A] is a group. *)
 Definition grp_ext `{Univalence} (B A : AbGroup@{u}) : Group.
@@ -84,15 +84,10 @@ Proof.
   apply baer_sum_pullback.
 Defined.
 
-Global Instance isbifunctor_ext `{Univalence}
-  : IsBifunctor (A:=AbGroup^op) ab_ext.
+Global Instance is0bifunctor_ext `{Univalence}
+  : Is0Bifunctor (A:=AbGroup^op) ab_ext.
 Proof.
-  snrapply Build_IsBifunctor.
-  1,2: exact _.
-  intros B B' f A A' g.
-  rapply Trunc_ind; intro E.
-  apply (ap tr).
-  apply abses_pushout_pullback_reorder.
+  rapply Build_Is0Bifunctor.
 Defined.
 
 (** We can push out a fixed extension while letting the map vary, and this defines a group homomorphism. *)
diff --git a/theories/Homotopy/Join/Core.v b/theories/Homotopy/Join/Core.v
index cb67d362cc3..d0a360f44c1 100644
--- a/theories/Homotopy/Join/Core.v
+++ b/theories/Homotopy/Join/Core.v
@@ -560,13 +560,30 @@ Section FunctorJoin.
   Definition equiv_functor_join {A B C D} (f : A <~> C) (g : B <~> D)
     : Join A B <~> Join C D := Build_Equiv _ _ (functor_join f g) _.
 
-  Global Instance isbifunctor_join : IsBifunctor Join.
+  Global Instance is0bifunctor_join : Is0Bifunctor Join.
   Proof.
-    snrapply Build_IsBifunctor.
+    snrapply Build_Is0Bifunctor.
     - intro A; snrapply Build_Is0Functor; intros B D g.
       exact (functor_join idmap g).
     - intro B; snrapply Build_Is0Functor; intros A C f.
       exact (functor_join f idmap).
+  Defined.
+
+  Global Instance is1bifunctor_join : Is1Bifunctor Join.
+  Proof.
+    snrapply Build_Is1Bifunctor.
+    - intro A; snrapply Build_Is1Functor.
+      + intros B C f g p.
+        exact (functor2_join (fun _ => 1) p).
+      + intro B; exact functor_join_idmap.
+      + intros B C D f g.
+        exact (functor_join_compose idmap f idmap g).
+    - intro B; snrapply Build_Is1Functor.
+      + intros A C f g p.
+        exact (functor2_join p (fun _ => 1)).
+      + intro A; exact functor_join_idmap.
+      + intros A C D f g.
+        exact (functor_join_compose f idmap g idmap).
     - intros A C f B D g x.
       lhs_V nrapply functor_join_compose.
       nrapply functor_join_compose.
diff --git a/theories/WildCat/Bifunctor.v b/theories/WildCat/Bifunctor.v
index f3b61d08252..6f0bc9f12dc 100644
--- a/theories/WildCat/Bifunctor.v
+++ b/theories/WildCat/Bifunctor.v
@@ -4,27 +4,25 @@ Require Import WildCat.Core WildCat.Opposite WildCat.Universe WildCat.Prod.
 
 (** * Bifunctors between WildCats *)
 
-Class IsBifunctor {A B C : Type} `{IsGraph A, IsGraph B, Is1Cat C}
+Class Is0Bifunctor {A B C : Type} `{IsGraph A, IsGraph B, IsGraph C}
   (F : A -> B -> C)
   := {
-    bifunctor_isfunctor_10 : forall a, Is0Functor (F a);
-    bifunctor_isfunctor_01 : forall b, Is0Functor (flip F b);
-    bifunctor_isbifunctor : forall a0 a1 (f : a0 $-> a1) b0 b1 (g : b0 $-> b1),
-      fmap (F _) g $o fmap (flip F _) f $== fmap (flip F _) f $o fmap (F _) g
+    bifunctor_is0functor01 :: forall a, Is0Functor (F a);
+    bifunctor_is0functor10 :: forall b, Is0Functor (flip F b);
   }.
 
-#[export] Existing Instance bifunctor_isfunctor_10.
-#[export] Existing Instance bifunctor_isfunctor_01.
-Arguments bifunctor_isbifunctor {A B C} {_ _ _ _ _ _}
-  F {_} {a0 a1} f {b0 b1} g.
-
 Class Is1Bifunctor {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
-  (F : A -> B -> C) `{!IsBifunctor F}
+  (F : A -> B -> C) `{!Is0Bifunctor F}
   := {
-    bifunctor_is1functor_10 :: forall a : A, Is1Functor (F a);
-    bifunctor_is1functor_01 :: forall b : B, Is1Functor (flip F b);
+    bifunctor_is1functor01 :: forall a : A, Is1Functor (F a);
+    bifunctor_is1functor10 :: forall b : B, Is1Functor (flip F b);
+    bifunctor_isbifunctor : forall a0 a1 (f : a0 $-> a1) b0 b1 (g : b0 $-> b1),
+      fmap (F _) g $o fmap (flip F _) f $== fmap (flip F _) f $o fmap (F _) g
   }.
 
+Arguments bifunctor_isbifunctor {A B C} {_ _ _ _ _ _ _ _ _ _ _ _}
+  F {_ _} {a0 a1} f {b0 b1} g.
+
 Definition bifunctor_hom {C : Type} `{IsGraph C}
   : C^op -> C -> Type := @Hom C _.
 
@@ -44,43 +42,35 @@ Proof.
   exact f.
 Defined.
 
-(** [Hom] is a bifunctor whenever [C] is a strong 1-category. *)
-Global Instance isbifunctor_hom {C : Type} `{Is1Cat_Strong C}
-  : IsBifunctor (bifunctor_hom (C:=C)).
+Global Instance is0bifunctor_hom {C : Type} `{Is1Cat C}
+  : Is0Bifunctor (bifunctor_hom (C:=C)).
 Proof.
-  srapply Build_IsBifunctor.
-  intros ? ? f ? ? g x; cbn.
-  unfold cat_precomp, cat_postcomp.
-  symmetry; apply cat_assoc_strong.
+  rapply Build_Is0Bifunctor.
 Defined.
 
 Definition fmap01 {A B C : Type} `{Is01Cat A, Is01Cat B, Is1Cat C}
-  (F : A -> B -> C) `{!IsBifunctor F}
+  (F : A -> B -> C) `{!Is0Bifunctor F}
   (a : A) {b0 b1 : B} (g : b0 $-> b1)
   : F a b0 $-> F a b1 := fmap (F a) g.
 
 Definition fmap10 {A B C : Type} `{Is01Cat A, Is01Cat B, Is1Cat C}
-  (F : A -> B -> C) `{!IsBifunctor F}
+  (F : A -> B -> C) `{!Is0Bifunctor F}
   {a0 a1 : A} (f : a0 $-> a1) (b : B)
   : (F a0 b) $-> (F a1 b) := fmap (flip F b) f.
 
-Global Instance isbifunctor_compose {A B C D : Type}
+Global Instance is0bifunctor_compose {A B C D : Type}
   `{IsGraph A, IsGraph B, Is1Cat C, Is1Cat D}
   (F : A -> B -> C) (G : C -> D) `{!Is0Functor G, !Is1Functor G}
-  `{P : !IsBifunctor F}
-  : IsBifunctor (fun a b => G (F a b)).
+  `{bf : !Is0Bifunctor F}
+  : Is0Bifunctor (fun a b => G (F a b)).
 Proof.
-  srapply Build_IsBifunctor.
-  intros ? ? f ? ? g; cbn.
-  refine ((fmap_comp G _ _)^$ $@ _ $@ fmap_comp G _ _).
-  rapply fmap2.
-  apply P.
+  rapply Build_Is0Bifunctor.
 Defined.
 
 Global Instance is1bifunctor_compose {A B C D : Type}
   `{Is1Cat A, Is1Cat B, Is1Cat C, Is1Cat D}
   (F : A -> B -> C) (G : C -> D) `{!Is0Functor G, !Is1Functor G}
-  `{!IsBifunctor F, !Is1Bifunctor F}
+  `{!Is0Bifunctor F, !Is1Bifunctor F}
   : Is1Bifunctor (fun a b => G (F a b)).
 Proof.
   nrapply Build_Is1Bifunctor.
@@ -102,10 +92,15 @@ Proof.
     + intros a b c f g.
       refine (fmap2 G (fmap_comp (flip F y) f g) $@ _).
       exact (fmap_comp G _ _).
+  - intros a0 a1 f b0 b1 g; cbn.
+    refine ((fmap_comp G _ _)^$ $@ _ $@ fmap_comp G _ _).
+    rapply fmap2.
+    cbn.
+    exact (bifunctor_isbifunctor F f g).
 Defined.
 
-(** There are two possible ways to define this, which will only agree in the event that F is a bifunctor. *)
-#[export] Instance Is0Functor_uncurry_bifunctor {A B C : Type}
+(** There are two possible ways to define this, which will only agree in the event that the bifunctor coherence condition ([bifunctor_isbifunctor]) holds. *)
+Global Instance is0functor_uncurry_bifunctor {A B C : Type}
   `{IsGraph A, IsGraph B, Is1Cat C}
   (F : A -> B -> C)
   `{forall a, Is0Functor (F a), forall b, Is0Functor (flip F b)}
@@ -119,7 +114,7 @@ Defined.
 
 Global Instance is1functor_uncurry_bifunctor {A B C : Type}
   `{Is1Cat A, Is1Cat B, Is1Cat C} (F : A -> B -> C)
-  `{!IsBifunctor F, !Is1Bifunctor F}
+  `{!Is0Bifunctor F, !Is1Bifunctor F}
   : Is1Functor (uncurry F).
 Proof.
   nrapply Build_Is1Functor.
@@ -136,3 +131,89 @@ Proof.
     refine (cat_assoc _ _ _ $@R _ $@ _ $@ (cat_assoc_opp _ _ _ $@R _)).
     exact (_ $@L (bifunctor_isbifunctor F _ _)^$ $@R _).
 Defined.
+
+(** *** Uncurried bifunctors are functorial in each argument. *)
+
+Global Instance is0functor_bifunctor_uncurried01 {A B C : Type}
+  `{Is01Cat A} `{IsGraph B} `{IsGraph C}
+  (F : A * B -> C) `{!Is0Functor F} (a : A)
+  : Is0Functor (fun b => F (a, b)).
+Proof.
+  apply Build_Is0Functor.
+  intros x y f.
+  rapply (fmap F).
+  exact (Id a, f).
+Defined.
+
+Global Instance is1functor_bifunctor_uncurried01 {A B C : Type}
+  `{Is1Cat A} `{Is1Cat B} `{Is1Cat C}
+  (F : A * B -> C) `{!Is0Functor F, !Is1Functor F} (a : A)
+  : Is1Functor (fun b => F (a, b)).
+Proof.
+  apply Build_Is1Functor.
+  - intros x y f g p.
+    rapply (fmap2 F).
+    exact (Id _, p).
+  - intros b.
+    exact (fmap_id F (a, b)).
+  - intros x y z f g.
+    refine (_ $@ _).
+    2: rapply (fmap_comp F).
+    rapply (fmap2 F).
+    exact ((cat_idl (Id a))^$, Id _).
+Defined.
+
+Global Instance is0functor_bifunctor_uncurried10 {A B C : Type}
+  `{IsGraph A} `{Is01Cat B} `{IsGraph C}
+  (F : A * B -> C) `{!Is0Functor F} (b : B)
+  : Is0Functor (fun a => F (a, b)).
+Proof.
+  apply Build_Is0Functor.
+  intros x y f.
+  rapply (fmap F).
+  exact (f, Id b).
+Defined.
+
+Global Instance is1functor_bifunctor_uncurried10 {A B C : Type}
+  `{Is1Cat A} `{Is1Cat B} `{Is1Cat C}
+  (F : A * B -> C) `{!Is0Functor F, !Is1Functor F} (b : B)
+  : Is1Functor (fun a => F (a, b)).
+Proof.
+  apply Build_Is1Functor.
+  - intros x y f g p.
+    rapply (fmap2 F).
+    exact (p, Id _).
+  - intros a.
+    exact (fmap_id F (a, b)).
+  - intros x y z f g.
+    refine (_ $@ _).
+    2: rapply (fmap_comp F).
+    rapply (fmap2 F).
+    exact (Id _, (cat_idl _)^$).
+Defined.
+
+Global Instance is0bifunctor_bifunctor_uncurried {A B C : Type}
+  `{Is01Cat A, Is01Cat B, IsGraph C}
+  (F : A * B -> C) `{!Is0Functor F}
+  : Is0Bifunctor (fun a b => F (a, b)).
+Proof.
+  rapply Build_Is0Bifunctor.
+Defined.
+
+Global Instance is1bifunctor_bifunctor_uncurried {A B C : Type}
+  `{Is1Cat A, Is1Cat B, Is1Cat C}
+  (F : A * B -> C) `{!Is0Functor F, !Is1Functor F}
+  : Is1Bifunctor (fun a b => F (a, b)).
+Proof.
+  apply Build_Is1Bifunctor.
+  - intros a.
+    exact (is1functor_bifunctor_uncurried01 F a).
+  - intros b.
+    exact (is1functor_bifunctor_uncurried10 F b).
+  - intros a b f c d g.
+    refine ((fmap_comp F _ _)^$ $@ _).
+    refine (_ $@ (fmap_comp F _ _)).
+    rapply (fmap2 F).
+    refine (cat_idl f $@ (cat_idr f)^$, _).
+    exact (cat_idr g $@ (cat_idl g)^$).
+Defined.
diff --git a/theories/WildCat/Monoidal.v b/theories/WildCat/Monoidal.v
index 4200aefe8ef..55477f16280 100644
--- a/theories/WildCat/Monoidal.v
+++ b/theories/WildCat/Monoidal.v
@@ -8,7 +8,7 @@ Section Monoidal.
   Context `{Is1Cat C}.
   Context `{HasEquivs C}.
   Context (tensor : C -> C -> C).
-  Context `{!IsBifunctor tensor}.
+  Context `{!Is0Bifunctor tensor}.
 
   Definition left_assoc : C -> C -> C -> C :=
     fun a b c => tensor (tensor a b) c.
diff --git a/theories/WildCat/Products.v b/theories/WildCat/Products.v
index cdc11cfb12f..76c5f04277d 100644
--- a/theories/WildCat/Products.v
+++ b/theories/WildCat/Products.v
@@ -427,9 +427,9 @@ End Symmetry.
 
 (** We prove bifunctoriality of [cat_binprod : A -> A -> A] by factoring it as [cat_prod Bool o Bool_rec A]. First, we prove that [Bool_rec A : A -> A -> (Bool -> A)] is a bifunctor. *)
 Local Instance is0bifunctor_boolrec {A : Type} `{Is1Cat A}
-  : IsBifunctor (Bool_rec A).
+  : Is0Bifunctor (Bool_rec A).
 Proof.
-  snrapply Build_IsBifunctor.
+  snrapply Build_Is0Bifunctor.
   - intros x.
     nrapply Build_Is0Functor.
     intros a b f [|].
@@ -440,9 +440,6 @@ Proof.
     intros a b f [|].
     + exact f.
     + reflexivity.
-  - intros a a' f b b' g [|].
-    + exact (cat_idl _ $@ (cat_idr _)^$).
-    + exact (cat_idr _ $@ (cat_idl _)^$).
 Defined.
 
 Local Instance is1bifunctor_boolrec {A : Type} `{Is1Cat A}
@@ -467,14 +464,17 @@ Proof.
     + intros a b c f g [|].
       1: reflexivity.
       exact (cat_idl _)^$.
+  - intros a a' f b b' g [|].
+    + exact (cat_idl _ $@ (cat_idr _)^$).
+    + exact (cat_idr _ $@ (cat_idl _)^$).
 Defined.
 
 (** As a special case of the product functor, restriction along [Bool_rec A] yields bifunctoriality of [cat_binprod]. *)
 Global Instance isbifunctor_cat_binprod {A : Type} `{HasBinaryProducts A}
-  : IsBifunctor (fun x y => cat_binprod x y).
+  : Is0Bifunctor (fun x y => cat_binprod x y).
 Proof.
   pose (p:=@has_products _ _ _ _ _ _ hasproductsbool_hasbinaryproducts).
-  exact (isbifunctor_compose
+  exact (is0bifunctor_compose
           (Bool_rec A) (fun x => cat_prod Bool x (product:=p x))).
 Defined.
 
@@ -491,28 +491,28 @@ Global Instance is0functor_cat_binprod_l {A : Type} `{HasBinaryProducts A}
   (y : A)
   : Is0Functor (fun x => cat_binprod x y).
 Proof.
-  exact (bifunctor_isfunctor_01 y).
+  exact (bifunctor_is0functor10 y).
 Defined.
 
 Global Instance is1functor_cat_binprod_l {A : Type} `{HasBinaryProducts A}
   (y : A)
   : Is1Functor (fun x => cat_binprod x y).
 Proof.
-  exact (bifunctor_is1functor_01 y).
+  exact (bifunctor_is1functor10 y).
 Defined.
 
 Global Instance is0functor_cat_binprod_r {A : Type} `{HasBinaryProducts A}
   (x : A)
   : Is0Functor (fun y => cat_binprod x y).
 Proof.
-  exact (bifunctor_isfunctor_10 x).
+  exact (bifunctor_is0functor01 x).
 Defined.
 
 Global Instance is1functor_cat_binprod_r {A : Type} `{HasBinaryProducts A}
   (x : A)
   : Is1Functor (fun y => cat_binprod x y).
 Proof.
-  exact (bifunctor_is1functor_10 x).
+  exact (bifunctor_is1functor01 x).
 Defined.
 
 (** [cat_binprod_corec] is also functorial in each morphsism. *)

From 783f5b96dd0124ec2c7c33b8e78294db405c72fd Mon Sep 17 00:00:00 2001
From: gio256 <102917377+gio256@users.noreply.github.com>
Date: Thu, 7 Mar 2024 17:59:58 -0700
Subject: [PATCH 02/25] WildCat/Bifunctor.v: Remove bifunctor_hom lemmas

---
 theories/Algebra/AbSES/Ext.v |  2 +-
 theories/WildCat/Bifunctor.v | 25 -------------------------
 2 files changed, 1 insertion(+), 26 deletions(-)

diff --git a/theories/Algebra/AbSES/Ext.v b/theories/Algebra/AbSES/Ext.v
index a6b3d034dea..9b2abed7019 100644
--- a/theories/Algebra/AbSES/Ext.v
+++ b/theories/Algebra/AbSES/Ext.v
@@ -26,7 +26,7 @@ Definition Ext' (B A : AbGroup@{u}) := Tr 0 (AbSES' B A).
 
 Global Instance is0bifunctor_ext'@{u v w | u < v, v < w} `{Univalence}
   : Is0Bifunctor@{v v w u u v} (Ext' : AbGroup@{u}^op -> AbGroup@{u} -> Type@{v})
-  := is0bifunctor_compose _ _ (bf:=isbifunctor_abses').
+  := is0bifunctor_compose _ _ (bf:=is0bifunctor_abses').
 
 (** [Ext B A] is an abelian group for any [A B : AbGroup]. The proof of commutativity is a bit faster if we separate out the proof that [Ext B A] is a group. *)
 Definition grp_ext `{Univalence} (B A : AbGroup@{u}) : Group.
diff --git a/theories/WildCat/Bifunctor.v b/theories/WildCat/Bifunctor.v
index 6f0bc9f12dc..0a64afba1c2 100644
--- a/theories/WildCat/Bifunctor.v
+++ b/theories/WildCat/Bifunctor.v
@@ -23,31 +23,6 @@ Class Is1Bifunctor {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
 Arguments bifunctor_isbifunctor {A B C} {_ _ _ _ _ _ _ _ _ _ _ _}
   F {_ _} {a0 a1} f {b0 b1} g.
 
-Definition bifunctor_hom {C : Type} `{IsGraph C}
-  : C^op -> C -> Type := @Hom C _.
-
-Local Instance is0functor_hom01 {C : Type} `{Is1Cat C}
-  : forall c, Is0Functor (bifunctor_hom c).
-Proof.
-  intro c; srapply Build_Is0Functor.
-  rapply cat_postcomp.
-Defined.
-
-Local Instance is0functor_hom10 {C : Type} `{Is1Cat C}
-  : forall c, Is0Functor (flip bifunctor_hom c).
-Proof.
-  intro c; srapply Build_Is0Functor.
-  intros ? ? f; cbn.
-  rapply cat_precomp.
-  exact f.
-Defined.
-
-Global Instance is0bifunctor_hom {C : Type} `{Is1Cat C}
-  : Is0Bifunctor (bifunctor_hom (C:=C)).
-Proof.
-  rapply Build_Is0Bifunctor.
-Defined.
-
 Definition fmap01 {A B C : Type} `{Is01Cat A, Is01Cat B, Is1Cat C}
   (F : A -> B -> C) `{!Is0Bifunctor F}
   (a : A) {b0 b1 : B} (g : b0 $-> b1)

From a95509dab1351c59347fa9777999dcb1440e9431 Mon Sep 17 00:00:00 2001
From: gio256 <102917377+gio256@users.noreply.github.com>
Date: Fri, 8 Mar 2024 08:43:06 -0700
Subject: [PATCH 03/25] AbSES/BaerSum.v: fix proof of is1bifunctor_abses

---
 theories/Algebra/AbSES/BaerSum.v | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

diff --git a/theories/Algebra/AbSES/BaerSum.v b/theories/Algebra/AbSES/BaerSum.v
index dae3f7f790d..b77b057b127 100644
--- a/theories/Algebra/AbSES/BaerSum.v
+++ b/theories/Algebra/AbSES/BaerSum.v
@@ -62,8 +62,8 @@ Global Instance is1bifunctor_abses' `{Univalence}
 Proof.
   snrapply Build_Is1Bifunctor.
   1,2: exact _.
-  - intros ? ? g ? ? f E; cbn.
-  apply abses_pushout_pullback_reorder.
+  intros ? ? g ? ? f E; cbn.
+  exact (abses_pushout_pullback_reorder E f g).
 Defined.
 
 (** Given a short exact sequence [A -> E -> B] and maps [f : A -> A'], [g : B' -> B], we can change the order of pushing out along [f] and pulling back along [g]. *)
@@ -236,14 +236,15 @@ Proof.
 Defined.
 
 Global Instance is1bifunctor_abses `{Univalence}
-  : Is1Bifunctor (AbSES : AbGroup^op -> AbGroup -> Type).
+  : Is1Bifunctor (AbSES : AbGroup^op -> AbGroup -> pType).
 Proof.
   snrapply Build_Is1Bifunctor.
-  (*TODO: why does typeclass search find is1functor_abses' lemmas here? *)
-  - intro; exact is1functor_abses'01.
-  - exact _.
-  - intros ? ? f ? ? g E; cbn.
-    apply abses_pushout_pullback_reorder.
+  1,2: exact _.
+  intros ? ? f ? ? g.
+  rapply hspace_phomotopy_from_homotopy.
+  1: apply ishspace_abses.
+  intro E; cbn.
+  apply abses_pushout_pullback_reorder.
 Defined.
 
 (** ** Pushouts and pullbacks respect the Baer sum *)

From 1046b481feb25be68d293de0b2067474ff196838 Mon Sep 17 00:00:00 2001
From: gio256 <102917377+gio256@users.noreply.github.com>
Date: Fri, 8 Mar 2024 09:29:03 -0700
Subject: [PATCH 04/25] WildCat/Bifunctor.v: simplify uncurried proofs

---
 theories/WildCat/Bifunctor.v | 66 ++++++++++++++++--------------------
 1 file changed, 30 insertions(+), 36 deletions(-)

diff --git a/theories/WildCat/Bifunctor.v b/theories/WildCat/Bifunctor.v
index 0a64afba1c2..57e8a6ee19b 100644
--- a/theories/WildCat/Bifunctor.v
+++ b/theories/WildCat/Bifunctor.v
@@ -1,6 +1,6 @@
 Require Import Basics.Overture Basics.Tactics.
 Require Import Types.Forall.
-Require Import WildCat.Core WildCat.Opposite WildCat.Universe WildCat.Prod.
+Require Import WildCat.Core WildCat.Prod.
 
 (** * Bifunctors between WildCats *)
 
@@ -114,9 +114,10 @@ Global Instance is0functor_bifunctor_uncurried01 {A B C : Type}
   (F : A * B -> C) `{!Is0Functor F} (a : A)
   : Is0Functor (fun b => F (a, b)).
 Proof.
-  apply Build_Is0Functor.
-  intros x y f.
-  rapply (fmap F).
+  nrapply (is0functor_compose (fun b => (a, b)) F).
+  2: exact _.
+  nrapply Build_Is0Functor.
+  intros b c f.
   exact (Id a, f).
 Defined.
 
@@ -125,17 +126,14 @@ Global Instance is1functor_bifunctor_uncurried01 {A B C : Type}
   (F : A * B -> C) `{!Is0Functor F, !Is1Functor F} (a : A)
   : Is1Functor (fun b => F (a, b)).
 Proof.
-  apply Build_Is1Functor.
-  - intros x y f g p.
-    rapply (fmap2 F).
+  nrapply (is1functor_compose (fun b => (a, b)) F).
+  2: exact _.
+  nrapply Build_Is1Functor.
+  - intros b c f g p.
     exact (Id _, p).
-  - intros b.
-    exact (fmap_id F (a, b)).
-  - intros x y z f g.
-    refine (_ $@ _).
-    2: rapply (fmap_comp F).
-    rapply (fmap2 F).
-    exact ((cat_idl (Id a))^$, Id _).
+  - intros b; reflexivity.
+  - intros b c d f g.
+    exact ((cat_idl _)^$, Id _).
 Defined.
 
 Global Instance is0functor_bifunctor_uncurried10 {A B C : Type}
@@ -143,9 +141,10 @@ Global Instance is0functor_bifunctor_uncurried10 {A B C : Type}
   (F : A * B -> C) `{!Is0Functor F} (b : B)
   : Is0Functor (fun a => F (a, b)).
 Proof.
-  apply Build_Is0Functor.
-  intros x y f.
-  rapply (fmap F).
+  nrapply (is0functor_compose (fun a => (a, b)) F).
+  2: exact _.
+  nrapply Build_Is0Functor.
+  intros a c f.
   exact (f, Id b).
 Defined.
 
@@ -154,16 +153,14 @@ Global Instance is1functor_bifunctor_uncurried10 {A B C : Type}
   (F : A * B -> C) `{!Is0Functor F, !Is1Functor F} (b : B)
   : Is1Functor (fun a => F (a, b)).
 Proof.
-  apply Build_Is1Functor.
-  - intros x y f g p.
-    rapply (fmap2 F).
+  nrapply (is1functor_compose (fun a => (a, b)) F).
+  2: exact _.
+  nrapply Build_Is1Functor.
+  - intros a c f g p.
     exact (p, Id _).
-  - intros a.
-    exact (fmap_id F (a, b)).
-  - intros x y z f g.
-    refine (_ $@ _).
-    2: rapply (fmap_comp F).
-    rapply (fmap2 F).
+  - intros a; reflexivity.
+  - intros a c d f g.
+    cbn.
     exact (Id _, (cat_idl _)^$).
 Defined.
 
@@ -181,14 +178,11 @@ Global Instance is1bifunctor_bifunctor_uncurried {A B C : Type}
   : Is1Bifunctor (fun a b => F (a, b)).
 Proof.
   apply Build_Is1Bifunctor.
-  - intros a.
-    exact (is1functor_bifunctor_uncurried01 F a).
-  - intros b.
-    exact (is1functor_bifunctor_uncurried10 F b).
-  - intros a b f c d g.
-    refine ((fmap_comp F _ _)^$ $@ _).
-    refine (_ $@ (fmap_comp F _ _)).
-    rapply (fmap2 F).
-    refine (cat_idl f $@ (cat_idr f)^$, _).
-    exact (cat_idr g $@ (cat_idl g)^$).
+  1,2: exact _.
+  intros a b f c d g.
+  refine ((fmap_comp F _ _)^$ $@ _).
+  refine (_ $@ (fmap_comp F _ _)).
+  rapply (fmap2 F).
+  refine (cat_idl f $@ (cat_idr f)^$, _).
+  exact (cat_idr g $@ (cat_idl g)^$).
 Defined.

From 62b8d2b4ebbee7a758065b87c6052a4354b84ed9 Mon Sep 17 00:00:00 2001
From: gio256 <102917377+gio256@users.noreply.github.com>
Date: Fri, 8 Mar 2024 12:02:47 -0700
Subject: [PATCH 05/25] AbGroups/AbHom.v: prove is1bifunctor_ab_hom

---
 theories/Algebra/AbGroups/AbHom.v | 34 +++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)

diff --git a/theories/Algebra/AbGroups/AbHom.v b/theories/Algebra/AbGroups/AbHom.v
index 98e3da60140..fcc5b53dfbd 100644
--- a/theories/Algebra/AbGroups/AbHom.v
+++ b/theories/Algebra/AbGroups/AbHom.v
@@ -63,12 +63,46 @@ Proof.
   by apply equiv_path_grouphomomorphism.
 Defined.
 
+Global Instance is1functor_ab_hom01 `{Funext} {A : Group^op}
+  : Is1Functor (ab_hom A).
+Proof.
+  nrapply Build_Is1Functor.
+  - intros B B' f g p phi.
+    apply equiv_path_grouphomomorphism; intro a; cbn.
+    exact (p (phi a)).
+  - intros B phi.
+    by apply equiv_path_grouphomomorphism.
+  - intros B C D f g phi.
+    by apply equiv_path_grouphomomorphism.
+Defined.
+
+Global Instance is1functor_ab_hom10 `{Funext} {B : AbGroup@{u}}
+  : Is1Functor (flip (ab_hom : Group^op -> AbGroup -> AbGroup) B).
+Proof.
+  nrapply Build_Is1Functor.
+  - intros A A' f g p phi.
+    apply equiv_path_grouphomomorphism; intro a; cbn.
+    exact (ap phi (p a)).
+  - intros A phi.
+    by apply equiv_path_grouphomomorphism.
+  - intros A C D f g phi.
+    by apply equiv_path_grouphomomorphism.
+Defined.
+
 Global Instance is0bifunctor_ab_hom `{Funext}
   : Is0Bifunctor (ab_hom : Group^op -> AbGroup -> AbGroup).
 Proof.
   rapply Build_Is0Bifunctor.
 Defined.
 
+Global Instance is1bifunctor_ab_hom `{Funext}
+  : Is1Bifunctor (ab_hom : Group^op -> AbGroup -> AbGroup).
+Proof.
+  rapply Build_Is1Bifunctor.
+  intros A A' f B B' g phi; cbn.
+  by apply equiv_path_grouphomomorphism.
+Defined.
+
 (** ** Properties of [ab_hom] *)
 
 (** Precomposition with a surjection is an embedding. *)

From 720075a69b350f78529fbd310f00ed77e838c1ce Mon Sep 17 00:00:00 2001
From: gio256 <102917377+gio256@users.noreply.github.com>
Date: Fri, 8 Mar 2024 14:14:28 -0700
Subject: [PATCH 06/25] AbSES/Ext.v: rough proofs of Is1Bifunctor

---
 theories/Algebra/AbSES/Ext.v | 61 ++++++++++++++++++++++++++++++++++--
 theories/WildCat/Bifunctor.v |  2 +-
 2 files changed, 59 insertions(+), 4 deletions(-)

diff --git a/theories/Algebra/AbSES/Ext.v b/theories/Algebra/AbSES/Ext.v
index 9b2abed7019..4de575cb46c 100644
--- a/theories/Algebra/AbSES/Ext.v
+++ b/theories/Algebra/AbSES/Ext.v
@@ -2,7 +2,7 @@ Require Import Basics Types Truncations.Core.
 Require Import Pointed WildCat.
 Require Import Truncations.SeparatedTrunc.
 Require Import AbelianGroup AbHom AbProjective.
-Require Import AbSES.Pullback AbSES.BaerSum AbSES.Core.
+Require Import AbSES.Pullback AbSES.Pushout AbSES.BaerSum AbSES.Core.
 
 Local Open Scope mc_scope.
 Local Open Scope mc_add_scope.
@@ -28,6 +28,11 @@ Global Instance is0bifunctor_ext'@{u v w | u < v, v < w} `{Univalence}
   : Is0Bifunctor@{v v w u u v} (Ext' : AbGroup@{u}^op -> AbGroup@{u} -> Type@{v})
   := is0bifunctor_compose _ _ (bf:=is0bifunctor_abses').
 
+(**TODO: universes*)
+Global Instance is1bifunctor_ext'@{u v w | u < v, v < w} `{Univalence}
+  : Is1Bifunctor@{v v w u u v v u u} (Ext' : AbGroup@{u}^op -> AbGroup@{u} -> Type@{v})
+  := is1bifunctor_compose _ _ (bf:=is1bifunctor_abses').
+
 (** [Ext B A] is an abelian group for any [A B : AbGroup]. The proof of commutativity is a bit faster if we separate out the proof that [Ext B A] is a group. *)
 Definition grp_ext `{Univalence} (B A : AbGroup@{u}) : Group.
 Proof.
@@ -60,7 +65,7 @@ Proof.
   apply baer_sum_commutative.
 Defined.
 
-Global Instance is01functor_ext `{Univalence} (B : AbGroup^op)
+Global Instance is0functor_ext01 `{Univalence} (B : AbGroup^op)
   : Is0Functor (ab_ext B).
 Proof.
   srapply Build_Is0Functor; intros ? ? f.
@@ -72,7 +77,7 @@ Proof.
   apply baer_sum_pushout.
 Defined.
 
-Global Instance is10functor_ext `{Univalence} (A : AbGroup)
+Global Instance is0functor_ext10 `{Univalence} (A : AbGroup)
   : Is0Functor (fun B : AbGroup^op => ab_ext B A).
 Proof.
   srapply Build_Is0Functor; intros ? ? f; cbn.
@@ -84,12 +89,62 @@ Proof.
   apply baer_sum_pullback.
 Defined.
 
+Global Instance is1functor_ext01 `{Univalence} (B : AbGroup^op)
+  : Is1Functor (ab_ext B).
+Proof.
+  snrapply Build_Is1Functor.
+  - intros A C f g p x.
+    strip_truncations; cbn.
+    apply (ap tr).
+    apply abses_pushout_homotopic.
+    exact p.
+  - intros A x.
+    strip_truncations; cbn.
+    apply (ap tr).
+    apply abses_pushout_id.
+  - intros A C D f g x.
+    strip_truncations; cbn.
+    apply (ap tr).
+    apply abses_pushout_compose.
+Defined.
+
+Global Instance is1functor_ext10 `{Univalence} (A : AbGroup)
+  : Is1Functor (fun B : AbGroup^op => ab_ext B A).
+Proof.
+  snrapply Build_Is1Functor.
+  - intros B C f g p x.
+    strip_truncations; cbn.
+    apply (ap tr).
+    apply abses_pullback_homotopic.
+    exact p.
+  - intros B x.
+    strip_truncations; cbn.
+    apply (ap tr).
+    apply abses_pullback_id.
+  - intros B C D f g x.
+    strip_truncations; cbn.
+    apply (ap tr).
+    symmetry.
+    apply abses_pullback_compose.
+Defined.
+
 Global Instance is0bifunctor_ext `{Univalence}
   : Is0Bifunctor (A:=AbGroup^op) ab_ext.
 Proof.
   rapply Build_Is0Bifunctor.
 Defined.
 
+Global Instance is1bifunctor_ext `{Univalence}
+  : Is1Bifunctor (A:=AbGroup^op) ab_ext.
+Proof.
+  snrapply Build_Is1Bifunctor.
+  1,2: exact _.
+  intros B B' f A A' g.
+  rapply Trunc_ind; intro E.
+  apply (ap tr).
+  apply abses_pushout_pullback_reorder.
+Defined.
+
 (** We can push out a fixed extension while letting the map vary, and this defines a group homomorphism. *)
 Definition abses_pushout_ext `{Univalence}
   {B A G : AbGroup@{u}} (E : AbSES B A)
diff --git a/theories/WildCat/Bifunctor.v b/theories/WildCat/Bifunctor.v
index 57e8a6ee19b..b234d7c4401 100644
--- a/theories/WildCat/Bifunctor.v
+++ b/theories/WildCat/Bifunctor.v
@@ -45,7 +45,7 @@ Defined.
 Global Instance is1bifunctor_compose {A B C D : Type}
   `{Is1Cat A, Is1Cat B, Is1Cat C, Is1Cat D}
   (F : A -> B -> C) (G : C -> D) `{!Is0Functor G, !Is1Functor G}
-  `{!Is0Bifunctor F, !Is1Bifunctor F}
+  `{!Is0Bifunctor F, bf : !Is1Bifunctor F}
   : Is1Bifunctor (fun a b => G (F a b)).
 Proof.
   nrapply Build_Is1Bifunctor.

From 56d82e77755113a2fbf2acf8fb35ee3c3965e287 Mon Sep 17 00:00:00 2001
From: gio256 <102917377+gio256@users.noreply.github.com>
Date: Sat, 9 Mar 2024 11:07:10 -0700
Subject: [PATCH 07/25] AbSES/Ext.v: simplify bifunctor proofs for ab_ext

---
 theories/Algebra/AbSES/Ext.v | 67 +++++++++++++++---------------------
 1 file changed, 28 insertions(+), 39 deletions(-)

diff --git a/theories/Algebra/AbSES/Ext.v b/theories/Algebra/AbSES/Ext.v
index 4de575cb46c..c468e3a9c2c 100644
--- a/theories/Algebra/AbSES/Ext.v
+++ b/theories/Algebra/AbSES/Ext.v
@@ -11,6 +11,14 @@ Local Open Scope mc_add_scope.
 
 Definition Ext (B A : AbGroup@{u}) := pTr 0 (AbSES B A).
 
+Global Instance is0bifunctor_ext `{Univalence}
+  : Is0Bifunctor (Ext : AbGroup^op -> AbGroup -> pType)
+  := is0bifunctor_compose _ _ (bf:=is0bifunctor_abses).
+
+Global Instance is1bifunctor_ext `{Univalence}
+  : Is1Bifunctor (Ext : AbGroup^op -> AbGroup -> pType)
+  := is1bifunctor_compose _ _ (bf:=is1bifunctor_abses).
+
 (** An extension [E : AbSES B A] is trivial in [Ext B A] if and only if [E] merely splits. *)
 Proposition iff_ab_ext_trivial_split `{Univalence} {B A : AbGroup} (E : AbSES B A)
   : merely {s : GroupHomomorphism B E & (projection _) $o s == idmap}
@@ -65,84 +73,65 @@ Proof.
   apply baer_sum_commutative.
 Defined.
 
-Global Instance is0functor_ext01 `{Univalence} (B : AbGroup^op)
+Global Instance is0functor_abext01 `{Univalence} (B : AbGroup^op)
   : Is0Functor (ab_ext B).
 Proof.
   srapply Build_Is0Functor; intros ? ? f.
   snrapply Build_GroupHomomorphism.
-  1: exact (fmap01 (A:=AbGroup^op) Ext' B f).
+  1: exact (fmap (Ext B) f).
   rapply Trunc_ind; intro E0.
   rapply Trunc_ind; intro E1.
   apply (ap tr); cbn.
   apply baer_sum_pushout.
 Defined.
 
-Global Instance is0functor_ext10 `{Univalence} (A : AbGroup)
+Global Instance is0functor_abext10 `{Univalence} (A : AbGroup)
   : Is0Functor (fun B : AbGroup^op => ab_ext B A).
 Proof.
   srapply Build_Is0Functor; intros ? ? f; cbn.
   snrapply Build_GroupHomomorphism.
-  1: exact (fmap10 (A:=AbGroup^op) Ext' f A).
+  1: exact (fmap (fun (B : AbGroup^op) => Ext B A) f).
   rapply Trunc_ind; intro E0.
   rapply Trunc_ind; intro E1.
   apply (ap tr); cbn.
   apply baer_sum_pullback.
 Defined.
 
-Global Instance is1functor_ext01 `{Univalence} (B : AbGroup^op)
+Global Instance is1functor_abext01 `{Univalence} (B : AbGroup^op)
   : Is1Functor (ab_ext B).
 Proof.
   snrapply Build_Is1Functor.
-  - intros A C f g p x.
-    strip_truncations; cbn.
-    apply (ap tr).
-    apply abses_pushout_homotopic.
-    exact p.
-  - intros A x.
-    strip_truncations; cbn.
-    apply (ap tr).
-    apply abses_pushout_id.
-  - intros A C D f g x.
-    strip_truncations; cbn.
-    apply (ap tr).
-    apply abses_pushout_compose.
+  - intros A C f g.
+    exact (fmap2 (Ext B)).
+  - exact (fmap_id (Ext B)).
+  - intros A C D.
+    exact (fmap_comp (Ext B)).
 Defined.
 
-Global Instance is1functor_ext10 `{Univalence} (A : AbGroup)
+Global Instance is1functor_abext10 `{Univalence} (A : AbGroup)
   : Is1Functor (fun B : AbGroup^op => ab_ext B A).
 Proof.
   snrapply Build_Is1Functor.
-  - intros B C f g p x.
-    strip_truncations; cbn.
-    apply (ap tr).
-    apply abses_pullback_homotopic.
-    exact p.
-  - intros B x.
-    strip_truncations; cbn.
-    apply (ap tr).
-    apply abses_pullback_id.
-  - intros B C D f g x.
-    strip_truncations; cbn.
-    apply (ap tr).
-    symmetry.
-    apply abses_pullback_compose.
+  - intros B C f g.
+    exact (fmap2 (fun B : AbGroup^op => Ext B A)).
+  - exact (fmap_id (fun B : AbGroup^op => Ext B A)).
+  - intros B C D.
+    exact (fmap_comp (fun B : AbGroup^op => Ext B A)).
 Defined.
 
-Global Instance is0bifunctor_ext `{Univalence}
+Global Instance is0bifunctor_abext `{Univalence}
   : Is0Bifunctor (A:=AbGroup^op) ab_ext.
 Proof.
   rapply Build_Is0Bifunctor.
 Defined.
 
-Global Instance is1bifunctor_ext `{Univalence}
+Global Instance is1bifunctor_abext `{Univalence}
   : Is1Bifunctor (A:=AbGroup^op) ab_ext.
 Proof.
   snrapply Build_Is1Bifunctor.
   1,2: exact _.
-  intros B B' f A A' g.
-  rapply Trunc_ind; intro E.
-  apply (ap tr).
-  apply abses_pushout_pullback_reorder.
+  intros A B.
+  exact (bifunctor_isbifunctor (Ext : AbGroup^op -> AbGroup -> pType)).
 Defined.
 
 (** We can push out a fixed extension while letting the map vary, and this defines a group homomorphism. *)

From 2c9fce63b21da1300b967be1a893eeb24e3aeb88 Mon Sep 17 00:00:00 2001
From: gio256 <102917377+gio256@users.noreply.github.com>
Date: Sat, 9 Mar 2024 11:20:42 -0700
Subject: [PATCH 08/25] AbSES/Ext.v: remove universe annotations

---
 theories/Algebra/AbSES/Ext.v | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/theories/Algebra/AbSES/Ext.v b/theories/Algebra/AbSES/Ext.v
index c468e3a9c2c..ec826e95e56 100644
--- a/theories/Algebra/AbSES/Ext.v
+++ b/theories/Algebra/AbSES/Ext.v
@@ -33,12 +33,11 @@ Defined.
 Definition Ext' (B A : AbGroup@{u}) := Tr 0 (AbSES' B A).
 
 Global Instance is0bifunctor_ext'@{u v w | u < v, v < w} `{Univalence}
-  : Is0Bifunctor@{v v w u u v} (Ext' : AbGroup@{u}^op -> AbGroup@{u} -> Type@{v})
+  : Is0Bifunctor (Ext' : AbGroup@{u}^op -> AbGroup@{u} -> Type@{v})
   := is0bifunctor_compose _ _ (bf:=is0bifunctor_abses').
 
-(**TODO: universes*)
 Global Instance is1bifunctor_ext'@{u v w | u < v, v < w} `{Univalence}
-  : Is1Bifunctor@{v v w u u v v u u} (Ext' : AbGroup@{u}^op -> AbGroup@{u} -> Type@{v})
+  : Is1Bifunctor (Ext' : AbGroup@{u}^op -> AbGroup@{u} -> Type@{v})
   := is1bifunctor_compose _ _ (bf:=is1bifunctor_abses').
 
 (** [Ext B A] is an abelian group for any [A B : AbGroup]. The proof of commutativity is a bit faster if we separate out the proof that [Ext B A] is a group. *)

From d78a876b34752388d8caf96a2d3314246208bbe2 Mon Sep 17 00:00:00 2001
From: gio256 <102917377+gio256@users.noreply.github.com>
Date: Sat, 9 Mar 2024 13:49:16 -0700
Subject: [PATCH 09/25] Simplify building of bifunctors

---
 theories/Homotopy/Join/Core.v |  32 +++----
 theories/WildCat/Bifunctor.v  | 152 ++++++++++++----------------------
 theories/WildCat/Prod.v       |  55 ++++++++++++
 3 files changed, 119 insertions(+), 120 deletions(-)

diff --git a/theories/Homotopy/Join/Core.v b/theories/Homotopy/Join/Core.v
index d0a360f44c1..35116772931 100644
--- a/theories/Homotopy/Join/Core.v
+++ b/theories/Homotopy/Join/Core.v
@@ -562,31 +562,21 @@ Section FunctorJoin.
 
   Global Instance is0bifunctor_join : Is0Bifunctor Join.
   Proof.
-    snrapply Build_Is0Bifunctor.
-    - intro A; snrapply Build_Is0Functor; intros B D g.
-      exact (functor_join idmap g).
-    - intro B; snrapply Build_Is0Functor; intros A C f.
-      exact (functor_join f idmap).
+    rapply Build_Is0Bifunctor'.
+    apply Build_Is0Functor.
+    intros A B [f g].
+    exact (functor_join f g).
   Defined.
 
   Global Instance is1bifunctor_join : Is1Bifunctor Join.
   Proof.
-    snrapply Build_Is1Bifunctor.
-    - intro A; snrapply Build_Is1Functor.
-      + intros B C f g p.
-        exact (functor2_join (fun _ => 1) p).
-      + intro B; exact functor_join_idmap.
-      + intros B C D f g.
-        exact (functor_join_compose idmap f idmap g).
-    - intro B; snrapply Build_Is1Functor.
-      + intros A C f g p.
-        exact (functor2_join p (fun _ => 1)).
-      + intro A; exact functor_join_idmap.
-      + intros A C D f g.
-        exact (functor_join_compose f idmap g idmap).
-    - intros A C f B D g x.
-      lhs_V nrapply functor_join_compose.
-      nrapply functor_join_compose.
+    snrapply Build_Is1Bifunctor'.
+    nrapply Build_Is1Functor.
+    - intros A B f g [p q].
+      exact (functor2_join p q).
+    - intros A; exact functor_join_idmap.
+    - intros A B C [f g] [h k].
+      exact (functor_join_compose f g h k).
   Defined.
 
 End FunctorJoin.
diff --git a/theories/WildCat/Bifunctor.v b/theories/WildCat/Bifunctor.v
index b234d7c4401..7391e2bdf77 100644
--- a/theories/WildCat/Bifunctor.v
+++ b/theories/WildCat/Bifunctor.v
@@ -23,20 +23,56 @@ Class Is1Bifunctor {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
 Arguments bifunctor_isbifunctor {A B C} {_ _ _ _ _ _ _ _ _ _ _ _}
   F {_ _} {a0 a1} f {b0 b1} g.
 
-Definition fmap01 {A B C : Type} `{Is01Cat A, Is01Cat B, Is1Cat C}
-  (F : A -> B -> C) `{!Is0Bifunctor F}
-  (a : A) {b0 b1 : B} (g : b0 $-> b1)
-  : F a b0 $-> F a b1 := fmap (F a) g.
+(** Functors from product categories are (uncurried) bifunctors. *)
+Global Instance is0bifunctor_functor_uncurried {A B C : Type}
+  `{Is01Cat A, Is01Cat B, IsGraph C} (F : A * B -> C) `{!Is0Functor F}
+  : Is0Bifunctor (fun a b => F (a, b)).
+Proof.
+  rapply Build_Is0Bifunctor.
+Defined.
 
+Global Instance is1bifunctor_functor_uncurried {A B C : Type}
+  `{Is1Cat A, Is1Cat B, Is1Cat C}
+  (F : A * B -> C) `{!Is0Functor F, !Is1Functor F}
+  : Is1Bifunctor (fun a b => F (a, b)).
+Proof.
+  apply Build_Is1Bifunctor.
+  1,2: exact _.
+  intros a b f c d g; cbn.
+  refine ((fmap_comp F _ _)^$ $@ _ $@ fmap_comp F _ _).
+  rapply (fmap2 F).
+  refine (cat_idl f $@ (cat_idr f)^$, _).
+  exact (cat_idr g $@ (cat_idl g)^$).
+Defined.
+
+(** It is often simplest to create a bifunctor [A -> B -> C] by constructing a functor from the product category [A * B]. *)
+Definition Build_Is0Bifunctor' {A B C : Type} `{Is01Cat A, Is01Cat B, IsGraph C}
+  (F : A -> B -> C) `{!Is0Functor (uncurry F)}
+  : Is0Bifunctor F
+  := is0bifunctor_functor_uncurried (uncurry F).
+
+Definition Build_Is1Bifunctor' {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
+  (F : A -> B -> C) `{!Is0Functor (uncurry F), !Is1Functor (uncurry F)}
+  : Is1Bifunctor F
+  := is1bifunctor_functor_uncurried (uncurry F).
+
+(* fmap in the first argument *)
 Definition fmap10 {A B C : Type} `{Is01Cat A, Is01Cat B, Is1Cat C}
-  (F : A -> B -> C) `{!Is0Bifunctor F}
-  {a0 a1 : A} (f : a0 $-> a1) (b : B)
-  : (F a0 b) $-> (F a1 b) := fmap (flip F b) f.
+  (F : A -> B -> C) `{!Is0Bifunctor F} {a0 a1 : A} (f : a0 $-> a1) (b : B)
+  : (F a0 b) $-> (F a1 b)
+  := fmap (flip F b) f.
+
+(* fmap in the second argument *)
+Definition fmap01 {A B C : Type} `{Is01Cat A, Is01Cat B, Is1Cat C}
+  (F : A -> B -> C) `{!Is0Bifunctor F} (a : A) {b0 b1 : B} (g : b0 $-> b1)
+  : F a b0 $-> F a b1
+  := fmap (F a) g.
 
+(** Restricting a functor along a bifunctor yields a bifunctor. *)
 Global Instance is0bifunctor_compose {A B C D : Type}
   `{IsGraph A, IsGraph B, Is1Cat C, Is1Cat D}
-  (F : A -> B -> C) (G : C -> D) `{!Is0Functor G, !Is1Functor G}
-  `{bf : !Is0Bifunctor F}
+  (F : A -> B -> C) `{bf : !Is0Bifunctor F}
+  (G : C -> D) `{!Is0Functor G, !Is1Functor G}
   : Is0Bifunctor (fun a b => G (F a b)).
 Proof.
   rapply Build_Is0Bifunctor.
@@ -67,26 +103,24 @@ Proof.
     + intros a b c f g.
       refine (fmap2 G (fmap_comp (flip F y) f g) $@ _).
       exact (fmap_comp G _ _).
-  - intros a0 a1 f b0 b1 g; cbn.
+  - intros a0 a1 f b0 b1 g.
     refine ((fmap_comp G _ _)^$ $@ _ $@ fmap_comp G _ _).
     rapply fmap2.
-    cbn.
     exact (bifunctor_isbifunctor F f g).
 Defined.
 
-(** There are two possible ways to define this, which will only agree in the event that the bifunctor coherence condition ([bifunctor_isbifunctor]) holds. *)
+(*TODO: does the comment below imply (incorrectly) that [Is0Bifunctor] ensures the two routes agree?*)
+(** Any 0-bifunctor [A -> B -> C] can be made into a functor from the product category [A * B -> C] in two ways. The bifunctor coherence condition ([bifunctor_isbifunctor]) states precisely that these two routes agree. *)
 Global Instance is0functor_uncurry_bifunctor {A B C : Type}
-  `{IsGraph A, IsGraph B, Is1Cat C}
-  (F : A -> B -> C)
-  `{forall a, Is0Functor (F a), forall b, Is0Functor (flip F b)}
+  `{IsGraph A, IsGraph B, Is1Cat C} (F : A -> B -> C) `{!Is0Bifunctor F}
   : Is0Functor (uncurry F).
 Proof.
-  srapply Build_Is0Functor.
-  intros [a1 b1] [a2 b2] [f g]; cbn in f, g.
-  unfold uncurry; cbn.
-  exact ((fmap (flip F b2) f) $o (fmap (F a1) g)).
+  nrapply Build_Is0Functor.
+  intros [a b] [c d] [f g].
+  exact (fmap (flip F d) f $o fmap (F a) g).
 Defined.
 
+(** Any 1-bifunctor defines a canonical functor from the product category. *)
 Global Instance is1functor_uncurry_bifunctor {A B C : Type}
   `{Is1Cat A, Is1Cat B, Is1Cat C} (F : A -> B -> C)
   `{!Is0Bifunctor F, !Is1Bifunctor F}
@@ -106,83 +140,3 @@ Proof.
     refine (cat_assoc _ _ _ $@R _ $@ _ $@ (cat_assoc_opp _ _ _ $@R _)).
     exact (_ $@L (bifunctor_isbifunctor F _ _)^$ $@R _).
 Defined.
-
-(** *** Uncurried bifunctors are functorial in each argument. *)
-
-Global Instance is0functor_bifunctor_uncurried01 {A B C : Type}
-  `{Is01Cat A} `{IsGraph B} `{IsGraph C}
-  (F : A * B -> C) `{!Is0Functor F} (a : A)
-  : Is0Functor (fun b => F (a, b)).
-Proof.
-  nrapply (is0functor_compose (fun b => (a, b)) F).
-  2: exact _.
-  nrapply Build_Is0Functor.
-  intros b c f.
-  exact (Id a, f).
-Defined.
-
-Global Instance is1functor_bifunctor_uncurried01 {A B C : Type}
-  `{Is1Cat A} `{Is1Cat B} `{Is1Cat C}
-  (F : A * B -> C) `{!Is0Functor F, !Is1Functor F} (a : A)
-  : Is1Functor (fun b => F (a, b)).
-Proof.
-  nrapply (is1functor_compose (fun b => (a, b)) F).
-  2: exact _.
-  nrapply Build_Is1Functor.
-  - intros b c f g p.
-    exact (Id _, p).
-  - intros b; reflexivity.
-  - intros b c d f g.
-    exact ((cat_idl _)^$, Id _).
-Defined.
-
-Global Instance is0functor_bifunctor_uncurried10 {A B C : Type}
-  `{IsGraph A} `{Is01Cat B} `{IsGraph C}
-  (F : A * B -> C) `{!Is0Functor F} (b : B)
-  : Is0Functor (fun a => F (a, b)).
-Proof.
-  nrapply (is0functor_compose (fun a => (a, b)) F).
-  2: exact _.
-  nrapply Build_Is0Functor.
-  intros a c f.
-  exact (f, Id b).
-Defined.
-
-Global Instance is1functor_bifunctor_uncurried10 {A B C : Type}
-  `{Is1Cat A} `{Is1Cat B} `{Is1Cat C}
-  (F : A * B -> C) `{!Is0Functor F, !Is1Functor F} (b : B)
-  : Is1Functor (fun a => F (a, b)).
-Proof.
-  nrapply (is1functor_compose (fun a => (a, b)) F).
-  2: exact _.
-  nrapply Build_Is1Functor.
-  - intros a c f g p.
-    exact (p, Id _).
-  - intros a; reflexivity.
-  - intros a c d f g.
-    cbn.
-    exact (Id _, (cat_idl _)^$).
-Defined.
-
-Global Instance is0bifunctor_bifunctor_uncurried {A B C : Type}
-  `{Is01Cat A, Is01Cat B, IsGraph C}
-  (F : A * B -> C) `{!Is0Functor F}
-  : Is0Bifunctor (fun a b => F (a, b)).
-Proof.
-  rapply Build_Is0Bifunctor.
-Defined.
-
-Global Instance is1bifunctor_bifunctor_uncurried {A B C : Type}
-  `{Is1Cat A, Is1Cat B, Is1Cat C}
-  (F : A * B -> C) `{!Is0Functor F, !Is1Functor F}
-  : Is1Bifunctor (fun a b => F (a, b)).
-Proof.
-  apply Build_Is1Bifunctor.
-  1,2: exact _.
-  intros a b f c d g.
-  refine ((fmap_comp F _ _)^$ $@ _).
-  refine (_ $@ (fmap_comp F _ _)).
-  rapply (fmap2 F).
-  refine (cat_idl f $@ (cat_idr f)^$, _).
-  exact (cat_idr g $@ (cat_idl g)^$).
-Defined.
diff --git a/theories/WildCat/Prod.v b/theories/WildCat/Prod.v
index 93b06f6d5bc..19be81015f9 100644
--- a/theories/WildCat/Prod.v
+++ b/theories/WildCat/Prod.v
@@ -177,3 +177,58 @@ Proof.
   - reflexivity.
 Defined.
 
+(** Functors from a product category are functorial in each argument *)
+
+Global Instance is0functor_functor_uncurried01 {A B C : Type}
+  `{Is01Cat A} `{IsGraph B} `{IsGraph C}
+  (F : A * B -> C) `{!Is0Functor F} (a : A)
+  : Is0Functor (fun b => F (a, b)).
+Proof.
+  nrapply (is0functor_compose (fun b => (a, b)) F).
+  2: exact _.
+  nrapply Build_Is0Functor.
+  intros b c f.
+  exact (Id a, f).
+Defined.
+
+Global Instance is1functor_functor_uncurried01 {A B C : Type}
+  `{Is1Cat A} `{Is1Cat B} `{Is1Cat C}
+  (F : A * B -> C) `{!Is0Functor F, !Is1Functor F} (a : A)
+  : Is1Functor (fun b => F (a, b)).
+Proof.
+  nrapply (is1functor_compose (fun b => (a, b)) F).
+  2: exact _.
+  nrapply Build_Is1Functor.
+  - intros b c f g p.
+    exact (Id _, p).
+  - intros b; reflexivity.
+  - intros b c d f g.
+    exact ((cat_idl _)^$, Id _).
+Defined.
+
+Global Instance is0functor_functor_uncurried10 {A B C : Type}
+  `{IsGraph A} `{Is01Cat B} `{IsGraph C}
+  (F : A * B -> C) `{!Is0Functor F} (b : B)
+  : Is0Functor (fun a => F (a, b)).
+Proof.
+  nrapply (is0functor_compose (fun a => (a, b)) F).
+  2: exact _.
+  nrapply Build_Is0Functor.
+  intros a c f.
+  exact (f, Id b).
+Defined.
+
+Global Instance is1functor_functor_uncurried10 {A B C : Type}
+  `{Is1Cat A} `{Is1Cat B} `{Is1Cat C}
+  (F : A * B -> C) `{!Is0Functor F, !Is1Functor F} (b : B)
+  : Is1Functor (fun a => F (a, b)).
+Proof.
+  nrapply (is1functor_compose (fun a => (a, b)) F).
+  2: exact _.
+  nrapply Build_Is1Functor.
+  - intros a c f g p.
+    exact (p, Id _).
+  - intros a; reflexivity.
+  - intros a c d f g.
+    exact (Id _, (cat_idl _)^$).
+Defined.

From e19d81e43cabf7ebe75f5772c04c8ed1d26df0fb Mon Sep 17 00:00:00 2001
From: gio256 <102917377+gio256@users.noreply.github.com>
Date: Sat, 9 Mar 2024 14:40:07 -0700
Subject: [PATCH 10/25] WildCat/Yoneda.v: Add bifunctor instances for hom

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

diff --git a/theories/WildCat/Yoneda.v b/theories/WildCat/Yoneda.v
index faf01c0e25b..241f0b2729f 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.Bifunctor.
 Require Import WildCat.ZeroGroupoid.
 
 (** ** Two-variable hom-functors *)
@@ -42,6 +43,14 @@ Proof.
     refine (cat_assoc_opp _ _ _).
 Defined.
 
+Global Instance is0bifunctor_hom {A} `{Is01Cat A}
+  : @Is0Bifunctor A^op A Type _ _ _ (@Hom A _)
+  := is0bifunctor_functor_uncurried _.
+
+Global Instance is1bifunctor_hom {A} `{Is1Cat A} `{HasMorExt A}
+  : @Is1Bifunctor A^op A Type _ _ _ _ _ _ _ _ _ _ _ _ (@Hom A _) _
+  := is1bifunctor_functor_uncurried _.
+
 Definition fun01_hom {A} `{Is01Cat A}
   : Fun01 (A^op * A) Type
   := @Build_Fun01 _ _ _ _ _ is0functor_hom.

From f5e4d86409be8dfbf74d569ebbaf0397b08f75de Mon Sep 17 00:00:00 2001
From: gio256 <102917377+gio256@users.noreply.github.com>
Date: Sat, 9 Mar 2024 15:45:58 -0700
Subject: [PATCH 11/25] WildCat/Prod.v: add product inclusions

---
 theories/WildCat/Prod.v | 76 ++++++++++++++++++++++++-----------------
 1 file changed, 44 insertions(+), 32 deletions(-)

diff --git a/theories/WildCat/Prod.v b/theories/WildCat/Prod.v
index 19be81015f9..e2bbdc4d066 100644
--- a/theories/WildCat/Prod.v
+++ b/theories/WildCat/Prod.v
@@ -177,27 +177,40 @@ Proof.
   - reflexivity.
 Defined.
 
-(** Functors from a product category are functorial in each argument *)
+(** Inclusions into a product category are functorial. *)
 
-Global Instance is0functor_functor_uncurried01 {A B C : Type}
-  `{Is01Cat A} `{IsGraph B} `{IsGraph C}
-  (F : A * B -> C) `{!Is0Functor F} (a : A)
-  : Is0Functor (fun b => F (a, b)).
+(* [A * {b}] *)
+Global Instance is0functor_prod_include10 {A B : Type} `{IsGraph A, Is01Cat B} (b : B)
+  : Is0Functor (fun a : A => (a, b)).
+Proof.
+  nrapply Build_Is0Functor.
+  intros a c f.
+  exact (f, Id b).
+Defined.
+
+Global Instance is1functor_prod_include10 {A B : Type} `{Is1Cat A, Is1Cat B} (b : B)
+  : Is1Functor (fun a : A => (a, b)).
+Proof.
+  nrapply Build_Is1Functor.
+  - intros a c f g p.
+    exact (p, Id _).
+  - intros a; reflexivity.
+  - intros a c d f g.
+    exact (Id _, (cat_idl _)^$).
+Defined.
+
+(* [{a} * B] *)
+Global Instance is0functor_prod_include01 {A B : Type} `{Is01Cat A, IsGraph B} (a : A)
+  : Is0Functor (fun b : B => (a, b)).
 Proof.
-  nrapply (is0functor_compose (fun b => (a, b)) F).
-  2: exact _.
   nrapply Build_Is0Functor.
   intros b c f.
   exact (Id a, f).
 Defined.
 
-Global Instance is1functor_functor_uncurried01 {A B C : Type}
-  `{Is1Cat A} `{Is1Cat B} `{Is1Cat C}
-  (F : A * B -> C) `{!Is0Functor F, !Is1Functor F} (a : A)
-  : Is1Functor (fun b => F (a, b)).
+Global Instance is1functor_prod_include01 {A B : Type} `{Is1Cat A, Is1Cat B} (a : A)
+  : Is1Functor (fun b : B => (a, b)).
 Proof.
-  nrapply (is1functor_compose (fun b => (a, b)) F).
-  2: exact _.
   nrapply Build_Is1Functor.
   - intros b c f g p.
     exact (Id _, p).
@@ -206,29 +219,28 @@ Proof.
     exact ((cat_idl _)^$, Id _).
 Defined.
 
+(** Functors from a product category are functorial in each argument *)
+
+Global Instance is0functor_functor_uncurried01 {A B C : Type}
+  `{Is01Cat A} `{IsGraph B} `{IsGraph C}
+  (F : A * B -> C) `{!Is0Functor F} (a : A)
+  : Is0Functor (fun b => F (a, b))
+  := is0functor_compose (fun b => (a, b)) F.
+
+Global Instance is1functor_functor_uncurried01 {A B C : Type}
+  `{Is1Cat A} `{Is1Cat B} `{Is1Cat C}
+  (F : A * B -> C) `{!Is0Functor F, !Is1Functor F} (a : A)
+  : Is1Functor (fun b => F (a, b))
+  := is1functor_compose (fun b => (a, b)) F.
+
 Global Instance is0functor_functor_uncurried10 {A B C : Type}
   `{IsGraph A} `{Is01Cat B} `{IsGraph C}
   (F : A * B -> C) `{!Is0Functor F} (b : B)
-  : Is0Functor (fun a => F (a, b)).
-Proof.
-  nrapply (is0functor_compose (fun a => (a, b)) F).
-  2: exact _.
-  nrapply Build_Is0Functor.
-  intros a c f.
-  exact (f, Id b).
-Defined.
+  : Is0Functor (fun a => F (a, b))
+  := is0functor_compose (fun a => (a, b)) F.
 
 Global Instance is1functor_functor_uncurried10 {A B C : Type}
   `{Is1Cat A} `{Is1Cat B} `{Is1Cat C}
   (F : A * B -> C) `{!Is0Functor F, !Is1Functor F} (b : B)
-  : Is1Functor (fun a => F (a, b)).
-Proof.
-  nrapply (is1functor_compose (fun a => (a, b)) F).
-  2: exact _.
-  nrapply Build_Is1Functor.
-  - intros a c f g p.
-    exact (p, Id _).
-  - intros a; reflexivity.
-  - intros a c d f g.
-    exact (Id _, (cat_idl _)^$).
-Defined.
+  : Is1Functor (fun a => F (a, b))
+  := is1functor_compose (fun a => (a, b)) F.

From 192a78649a6594bc1868d8c5b92295ffb2465939 Mon Sep 17 00:00:00 2001
From: gio256 <102917377+gio256@users.noreply.github.com>
Date: Sat, 9 Mar 2024 15:52:24 -0700
Subject: [PATCH 12/25] WildCat/Bifunctor.v: remove comment

---
 theories/WildCat/Bifunctor.v | 1 -
 1 file changed, 1 deletion(-)

diff --git a/theories/WildCat/Bifunctor.v b/theories/WildCat/Bifunctor.v
index 7391e2bdf77..f5775cfdf5b 100644
--- a/theories/WildCat/Bifunctor.v
+++ b/theories/WildCat/Bifunctor.v
@@ -109,7 +109,6 @@ Proof.
     exact (bifunctor_isbifunctor F f g).
 Defined.
 
-(*TODO: does the comment below imply (incorrectly) that [Is0Bifunctor] ensures the two routes agree?*)
 (** Any 0-bifunctor [A -> B -> C] can be made into a functor from the product category [A * B -> C] in two ways. The bifunctor coherence condition ([bifunctor_isbifunctor]) states precisely that these two routes agree. *)
 Global Instance is0functor_uncurry_bifunctor {A B C : Type}
   `{IsGraph A, IsGraph B, Is1Cat C} (F : A -> B -> C) `{!Is0Bifunctor F}

From beed14d6de54b8291d9baffbe1b41ed153e1b33d Mon Sep 17 00:00:00 2001
From: gio256 <102917377+gio256@users.noreply.github.com>
Date: Sat, 9 Mar 2024 15:56:51 -0700
Subject: [PATCH 13/25] AbSES/Ext.v: remove universe annotations

---
 theories/Algebra/AbSES/Ext.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/theories/Algebra/AbSES/Ext.v b/theories/Algebra/AbSES/Ext.v
index ec826e95e56..5fb5e83ee32 100644
--- a/theories/Algebra/AbSES/Ext.v
+++ b/theories/Algebra/AbSES/Ext.v
@@ -32,12 +32,12 @@ Defined.
 
 Definition Ext' (B A : AbGroup@{u}) := Tr 0 (AbSES' B A).
 
-Global Instance is0bifunctor_ext'@{u v w | u < v, v < w} `{Univalence}
-  : Is0Bifunctor (Ext' : AbGroup@{u}^op -> AbGroup@{u} -> Type@{v})
+Global Instance is0bifunctor_ext' `{Univalence}
+  : Is0Bifunctor (Ext' : AbGroup^op -> AbGroup -> Type)
   := is0bifunctor_compose _ _ (bf:=is0bifunctor_abses').
 
-Global Instance is1bifunctor_ext'@{u v w | u < v, v < w} `{Univalence}
-  : Is1Bifunctor (Ext' : AbGroup@{u}^op -> AbGroup@{u} -> Type@{v})
+Global Instance is1bifunctor_ext' `{Univalence}
+  : Is1Bifunctor (Ext' : AbGroup^op -> AbGroup -> Type)
   := is1bifunctor_compose _ _ (bf:=is1bifunctor_abses').
 
 (** [Ext B A] is an abelian group for any [A B : AbGroup]. The proof of commutativity is a bit faster if we separate out the proof that [Ext B A] is a group. *)

From f9302324ad9c8430daa0dd7ae51fcfa65f7d2836 Mon Sep 17 00:00:00 2001
From: gio256 <102917377+gio256@users.noreply.github.com>
Date: Sat, 9 Mar 2024 16:14:13 -0700
Subject: [PATCH 14/25] WildCat/Yoneda.v: add comment

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

diff --git a/theories/WildCat/Yoneda.v b/theories/WildCat/Yoneda.v
index 241f0b2729f..3ae8ed87644 100644
--- a/theories/WildCat/Yoneda.v
+++ b/theories/WildCat/Yoneda.v
@@ -47,6 +47,7 @@ Global Instance is0bifunctor_hom {A} `{Is01Cat A}
   : @Is0Bifunctor A^op A Type _ _ _ (@Hom A _)
   := is0bifunctor_functor_uncurried _.
 
+(** While it is possible to prove the bifunctor coherence condition from [Is1Cat_Strong], 1-functoriality requires morphism extensionality.*)
 Global Instance is1bifunctor_hom {A} `{Is1Cat A} `{HasMorExt A}
   : @Is1Bifunctor A^op A Type _ _ _ _ _ _ _ _ _ _ _ _ (@Hom A _) _
   := is1bifunctor_functor_uncurried _.

From da5cb5a9dfa761f14c59560e4e549e71fc25cde5 Mon Sep 17 00:00:00 2001
From: gio256 <102917377+gio256@users.noreply.github.com>
Date: Sat, 9 Mar 2024 16:36:05 -0700
Subject: [PATCH 15/25] WildCat/Monoidal: tensor product is a 1-bifunctor

---
 theories/WildCat/Monoidal.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/WildCat/Monoidal.v b/theories/WildCat/Monoidal.v
index 55477f16280..a38bd28be0f 100644
--- a/theories/WildCat/Monoidal.v
+++ b/theories/WildCat/Monoidal.v
@@ -8,7 +8,7 @@ Section Monoidal.
   Context `{Is1Cat C}.
   Context `{HasEquivs C}.
   Context (tensor : C -> C -> C).
-  Context `{!Is0Bifunctor tensor}.
+  Context `{!Is0Bifunctor tensor, !Is1Bifunctor tensor}.
 
   Definition left_assoc : C -> C -> C -> C :=
     fun a b c => tensor (tensor a b) c.

From c41d397e38e8ff5af49473171adc1bf115c90f80 Mon Sep 17 00:00:00 2001
From: gio256 <102917377+gio256@users.noreply.github.com>
Date: Sun, 10 Mar 2024 17:07:44 -0600
Subject: [PATCH 16/25] WildCat equivs: add compose_catie'

---
 theories/WildCat/DisplayedEquiv.v | 44 +++++++++++++++++++++++--------
 theories/WildCat/Equiv.v          | 44 ++++++++++++++++++++-----------
 2 files changed, 61 insertions(+), 27 deletions(-)

diff --git a/theories/WildCat/DisplayedEquiv.v b/theories/WildCat/DisplayedEquiv.v
index 3a207682f58..713b743dcd0 100644
--- a/theories/WildCat/DisplayedEquiv.v
+++ b/theories/WildCat/DisplayedEquiv.v
@@ -172,23 +172,43 @@ Global Instance reflexive_dcate {A} {D : A -> Type} `{DHasEquivs A D} {a : A}
   := did_cate.
 
 (** Equivalences can be composed. *)
-Global Instance dcompose_catie {A} {D : A -> Type} `{DHasEquivs A D}
-  {a b c : A} {g : b $<~> c} {f : a $<~> b} {a' : D a} {b' : D b} {c' : D c}
-  (g' : DCatEquiv g b' c') (f' : DCatEquiv f a' b')
-  : DCatIsEquiv (dcate_fun g' $o' f').
+Global Instance dcompose_catie' {A} {D : A -> Type} `{DHasEquivs A D}
+  {a b c : A} {g : b $-> c} `{!CatIsEquiv g} {f : a $-> b} `{!CatIsEquiv f}
+  {a' : D a} {b' : D b} {c' : D c}
+  (g' : DHom g b' c') `{ge' : !DCatIsEquiv g'}
+  (f' : DHom f a' b') `{fe' : !DCatIsEquiv f'}
+  : DCatIsEquiv (fe:=compose_catie' g f) (g' $o' f').
 Proof.
   snrapply dcatie_adjointify.
-  - exact (dcate_fun f'^-1$' $o' g'^-1$').
+  - refine (_ $o' _).
+    1: nrapply (Build_DCatEquiv f')^-1$'; exact fe'.
+    nrapply (Build_DCatEquiv g')^-1$'; exact ge'.
   - refine (dcat_assoc _ _ _ $@' _).
+    refine (_ $@L' ((dcate_buildequiv_fun f')^$' $@R' _ ) $@' _).
+    1: exact isd0gpd_hom.
     refine (_ $@L' dcat_assoc_opp _ _ _ $@' _).
-    refine (_ $@L' (dcate_isretr _ $@R' _) $@' _).
+    refine (_ $@L' (dcate_isretr (Build_DCatEquiv f') $@R' _) $@' _).
     refine (_ $@L' dcat_idl _ $@' _).
-    apply dcate_isretr.
+    refine ((dcate_buildequiv_fun g')^$' $@R' _ $@' _).
+    1: exact isd0gpd_hom.
+    nrapply dcate_isretr.
   - refine (dcat_assoc _ _ _ $@' _).
     refine (_ $@L' dcat_assoc_opp _ _ _ $@' _).
-    refine (_ $@L' (dcate_issect _ $@R' _) $@' _).
+    refine (_ $@L' (_ $@L' (dcate_buildequiv_fun g')^$' $@R' _) $@' _).
+    1: exact isd0gpd_hom.
+    refine (_ $@L' (dcate_issect (Build_DCatEquiv g') $@R' _) $@' _).
     refine (_ $@L' dcat_idl _ $@' _).
-    apply dcate_issect.
+    refine (_ $@L' (dcate_buildequiv_fun f')^$' $@' _).
+    1: exact isd0gpd_hom.
+    nrapply dcate_issect.
+Defined.
+
+Global Instance dcompose_catie {A} {D : A -> Type} `{DHasEquivs A D}
+  {a b c : A} {g : b $<~> c} {f : a $<~> b} {a' : D a} {b' : D b} {c' : D c}
+  (g' : DCatEquiv g b' c') (f' : DCatEquiv f a' b')
+  : DCatIsEquiv (dcate_fun g' $o' f').
+Proof.
+  rapply dcompose_catie'.
 Defined.
 
 Definition dcompose_cate {A} {D : A -> Type} `{DHasEquivs A D}
@@ -387,8 +407,10 @@ Definition dcate_inv_compose {A} {D : A -> Type} `{DHasEquivs A D}
     (dcate_fun (f' $oE' e')^-1$') (dcate_fun (e'^-1$' $oE' f'^-1$')).
 Proof.
   refine (_ $@' (dcompose_cate_fun e'^-1$' f'^-1$')^$').
-  - snrapply dcate_inv_adjointify.
-  - exact isd0gpd_hom.
+  2: exact isd0gpd_hom.
+  refine (dcate_inv_adjointify _ _ _ _ $@' _).
+  refine (dcate_inv2 (dcate_buildequiv_fun _) $@R' _ $@' _).
+  exact (_ $@L' dcate_inv2 (dcate_buildequiv_fun _)).
 Defined.
 
 Definition dcate_inv_V {A} {D : A -> Type} `{DHasEquivs A D}
diff --git a/theories/WildCat/Equiv.v b/theories/WildCat/Equiv.v
index 820c839bc5a..e8c8a3153de 100644
--- a/theories/WildCat/Equiv.v
+++ b/theories/WildCat/Equiv.v
@@ -85,7 +85,7 @@ Defined.
 
 Notation "f ^-1$" := (cate_inv f).
 
-Definition cate_issect {A} `{HasEquivs A} {a b} (f : a $<~> b) 
+Definition cate_issect {A} `{HasEquivs A} {a b} (f : a $<~> b)
   : f^-1$ $o f $== Id a.
 Proof.
   refine (_ $@ cate_issect' a b f).
@@ -152,23 +152,33 @@ Global Instance symmetric_cate {A} `{HasEquivs A}
   := fun a b f => cate_inv f.
 
 (** Equivalences can be composed. *)
-Global Instance compose_catie {A} `{HasEquivs A} {a b c : A}
-  (g : b $<~> c) (f : a $<~> b)
+Definition compose_catie' {A} `{HasEquivs A} {a b c : A}
+  (g : b $-> c) `{!CatIsEquiv g} (f : a $-> b) `{!CatIsEquiv f}
   : CatIsEquiv (g $o f).
 Proof.
-  refine (catie_adjointify _ (f^-1$ $o g^-1$) _ _).
-  - refine (cat_assoc _ _ _ $@ _).
-    refine ((_ $@L cat_assoc_opp _ _ _) $@ _).
-    refine ((_ $@L (cate_isretr _ $@R _)) $@ _).
-    refine ((_ $@L cat_idl _) $@ _).
-    apply cate_isretr.
-  - refine (cat_assoc _ _ _ $@ _).
-    refine ((_ $@L cat_assoc_opp _ _ _) $@ _).
-    refine ((_ $@L (cate_issect _ $@R _)) $@ _).
-    refine ((_ $@L cat_idl _) $@ _).
-    apply cate_issect.
+  snrapply catie_adjointify.
+  - exact ((Build_CatEquiv f)^-1$ $o (Build_CatEquiv g)^-1$).
+  - nrefine (cat_assoc _ _ _ $@ _).
+    refine (_ $@L ((cate_buildequiv_fun f)^$ $@R _ ) $@ _).
+    nrefine (_ $@L cat_assoc_opp _ _ _ $@ _).
+    nrefine (_ $@L (cate_isretr (Build_CatEquiv f) $@R _) $@ _).
+    nrefine (_ $@L cat_idl _ $@ _).
+    refine ((cate_buildequiv_fun g)^$ $@R _ $@ _).
+    nrapply cate_isretr.
+  - nrefine (cat_assoc _ _ _ $@ _).
+    nrefine (_ $@L cat_assoc_opp _ _ _ $@ _).
+    refine (_ $@L (_ $@L (cate_buildequiv_fun g)^$ $@R _) $@ _).
+    nrefine (_ $@L (cate_issect (Build_CatEquiv g) $@R _) $@ _).
+    nrefine (_ $@L cat_idl _ $@ _).
+    refine (_ $@L (cate_buildequiv_fun f)^$ $@ _).
+    nrapply cate_issect.
 Defined.
 
+Global Instance compose_catie {A} `{HasEquivs A} {a b c : A}
+  (g : b $<~> c) (f : a $<~> b)
+  : CatIsEquiv (g $o f)
+  := compose_catie' g f.
+
 Definition compose_cate {A} `{HasEquivs A} {a b c : A}
   (g : b $<~> c) (f : a $<~> b) : a $<~> c
   := Build_CatEquiv (g $o f).
@@ -190,7 +200,7 @@ Proof.
   apply cate_buildequiv_fun.
 Defined.
 
-Definition id_cate_fun {A} `{HasEquivs A} (a : A) 
+Definition id_cate_fun {A} `{HasEquivs A} (a : A)
   : cate_fun (id_cate a) $== Id a.
 Proof.
   apply cate_buildequiv_fun.
@@ -325,7 +335,9 @@ Definition cate_inv_compose {A} `{HasEquivs A} {a b c : A} (e : a $<~> b) (f : b
   : cate_fun (f $oE e)^-1$ $== cate_fun (e^-1$ $oE f^-1$).
 Proof.
   refine (_ $@ (compose_cate_fun _ _)^$).
-  apply cate_inv_adjointify.
+  nrefine (cate_inv_adjointify _ _ _ _ $@ _).
+  nrefine (cate_inv2 (cate_buildequiv_fun _) $@R _ $@ _).
+  exact (_ $@L cate_inv2 (cate_buildequiv_fun _)).
 Defined.
 
 Definition cate_inv_V {A} `{HasEquivs A} {a b : A} (e : a $<~> b)

From 2ae47ce8fb16bb7de5467e5a758eb6044549803f Mon Sep 17 00:00:00 2001
From: gio256 <102917377+gio256@users.noreply.github.com>
Date: Sun, 10 Mar 2024 17:14:34 -0600
Subject: [PATCH 17/25] Move bifunctor lemmas from Prod.v to Bifunctor.v

---
 contrib/SetoidRewrite.v      |  35 +-----------
 theories/WildCat/Bifunctor.v | 107 +++++++++++++++++++++++------------
 theories/WildCat/Prod.v      |  70 ++++++++---------------
 3 files changed, 99 insertions(+), 113 deletions(-)

diff --git a/contrib/SetoidRewrite.v b/contrib/SetoidRewrite.v
index 83fcfbbf3bb..d01c68cb008 100644
--- a/contrib/SetoidRewrite.v
+++ b/contrib/SetoidRewrite.v
@@ -99,7 +99,7 @@ Proof.
   intros f1 f2.
   apply (is0functor_postcomp a b c g ).
 Defined.
-                  
+
 #[export] Instance IsProper_catcomp {A : Type} `{Is1Cat A}
   {a b c : A}
   : CMorphisms.Proper (GpdHom ==> GpdHom ==> GpdHom)
@@ -111,7 +111,7 @@ Proof.
   exact eq_g.
 Defined.
 
-#[export] Instance gpd_hom_to_hom_proper {A B: Type} `{Is0Gpd A} 
+#[export] Instance gpd_hom_to_hom_proper {A B: Type} `{Is0Gpd A}
   {R : Relation B} (F : A -> B)
   `{CMorphisms.Proper _ (GpdHom ==> R) F}
   : CMorphisms.Proper (Hom ==> R) F.
@@ -119,35 +119,6 @@ Proof.
   intros a b eq_ab; apply H2; exact eq_ab.
 Defined.
 
-#[export] Instance Is1Functor_uncurry_bifunctor {A B C : Type}
-  `{Is1Cat A, Is1Cat B, Is1Cat C}
-  (F : A -> B -> C)
-  `{!Is0Bifunctor F, !Is1Bifunctor F}
-  : Is1Functor (uncurry F).
-Proof.
-  nrapply Build_Is1Functor.
-  - intros [a1 a2] [b1 b2] [f1 f2] [g1 g2] [eq_fg1 eq_fg2];
-      cbn in f1, f2, g1, g2, eq_fg1, eq_fg2. cbn.
-    rewrite eq_fg1, eq_fg2.
-    reflexivity.
-  - intros [a b]; cbn.
-    (* rewrite fmap_id generates an extra goal. Not sure how to get typeclass resolution to figure this out automatically. *)
-    rewrite (fmap_id _).
-    rewrite (fmap_id _).
-    rewrite cat_idl.
-    reflexivity.
-  - intros [a1 b1] [a2 b2] [a3 b3] [f1 f2] [g1 g2];
-      cbn in f1, f2, g1, g2.
-    cbn.
-    rewrite (fmap_comp _).
-    rewrite (fmap_comp _).
-    rewrite cat_assoc.
-    rewrite <- (cat_assoc _ (fmap (F a1) g2)).
-    rewrite <- (bifunctor_isbifunctor F f1 g2).
-    rewrite ! cat_assoc.
-    reflexivity.
-Defined.
-
 #[export] Instance gpd_hom_is_proper1 {A : Type} `{Is0Gpd A}
  : CMorphisms.Proper
      (Hom ==> Hom ==> CRelationClasses.arrow) Hom.
@@ -192,7 +163,7 @@ Defined.
 
 Proposition nat_equiv_faithful {A B : Type}
   {F G : A -> B} `{Is1Functor _ _ F}
-  `{!Is0Functor G, !Is1Functor G} 
+  `{!Is0Functor G, !Is1Functor G}
   `{!HasEquivs B} (tau : NatEquiv F G)
   : Faithful F -> Faithful G.
 Proof.
diff --git a/theories/WildCat/Bifunctor.v b/theories/WildCat/Bifunctor.v
index f5775cfdf5b..7ecd7dd4bff 100644
--- a/theories/WildCat/Bifunctor.v
+++ b/theories/WildCat/Bifunctor.v
@@ -1,6 +1,6 @@
 Require Import Basics.Overture Basics.Tactics.
 Require Import Types.Forall.
-Require Import WildCat.Core WildCat.Prod.
+Require Import WildCat.Core WildCat.Prod WildCat.Equiv.
 
 (** * Bifunctors between WildCats *)
 
@@ -56,18 +56,84 @@ Definition Build_Is1Bifunctor' {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
   : Is1Bifunctor F
   := is1bifunctor_functor_uncurried (uncurry F).
 
-(* fmap in the first argument *)
-Definition fmap10 {A B C : Type} `{Is01Cat A, Is01Cat B, Is1Cat C}
+(** [fmap] in the first argument *)
+Definition fmap10 {A B C : Type} `{IsGraph A, IsGraph B, IsGraph C}
   (F : A -> B -> C) `{!Is0Bifunctor F} {a0 a1 : A} (f : a0 $-> a1) (b : B)
   : (F a0 b) $-> (F a1 b)
   := fmap (flip F b) f.
 
-(* fmap in the second argument *)
-Definition fmap01 {A B C : Type} `{Is01Cat A, Is01Cat B, Is1Cat C}
+(** [fmap] in the second argument *)
+Definition fmap01 {A B C : Type} `{IsGraph A, IsGraph B, IsGraph C}
   (F : A -> B -> C) `{!Is0Bifunctor F} (a : A) {b0 b1 : B} (g : b0 $-> b1)
   : F a b0 $-> F a b1
   := fmap (F a) g.
 
+(** There are two ways to [fmap] in both arguments of a bifunctor. The bifunctor coherence condition ([bifunctor_isbifunctor]) states precisely that these two routes agree. *)
+Definition fmap11 {A B C : Type} `{IsGraph A, IsGraph B, Is01Cat C}
+  (F : A -> B -> C) `{!Is0Bifunctor F} {a0 a1 : A} (f : a0 $-> a1)
+  {b0 b1 : B} (g : b0 $-> b1)
+  : F a0 b0 $-> F a1 b1
+  := fmap (F _) g $o fmap (flip F _) f.
+
+Definition fmap11' {A B C : Type} `{IsGraph A, IsGraph B, Is01Cat C}
+  (F : A -> B -> C) `{!Is0Bifunctor F} {a0 a1 : A} (f : a0 $-> a1)
+  {b0 b1 : B} (g : b0 $-> b1)
+  : F a0 b0 $-> F a1 b1
+  := fmap (flip F _) f $o fmap (F _) g.
+
+Definition fmap22 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
+  (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
+  {a0 a1 : A} {f : a0 $-> a1} {f' : a0 $-> a1}
+  {b0 b1 : B} {g : b0 $-> b1} {g' : b0 $-> b1}
+  (p : f $== f') (q : g $== g')
+  : fmap11 F f g $== fmap11 F f' g'
+  := fmap2 (F _) q $@R _ $@ (_ $@L fmap2 (flip F _) p).
+
+Global Instance iemap11 {A B C : Type} `{HasEquivs A, HasEquivs B, HasEquivs C}
+  (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
+  {a0 a1 : A} (f : a0 $<~> a1) {b0 b1 : B} (g : b0 $<~> b1)
+  : CatIsEquiv (fmap11 F f g).
+Proof.
+  rapply compose_catie'.
+  exact (iemap (flip F _) f).
+Defined.
+
+Definition emap11 {A B C : Type} `{HasEquivs A, HasEquivs B, HasEquivs C}
+  (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
+  {a0 a1 : A} (f : a0 $<~> a1) {b0 b1 : B} (g : b0 $<~> b1)
+  : F a0 b0 $<~> F a1 b1
+  := Build_CatEquiv (fmap11 F f g).
+
+(** Any 0-bifunctor [A -> B -> C] can be made into a functor from the product category [A * B -> C] in two ways. *)
+Global Instance is0functor_uncurry_bifunctor {A B C : Type}
+  `{IsGraph A, IsGraph B, Is01Cat C} (F : A -> B -> C) `{!Is0Bifunctor F}
+  : Is0Functor (uncurry F).
+Proof.
+  nrapply Build_Is0Functor.
+  intros a b [f g].
+  exact (fmap11 F f g).
+Defined.
+
+(** Any 1-bifunctor defines a canonical functor from the product category. *)
+Global Instance is1functor_uncurry_bifunctor {A B C : Type}
+  `{Is1Cat A, Is1Cat B, Is1Cat C} (F : A -> B -> C)
+  `{!Is0Bifunctor F, !Is1Bifunctor F}
+  : Is1Functor (uncurry F).
+Proof.
+  nrapply Build_Is1Functor.
+  - intros x y f g [p q].
+    exact (fmap22 F p q).
+  - intros x.
+    refine (fmap_id (F _) _ $@R _ $@ _).
+    refine (_ $@L fmap_id (flip F _) _ $@ cat_idl _).
+  - intros x y z f g.
+    refine (fmap_comp (F _) _ _ $@R _ $@ _).
+    refine (_ $@L fmap_comp (flip F _) _ _  $@ _).
+    nrefine (cat_assoc_opp _ _ _ $@ _ $@ cat_assoc _ _ _).
+    nrefine (cat_assoc _ _ _ $@R _ $@ _ $@ (cat_assoc_opp _ _ _ $@R _)).
+    exact (_ $@L bifunctor_isbifunctor F _ _ $@R _).
+Defined.
+
 (** Restricting a functor along a bifunctor yields a bifunctor. *)
 Global Instance is0bifunctor_compose {A B C D : Type}
   `{IsGraph A, IsGraph B, Is1Cat C, Is1Cat D}
@@ -108,34 +174,3 @@ Proof.
     rapply fmap2.
     exact (bifunctor_isbifunctor F f g).
 Defined.
-
-(** Any 0-bifunctor [A -> B -> C] can be made into a functor from the product category [A * B -> C] in two ways. The bifunctor coherence condition ([bifunctor_isbifunctor]) states precisely that these two routes agree. *)
-Global Instance is0functor_uncurry_bifunctor {A B C : Type}
-  `{IsGraph A, IsGraph B, Is1Cat C} (F : A -> B -> C) `{!Is0Bifunctor F}
-  : Is0Functor (uncurry F).
-Proof.
-  nrapply Build_Is0Functor.
-  intros [a b] [c d] [f g].
-  exact (fmap (flip F d) f $o fmap (F a) g).
-Defined.
-
-(** Any 1-bifunctor defines a canonical functor from the product category. *)
-Global Instance is1functor_uncurry_bifunctor {A B C : Type}
-  `{Is1Cat A, Is1Cat B, Is1Cat C} (F : A -> B -> C)
-  `{!Is0Bifunctor F, !Is1Bifunctor F}
-  : Is1Functor (uncurry F).
-Proof.
-  nrapply Build_Is1Functor.
-  - intros x y f g [p q].
-    refine (fmap2 (flip F _) p $@R _ $@ _).
-    exact (_ $@L fmap2 (F _) q).
-  - intros x.
-    refine (fmap_id (flip F _) _ $@R _ $@ _).
-    refine (_ $@L fmap_id (F _) _ $@ cat_idl _).
-  - intros x y z f g.
-    refine (fmap_comp (flip F _) _ _ $@R _ $@ _).
-    refine (_ $@L fmap_comp (F _) _ _  $@ _).
-    refine (cat_assoc_opp _ _ _ $@ _ $@ cat_assoc _ _ _).
-    refine (cat_assoc _ _ _ $@R _ $@ _ $@ (cat_assoc_opp _ _ _ $@R _)).
-    exact (_ $@L (bifunctor_isbifunctor F _ _)^$ $@R _).
-Defined.
diff --git a/theories/WildCat/Prod.v b/theories/WildCat/Prod.v
index e2bbdc4d066..4b94a24a9b0 100644
--- a/theories/WildCat/Prod.v
+++ b/theories/WildCat/Prod.v
@@ -21,16 +21,9 @@ Proof.
     exact (f1 $o f2 , g1 $o g2).
 Defined.
 
-(** To avoid having to define a separate notion of "two-variable functor", we define two-variable functors in uncurried form.  The following definition applies such a two-variable functor, with a currying built in. *)
-Definition fmap11 {A B C : Type} `{IsGraph A} `{IsGraph B} `{IsGraph C}
-  (F : A -> B -> C) {H2 : Is0Functor (uncurry F)}
-  {a1 a2 : A} {b1 b2 : B} (f1 : a1 $-> a2) (f2 : b1 $-> b2)
-  : F a1 b1 $-> F a2 b2
-  := @fmap _ _ _ _ (uncurry F) H2 (a1, b1) (a2, b2) (f1, f2).
-
 Global Instance is0gpd_prod A B `{Is0Gpd A} `{Is0Gpd B}
  : Is0Gpd (A * B).
-Proof. 
+Proof.
   srapply Build_Is0Gpd.
   intros [x1 x2] [y1 y2] [f1 f2].
   cbn in *.
@@ -49,12 +42,12 @@ Global Instance is1cat_prod A B `{Is1Cat A} `{Is1Cat B}
 Proof.
   srapply (Build_Is1Cat).
   - intros [x1 x2] [y1 y2] [z1 z2] [h1 h2].
-    srapply Build_Is0Functor.  
-    intros [f1 f2] [g1 g2] [p1 p2]; cbn in *. 
+    srapply Build_Is0Functor.
+    intros [f1 f2] [g1 g2] [p1 p2]; cbn in *.
     exact ( h1 $@L p1 , h2 $@L p2 ).
   - intros [x1 x2] [y1 y2] [z1 z2] [h1 h2].
-    srapply Build_Is0Functor.  
-    intros [f1 f2] [g1 g2] [p1 p2]; cbn in *. 
+    srapply Build_Is0Functor.
+    intros [f1 f2] [g1 g2] [p1 p2]; cbn in *.
     exact ( p1 $@R h1 , p2 $@R h2 ).
   - intros [a1 a2] [b1 b2] [c1 c2] [d1 d2] [f1 f2] [g1 g2] [h1 h2].
     cbn in *.
@@ -64,10 +57,9 @@ Proof.
     exact (cat_idl _, cat_idl _).
   - intros [a1 a2] [b1 b2] [g1 g2].
     cbn in *.
-    exact (cat_idr _, cat_idr _). 
+    exact (cat_idr _, cat_idr _).
 Defined.
 
-
 (** Product categories inherit equivalences *)
 
 Global Instance hasequivs_prod A B `{HasEquivs A} `{HasEquivs B}
@@ -97,27 +89,6 @@ Global Instance isequivs_prod A B `{HasEquivs A} `{HasEquivs B}
        {ef : CatIsEquiv f} {eg : CatIsEquiv g}
   : @CatIsEquiv (A*B) _ _ _ _ _ (a1,b1) (a2,b2) (f,g) := (ef,eg).
 
-(** More coherent two-variable functors. *)
-
-Definition fmap22 {A B C : Type} `{Is1Cat A} `{Is1Cat B} `{Is1Cat C}
-  (F : A -> B -> C) `{!Is0Functor (uncurry F), !Is1Functor (uncurry F)}
-  {a1 a2 : A} {b1 b2 : B} (f1 : a1 $-> a2) (f2 : b1 $-> b2) (g1 : a1 $-> a2) (g2 : b1 $-> b2)
-  (alpha : f1 $== g1) (beta : f2 $== g2)
-  : (fmap11 F f1 f2) $== (fmap11 F g1 g2)
-  := @fmap2 _ _ _ _ _ _ _ _ _ _ (uncurry F) _ _ (a1, b1) (a2, b2) (f1, f2) (g1, g2) (alpha, beta).
-
-Global Instance iemap11 {A B C : Type} `{HasEquivs A} `{HasEquivs B} `{HasEquivs C}
-           (F : A -> B -> C) `{!Is0Functor (uncurry F), !Is1Functor (uncurry F)}
-           {a1 a2 : A} {b1 b2 : B} (f1 : a1 $<~> a2) (f2 : b1 $<~> b2)
-  : CatIsEquiv (fmap11 F f1 f2)
-  := @iemap _ _ _ _ _ _ _ _ _ _ _ _ (uncurry F) _ _ (a1, b1) (a2, b2) (f1, f2).
-
-Definition emap11 {A B C : Type} `{HasEquivs A} `{HasEquivs B} `{HasEquivs C}
-           (F : A -> B -> C) `{!Is0Functor (uncurry F), !Is1Functor (uncurry F)}
-           {a1 a2 : A} {b1 b2 : B} (fe1 : a1 $<~> a2)
-           (fe2 : b1 $<~> b2) : (F a1 b1) $<~> (F a2 b2)
-  := @emap _ _ _ _ _ _ _ _ _ _ _ _ (uncurry F) _ _ (a1, b1) (a2, b2) (fe1, fe2).
-
 (** ** Product functors *)
 
 Global Instance is0functor_prod_functor {A B C D : Type}
@@ -179,8 +150,8 @@ Defined.
 
 (** Inclusions into a product category are functorial. *)
 
-(* [A * {b}] *)
-Global Instance is0functor_prod_include10 {A B : Type} `{IsGraph A, Is01Cat B} (b : B)
+Global Instance is0functor_prod_include10 {A B : Type} `{IsGraph A, Is01Cat B}
+  (b : B)
   : Is0Functor (fun a : A => (a, b)).
 Proof.
   nrapply Build_Is0Functor.
@@ -188,7 +159,8 @@ Proof.
   exact (f, Id b).
 Defined.
 
-Global Instance is1functor_prod_include10 {A B : Type} `{Is1Cat A, Is1Cat B} (b : B)
+Global Instance is1functor_prod_include10 {A B : Type} `{Is1Cat A, Is1Cat B}
+  (b : B)
   : Is1Functor (fun a : A => (a, b)).
 Proof.
   nrapply Build_Is1Functor.
@@ -199,8 +171,8 @@ Proof.
     exact (Id _, (cat_idl _)^$).
 Defined.
 
-(* [{a} * B] *)
-Global Instance is0functor_prod_include01 {A B : Type} `{Is01Cat A, IsGraph B} (a : A)
+Global Instance is0functor_prod_include01 {A B : Type} `{Is01Cat A, IsGraph B}
+  (a : A)
   : Is0Functor (fun b : B => (a, b)).
 Proof.
   nrapply Build_Is0Functor.
@@ -208,7 +180,8 @@ Proof.
   exact (Id a, f).
 Defined.
 
-Global Instance is1functor_prod_include01 {A B : Type} `{Is1Cat A, Is1Cat B} (a : A)
+Global Instance is1functor_prod_include01 {A B : Type} `{Is1Cat A, Is1Cat B}
+  (a : A)
   : Is1Functor (fun b : B => (a, b)).
 Proof.
   nrapply Build_Is1Functor.
@@ -222,25 +195,32 @@ Defined.
 (** Functors from a product category are functorial in each argument *)
 
 Global Instance is0functor_functor_uncurried01 {A B C : Type}
-  `{Is01Cat A} `{IsGraph B} `{IsGraph C}
+  `{Is01Cat A, IsGraph B, IsGraph C}
   (F : A * B -> C) `{!Is0Functor F} (a : A)
   : Is0Functor (fun b => F (a, b))
   := is0functor_compose (fun b => (a, b)) F.
 
 Global Instance is1functor_functor_uncurried01 {A B C : Type}
-  `{Is1Cat A} `{Is1Cat B} `{Is1Cat C}
+  `{Is1Cat A, Is1Cat B, Is1Cat C}
   (F : A * B -> C) `{!Is0Functor F, !Is1Functor F} (a : A)
   : Is1Functor (fun b => F (a, b))
   := is1functor_compose (fun b => (a, b)) F.
 
 Global Instance is0functor_functor_uncurried10 {A B C : Type}
-  `{IsGraph A} `{Is01Cat B} `{IsGraph C}
+  `{IsGraph A, Is01Cat B, IsGraph C}
   (F : A * B -> C) `{!Is0Functor F} (b : B)
   : Is0Functor (fun a => F (a, b))
   := is0functor_compose (fun a => (a, b)) F.
 
 Global Instance is1functor_functor_uncurried10 {A B C : Type}
-  `{Is1Cat A} `{Is1Cat B} `{Is1Cat C}
+  `{Is1Cat A, Is1Cat B, Is1Cat C}
   (F : A * B -> C) `{!Is0Functor F, !Is1Functor F} (b : B)
   : Is1Functor (fun a => F (a, b))
   := is1functor_compose (fun a => (a, b)) F.
+
+(** Applies a two variable functor via uncurrying. Note that the precondition on [C] is slightly weaker than that of [Bifunctor.fmap11]. *)
+Definition fmap11_uncurry {A B C : Type} `{IsGraph A, IsGraph B, IsGraph C}
+  (F : A -> B -> C) {H2 : Is0Functor (uncurry F)}
+  {a0 a1 : A} (f : a0 $-> a1) {b0 b1 : B} (g : b0 $-> b1)
+  : F a0 b0 $-> F a1 b1
+  := @fmap _ _ _ _ (uncurry F) H2 (a0, b0) (a1, b1) (f, g).

From 1426fd97d380cfeb94d1c57205430a84a92332f4 Mon Sep 17 00:00:00 2001
From: gio256 <102917377+gio256@users.noreply.github.com>
Date: Mon, 11 Mar 2024 13:52:58 -0600
Subject: [PATCH 18/25] WildCat/Bifunctor.v: clean up two proofs

---
 theories/WildCat/Bifunctor.v | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/theories/WildCat/Bifunctor.v b/theories/WildCat/Bifunctor.v
index 7ecd7dd4bff..67017860dac 100644
--- a/theories/WildCat/Bifunctor.v
+++ b/theories/WildCat/Bifunctor.v
@@ -87,7 +87,7 @@ Definition fmap22 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
   {b0 b1 : B} {g : b0 $-> b1} {g' : b0 $-> b1}
   (p : f $== f') (q : g $== g')
   : fmap11 F f g $== fmap11 F f' g'
-  := fmap2 (F _) q $@R _ $@ (_ $@L fmap2 (flip F _) p).
+  := fmap2 (flip F _) p $@@ fmap2 (F _) q.
 
 Global Instance iemap11 {A B C : Type} `{HasEquivs A, HasEquivs B, HasEquivs C}
   (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
@@ -124,11 +124,10 @@ Proof.
   - intros x y f g [p q].
     exact (fmap22 F p q).
   - intros x.
-    refine (fmap_id (F _) _ $@R _ $@ _).
-    refine (_ $@L fmap_id (flip F _) _ $@ cat_idl _).
+    refine (fmap_id (flip F _) _ $@@ fmap_id (F _) _ $@ _).
+    apply cat_idl.
   - intros x y z f g.
-    refine (fmap_comp (F _) _ _ $@R _ $@ _).
-    refine (_ $@L fmap_comp (flip F _) _ _  $@ _).
+    refine (fmap_comp (flip F _) _ _ $@@ fmap_comp (F _) _ _ $@ _ ).
     nrefine (cat_assoc_opp _ _ _ $@ _ $@ cat_assoc _ _ _).
     nrefine (cat_assoc _ _ _ $@R _ $@ _ $@ (cat_assoc_opp _ _ _ $@R _)).
     exact (_ $@L bifunctor_isbifunctor F _ _ $@R _).

From b662a72748a3880b051673536c0845f0900189c4 Mon Sep 17 00:00:00 2001
From: gio256 <102917377+gio256@users.noreply.github.com>
Date: Mon, 11 Mar 2024 13:53:15 -0600
Subject: [PATCH 19/25] WildCat equivs: re-define compose_catie'

---
 theories/WildCat/DisplayedEquiv.v | 68 ++++++++++++++++++-------------
 theories/WildCat/Equiv.v          | 52 +++++++++++++----------
 2 files changed, 70 insertions(+), 50 deletions(-)

diff --git a/theories/WildCat/DisplayedEquiv.v b/theories/WildCat/DisplayedEquiv.v
index 713b743dcd0..9a38a6aa1e0 100644
--- a/theories/WildCat/DisplayedEquiv.v
+++ b/theories/WildCat/DisplayedEquiv.v
@@ -171,44 +171,58 @@ Global Instance reflexive_dcate {A} {D : A -> Type} `{DHasEquivs A D} {a : A}
   : Reflexive (DCatEquiv (id_cate a))
   := did_cate.
 
-(** Equivalences can be composed. *)
-Global Instance dcompose_catie' {A} {D : A -> Type} `{DHasEquivs A D}
-  {a b c : A} {g : b $-> c} `{!CatIsEquiv g} {f : a $-> b} `{!CatIsEquiv f}
-  {a' : D a} {b' : D b} {c' : D c}
-  (g' : DHom g b' c') `{ge' : !DCatIsEquiv g'}
-  (f' : DHom f a' b') `{fe' : !DCatIsEquiv f'}
-  : DCatIsEquiv (fe:=compose_catie' g f) (g' $o' f').
+(** Anything homotopic to an equivalence is an equivalence. This should not be an instance. *)
+Definition dcate_homotopic {A} {D : A -> Type} `{DHasEquivs A D} {a b : A}
+  {f : a $-> b} `{!CatIsEquiv f} {g : a $-> b} {p : f $== g} {a' : D a}
+  {b' : D b} (f' : DHom f a' b') `{fe' : !DCatIsEquiv f'} {g' : DHom g a' b'}
+  (p' : DGpdHom p f' g')
+  : DCatIsEquiv (fe:=cate_homotopic f p) g'.
 Proof.
   snrapply dcatie_adjointify.
-  - refine (_ $o' _).
-    1: nrapply (Build_DCatEquiv f')^-1$'; exact fe'.
-    nrapply (Build_DCatEquiv g')^-1$'; exact ge'.
-  - refine (dcat_assoc _ _ _ $@' _).
-    refine (_ $@L' ((dcate_buildequiv_fun f')^$' $@R' _ ) $@' _).
+  - exact (Build_DCatEquiv (fe':=fe') f')^-1$'.
+  - refine (p'^$' $@R' _ $@' _).
     1: exact isd0gpd_hom.
-    refine (_ $@L' dcat_assoc_opp _ _ _ $@' _).
-    refine (_ $@L' (dcate_isretr (Build_DCatEquiv f') $@R' _) $@' _).
-    refine (_ $@L' dcat_idl _ $@' _).
-    refine ((dcate_buildequiv_fun g')^$' $@R' _ $@' _).
+    refine ((dcate_buildequiv_fun f')^$' $@R' _ $@' _).
     1: exact isd0gpd_hom.
-    nrapply dcate_isretr.
-  - refine (dcat_assoc _ _ _ $@' _).
-    refine (_ $@L' dcat_assoc_opp _ _ _ $@' _).
-    refine (_ $@L' (_ $@L' (dcate_buildequiv_fun g')^$' $@R' _) $@' _).
+    apply dcate_isretr.
+  - refine (_ $@L' p'^$' $@' _).
     1: exact isd0gpd_hom.
-    refine (_ $@L' (dcate_issect (Build_DCatEquiv g') $@R' _) $@' _).
-    refine (_ $@L' dcat_idl _ $@' _).
     refine (_ $@L' (dcate_buildequiv_fun f')^$' $@' _).
     1: exact isd0gpd_hom.
-    nrapply dcate_issect.
+    apply dcate_issect.
 Defined.
 
+(** Equivalences can be composed. *)
 Global Instance dcompose_catie {A} {D : A -> Type} `{DHasEquivs A D}
   {a b c : A} {g : b $<~> c} {f : a $<~> b} {a' : D a} {b' : D b} {c' : D c}
   (g' : DCatEquiv g b' c') (f' : DCatEquiv f a' b')
   : DCatIsEquiv (dcate_fun g' $o' f').
 Proof.
-  rapply dcompose_catie'.
+  snrapply dcatie_adjointify.
+  - exact (dcate_fun f'^-1$' $o' g'^-1$').
+  - refine (dcat_assoc _ _ _ $@' _).
+    refine (_ $@L' dcat_assoc_opp _ _ _ $@' _).
+    refine (_ $@L' (dcate_isretr _ $@R' _) $@' _).
+    refine (_ $@L' dcat_idl _ $@' _).
+    apply dcate_isretr.
+  - refine (dcat_assoc _ _ _ $@' _).
+    refine (_ $@L' dcat_assoc_opp _ _ _ $@' _).
+    refine (_ $@L' (dcate_issect _ $@R' _) $@' _).
+    refine (_ $@L' dcat_idl _ $@' _).
+    apply dcate_issect.
+Defined.
+
+Global Instance dcompose_catie' {A} {D : A -> Type} `{DHasEquivs A D}
+  {a b c : A} {g : b $-> c} `{!CatIsEquiv g} {f : a $-> b} `{!CatIsEquiv f}
+  {a' : D a} {b' : D b} {c' : D c}
+  (g' : DHom g b' c') `{ge' : !DCatIsEquiv g'}
+  (f' : DHom f a' b') `{fe' : !DCatIsEquiv f'}
+  : DCatIsEquiv (fe:=compose_catie' g f) (g' $o' f').
+Proof.
+  pose (ff:=Build_DCatEquiv (fe':=fe') f').
+  pose (gg:=Build_DCatEquiv (fe':=ge') g').
+  nrefine (dcate_homotopic (fe':=dcompose_catie gg ff) _ _).
+  exact (dcate_buildequiv_fun _ $@@' dcate_buildequiv_fun _).
 Defined.
 
 Definition dcompose_cate {A} {D : A -> Type} `{DHasEquivs A D}
@@ -407,10 +421,8 @@ Definition dcate_inv_compose {A} {D : A -> Type} `{DHasEquivs A D}
     (dcate_fun (f' $oE' e')^-1$') (dcate_fun (e'^-1$' $oE' f'^-1$')).
 Proof.
   refine (_ $@' (dcompose_cate_fun e'^-1$' f'^-1$')^$').
-  2: exact isd0gpd_hom.
-  refine (dcate_inv_adjointify _ _ _ _ $@' _).
-  refine (dcate_inv2 (dcate_buildequiv_fun _) $@R' _ $@' _).
-  exact (_ $@L' dcate_inv2 (dcate_buildequiv_fun _)).
+  - snrapply dcate_inv_adjointify.
+  - exact isd0gpd_hom.
 Defined.
 
 Definition dcate_inv_V {A} {D : A -> Type} `{DHasEquivs A D}
diff --git a/theories/WildCat/Equiv.v b/theories/WildCat/Equiv.v
index e8c8a3153de..8d5667c1c9c 100644
--- a/theories/WildCat/Equiv.v
+++ b/theories/WildCat/Equiv.v
@@ -151,33 +151,43 @@ Global Instance symmetric_cate {A} `{HasEquivs A}
   : Symmetric (@CatEquiv A _ _ _ _ _)
   := fun a b f => cate_inv f.
 
-(** Equivalences can be composed. *)
-Definition compose_catie' {A} `{HasEquivs A} {a b c : A}
-  (g : b $-> c) `{!CatIsEquiv g} (f : a $-> b) `{!CatIsEquiv f}
-  : CatIsEquiv (g $o f).
+(** Anything homotopic to an equivalence is an equivalence. This should not be an instance. *)
+Definition cate_homotopic {A} `{HasEquivs A} {a b : A}
+  (f : a $-> b) `{!CatIsEquiv f} {g : a $-> b} (p : f $== g)
+  : CatIsEquiv g.
 Proof.
   snrapply catie_adjointify.
-  - exact ((Build_CatEquiv f)^-1$ $o (Build_CatEquiv g)^-1$).
-  - nrefine (cat_assoc _ _ _ $@ _).
-    refine (_ $@L ((cate_buildequiv_fun f)^$ $@R _ ) $@ _).
-    nrefine (_ $@L cat_assoc_opp _ _ _ $@ _).
-    nrefine (_ $@L (cate_isretr (Build_CatEquiv f) $@R _) $@ _).
-    nrefine (_ $@L cat_idl _ $@ _).
-    refine ((cate_buildequiv_fun g)^$ $@R _ $@ _).
-    nrapply cate_isretr.
-  - nrefine (cat_assoc _ _ _ $@ _).
-    nrefine (_ $@L cat_assoc_opp _ _ _ $@ _).
-    refine (_ $@L (_ $@L (cate_buildequiv_fun g)^$ $@R _) $@ _).
-    nrefine (_ $@L (cate_issect (Build_CatEquiv g) $@R _) $@ _).
-    nrefine (_ $@L cat_idl _ $@ _).
+  - exact (Build_CatEquiv f)^-1$.
+  - refine (p^$ $@R _ $@ _).
+    refine ((cate_buildequiv_fun f)^$ $@R _ $@ _).
+    apply cate_isretr.
+  - refine (_ $@L p^$ $@ _).
     refine (_ $@L (cate_buildequiv_fun f)^$ $@ _).
-    nrapply cate_issect.
+    apply cate_issect.
 Defined.
 
+(** Equivalences can be composed. *)
 Global Instance compose_catie {A} `{HasEquivs A} {a b c : A}
   (g : b $<~> c) (f : a $<~> b)
+  : CatIsEquiv (g $o f).
+Proof.
+  refine (catie_adjointify _ (f^-1$ $o g^-1$) _ _).
+  - refine (cat_assoc _ _ _ $@ _).
+    refine ((_ $@L cat_assoc_opp _ _ _) $@ _).
+    refine ((_ $@L (cate_isretr _ $@R _)) $@ _).
+    refine ((_ $@L cat_idl _) $@ _).
+    apply cate_isretr.
+  - refine (cat_assoc _ _ _ $@ _).
+    refine ((_ $@L cat_assoc_opp _ _ _) $@ _).
+    refine ((_ $@L (cate_issect _ $@R _)) $@ _).
+    refine ((_ $@L cat_idl _) $@ _).
+    apply cate_issect.
+Defined.
+
+Global Instance compose_catie' {A} `{HasEquivs A} {a b c : A}
+  (g : b $-> c) `{!CatIsEquiv g} (f : a $-> b) `{!CatIsEquiv f}
   : CatIsEquiv (g $o f)
-  := compose_catie' g f.
+  := cate_homotopic _ (cate_buildequiv_fun _ $@@ cate_buildequiv_fun _).
 
 Definition compose_cate {A} `{HasEquivs A} {a b c : A}
   (g : b $<~> c) (f : a $<~> b) : a $<~> c
@@ -335,9 +345,7 @@ Definition cate_inv_compose {A} `{HasEquivs A} {a b c : A} (e : a $<~> b) (f : b
   : cate_fun (f $oE e)^-1$ $== cate_fun (e^-1$ $oE f^-1$).
 Proof.
   refine (_ $@ (compose_cate_fun _ _)^$).
-  nrefine (cate_inv_adjointify _ _ _ _ $@ _).
-  nrefine (cate_inv2 (cate_buildequiv_fun _) $@R _ $@ _).
-  exact (_ $@L cate_inv2 (cate_buildequiv_fun _)).
+  apply cate_inv_adjointify.
 Defined.
 
 Definition cate_inv_V {A} `{HasEquivs A} {a b : A} (e : a $<~> b)

From f902579697037eb6e8341f5dbd0679e7e0fc7fbb Mon Sep 17 00:00:00 2001
From: gio256 <102917377+gio256@users.noreply.github.com>
Date: Tue, 12 Mar 2024 10:32:59 -0600
Subject: [PATCH 20/25] WildCat equivs fix: cate_homotopic to catie_homotopic

---
 theories/WildCat/DisplayedEquiv.v | 6 +++---
 theories/WildCat/Equiv.v          | 4 ++--
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/theories/WildCat/DisplayedEquiv.v b/theories/WildCat/DisplayedEquiv.v
index 9a38a6aa1e0..2ed8b3c2ce0 100644
--- a/theories/WildCat/DisplayedEquiv.v
+++ b/theories/WildCat/DisplayedEquiv.v
@@ -172,11 +172,11 @@ Global Instance reflexive_dcate {A} {D : A -> Type} `{DHasEquivs A D} {a : A}
   := did_cate.
 
 (** Anything homotopic to an equivalence is an equivalence. This should not be an instance. *)
-Definition dcate_homotopic {A} {D : A -> Type} `{DHasEquivs A D} {a b : A}
+Definition dcatie_homotopic {A} {D : A -> Type} `{DHasEquivs A D} {a b : A}
   {f : a $-> b} `{!CatIsEquiv f} {g : a $-> b} {p : f $== g} {a' : D a}
   {b' : D b} (f' : DHom f a' b') `{fe' : !DCatIsEquiv f'} {g' : DHom g a' b'}
   (p' : DGpdHom p f' g')
-  : DCatIsEquiv (fe:=cate_homotopic f p) g'.
+  : DCatIsEquiv (fe:=catie_homotopic f p) g'.
 Proof.
   snrapply dcatie_adjointify.
   - exact (Build_DCatEquiv (fe':=fe') f')^-1$'.
@@ -221,7 +221,7 @@ Global Instance dcompose_catie' {A} {D : A -> Type} `{DHasEquivs A D}
 Proof.
   pose (ff:=Build_DCatEquiv (fe':=fe') f').
   pose (gg:=Build_DCatEquiv (fe':=ge') g').
-  nrefine (dcate_homotopic (fe':=dcompose_catie gg ff) _ _).
+  nrefine (dcatie_homotopic (fe':=dcompose_catie gg ff) _ _).
   exact (dcate_buildequiv_fun _ $@@' dcate_buildequiv_fun _).
 Defined.
 
diff --git a/theories/WildCat/Equiv.v b/theories/WildCat/Equiv.v
index 8d5667c1c9c..7da515c8a94 100644
--- a/theories/WildCat/Equiv.v
+++ b/theories/WildCat/Equiv.v
@@ -152,7 +152,7 @@ Global Instance symmetric_cate {A} `{HasEquivs A}
   := fun a b f => cate_inv f.
 
 (** Anything homotopic to an equivalence is an equivalence. This should not be an instance. *)
-Definition cate_homotopic {A} `{HasEquivs A} {a b : A}
+Definition catie_homotopic {A} `{HasEquivs A} {a b : A}
   (f : a $-> b) `{!CatIsEquiv f} {g : a $-> b} (p : f $== g)
   : CatIsEquiv g.
 Proof.
@@ -187,7 +187,7 @@ Defined.
 Global Instance compose_catie' {A} `{HasEquivs A} {a b c : A}
   (g : b $-> c) `{!CatIsEquiv g} (f : a $-> b) `{!CatIsEquiv f}
   : CatIsEquiv (g $o f)
-  := cate_homotopic _ (cate_buildequiv_fun _ $@@ cate_buildequiv_fun _).
+  := catie_homotopic _ (cate_buildequiv_fun _ $@@ cate_buildequiv_fun _).
 
 Definition compose_cate {A} `{HasEquivs A} {a b c : A}
   (g : b $<~> c) (f : a $<~> b) : a $<~> c

From c2616daee3b3dfaa3a6b6ab55f45de86b56807dc Mon Sep 17 00:00:00 2001
From: gio256 <102917377+gio256@users.noreply.github.com>
Date: Wed, 13 Mar 2024 14:22:31 -0600
Subject: [PATCH 21/25] WildCat/Yoneda.v: opyon_0gpd bifunctor instances

---
 theories/WildCat/Yoneda.v | 39 +++++++++++++++++++++++++++++++++++++--
 1 file changed, 37 insertions(+), 2 deletions(-)

diff --git a/theories/WildCat/Yoneda.v b/theories/WildCat/Yoneda.v
index 3ae8ed87644..0f9bfd51050 100644
--- a/theories/WildCat/Yoneda.v
+++ b/theories/WildCat/Yoneda.v
@@ -44,12 +44,12 @@ Proof.
 Defined.
 
 Global Instance is0bifunctor_hom {A} `{Is01Cat A}
-  : @Is0Bifunctor A^op A Type _ _ _ (@Hom A _)
+  : Is0Bifunctor (A:=A^op) (B:=A) (C:=Type) (@Hom A _)
   := is0bifunctor_functor_uncurried _.
 
 (** While it is possible to prove the bifunctor coherence condition from [Is1Cat_Strong], 1-functoriality requires morphism extensionality.*)
 Global Instance is1bifunctor_hom {A} `{Is1Cat A} `{HasMorExt A}
-  : @Is1Bifunctor A^op A Type _ _ _ _ _ _ _ _ _ _ _ _ (@Hom A _) _
+  : Is1Bifunctor (A:=A^op) (B:=A) (C:=Type) (@Hom A _)
   := is1bifunctor_functor_uncurried _.
 
 Definition fun01_hom {A} `{Is01Cat A}
@@ -229,6 +229,41 @@ Defined.
 Definition opyon_0gpd {A : Type} `{Is1Cat A} (a : A) : A -> ZeroGpd
   := fun b => Build_ZeroGpd (a $-> b) _ _ _.
 
+Global Instance is0functor_hom_0gpd {A : Type} `{Is1Cat A}
+  : Is0Functor (A:=A^op*A) (B:=ZeroGpd) (uncurry (opyon_0gpd (A:=A))).
+Proof.
+  nrapply Build_Is0Functor.
+  intros [a1 a2] [b1 b2] [f1 f2]; cbn in *.
+  snrapply Build_Morphism_0Gpd.
+  - exact (cat_postcomp _ f2 o cat_precomp _ f1).
+  - rapply (is0functor_compose _ _).
+    + apply is0functor_precomp.
+    + apply is0functor_postcomp.
+Defined.
+
+Global Instance is1functor_hom_0gpd {A : Type} `{Is1Cat A}
+  : Is1Functor (A:=A^op*A) (B:=ZeroGpd) (uncurry (opyon_0gpd (A:=A))).
+Proof.
+  nrapply Build_Is1Functor.
+  - intros [a1 a2] [b1 b2] [f1 f2] [g1 g2] [p q] h.
+    exact (h $@L p $@@ q).
+  - intros [a1 a2] h.
+    exact (cat_idl _ $@ cat_idr _).
+  - intros [a1 a2] [b1 b2] [c1 c2] [f1 f2] [g1 g2] h.
+    refine (cat_assoc _ _ _ $@ _).
+    refine (g2 $@L _).
+    refine (_ $@L (cat_assoc_opp _ _ _) $@ _).
+    exact (cat_assoc_opp _ _ _).
+Defined.
+
+Global Instance is0bifunctor_hom_0gpd {A : Type} `{Is1Cat A}
+  : Is0Bifunctor (A:=A^op) (B:=A) (C:=ZeroGpd) (opyon_0gpd (A:=A))
+  := is0bifunctor_functor_uncurried _.
+
+Global Instance is1bifunctor_hom_0gpd {A : Type} `{Is1Cat A}
+  : Is1Bifunctor (A:=A^op) (B:=A) (C:=ZeroGpd) (opyon_0gpd (A:=A))
+  := is1bifunctor_functor_uncurried _.
+
 Global Instance is0functor_opyon_0gpd {A : Type} `{Is1Cat A} (a : A)
   : Is0Functor (opyon_0gpd a).
 Proof.

From 07b6ff4f7a183dc3d29b46fb7901b60921b80e70 Mon Sep 17 00:00:00 2001
From: gio256 <102917377+gio256@users.noreply.github.com>
Date: Wed, 13 Mar 2024 14:26:59 -0600
Subject: [PATCH 22/25] contrib/SetoidRewrite.v: formatting

---
 contrib/SetoidRewrite.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/contrib/SetoidRewrite.v b/contrib/SetoidRewrite.v
index d01c68cb008..d905e50362e 100644
--- a/contrib/SetoidRewrite.v
+++ b/contrib/SetoidRewrite.v
@@ -71,7 +71,7 @@ Defined.
 
 Open Scope signatureT_scope.
 
-#[export] Instance symmetry_flip {A B: Type} {f : A -> B}
+#[export] Instance symmetry_flip {A B : Type} {f : A -> B}
   {R : Relation A} {R' : Relation B} `{Symmetric _ R}
   (H0 : CMorphisms.Proper (R ++> R') f)
   : CMorphisms.Proper (R --> R') f.
@@ -80,7 +80,7 @@ Proof.
   apply H0. unfold CRelationClasses.flip. symmetry. exact Rab.
 Defined.
 
-#[export] Instance symmetric_flip_snd {A B C: Type} {R : Relation A}
+#[export] Instance symmetric_flip_snd {A B C : Type} {R : Relation A}
   {R' : Relation B} {R'' : Relation C} `{Symmetric _ R'}
   (f : A -> B -> C) (H1 : CMorphisms.Proper (R ++> R' ++> R'') f)
   : CMorphisms.Proper (R ++> R' --> R'') f.
@@ -88,7 +88,7 @@ Proof.
   intros a b Rab x y R'yx. apply H1; [ assumption | symmetry; assumption ].
 Defined.
 
-#[export] Instance IsProper_fmap {A B: Type} `{Is1Cat A}
+#[export] Instance IsProper_fmap {A B : Type} `{Is1Cat A}
   `{Is1Cat A} (F : A -> B) `{Is1Functor _ _ F} (a b : A)
   : CMorphisms.Proper (GpdHom ==> GpdHom) (@fmap _ _ _ _ F _ a b) := fun _ _ eq => fmap2 F eq.
 
@@ -111,7 +111,7 @@ Proof.
   exact eq_g.
 Defined.
 
-#[export] Instance gpd_hom_to_hom_proper {A B: Type} `{Is0Gpd A}
+#[export] Instance gpd_hom_to_hom_proper {A B : Type} `{Is0Gpd A}
   {R : Relation B} (F : A -> B)
   `{CMorphisms.Proper _ (GpdHom ==> R) F}
   : CMorphisms.Proper (Hom ==> R) F.

From 2ed10657effbb7a983bdb74eb65606445e10c865 Mon Sep 17 00:00:00 2001
From: gio256 <102917377+gio256@users.noreply.github.com>
Date: Wed, 13 Mar 2024 17:10:54 -0600
Subject: [PATCH 23/25] WildCat/Yoneda.v: clean up is0functor_hom_0gpd

---
 theories/WildCat/Yoneda.v | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/theories/WildCat/Yoneda.v b/theories/WildCat/Yoneda.v
index 0f9bfd51050..503a81dece4 100644
--- a/theories/WildCat/Yoneda.v
+++ b/theories/WildCat/Yoneda.v
@@ -233,12 +233,9 @@ Global Instance is0functor_hom_0gpd {A : Type} `{Is1Cat A}
   : Is0Functor (A:=A^op*A) (B:=ZeroGpd) (uncurry (opyon_0gpd (A:=A))).
 Proof.
   nrapply Build_Is0Functor.
-  intros [a1 a2] [b1 b2] [f1 f2]; cbn in *.
-  snrapply Build_Morphism_0Gpd.
-  - exact (cat_postcomp _ f2 o cat_precomp _ f1).
-  - rapply (is0functor_compose _ _).
-    + apply is0functor_precomp.
-    + apply is0functor_postcomp.
+  intros [a1 a2] [b1 b2] [f1 f2]; unfold op in *; cbn in *.
+  rapply (Build_Morphism_0Gpd (opyon_0gpd a1 a2) (opyon_0gpd b1 b2)
+          (cat_postcomp b1 f2 o cat_precomp a2 f1)).
 Defined.
 
 Global Instance is1functor_hom_0gpd {A : Type} `{Is1Cat A}

From 6c975c1738a70d433c6c69e41bfb6e6e87dbb087 Mon Sep 17 00:00:00 2001
From: gio256 <102917377+gio256@users.noreply.github.com>
Date: Thu, 14 Mar 2024 10:47:32 -0600
Subject: [PATCH 24/25] WildCat/Bifunctor.v: formatting

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

diff --git a/theories/WildCat/Bifunctor.v b/theories/WildCat/Bifunctor.v
index 67017860dac..2930d1cb668 100644
--- a/theories/WildCat/Bifunctor.v
+++ b/theories/WildCat/Bifunctor.v
@@ -136,7 +136,7 @@ Defined.
 (** Restricting a functor along a bifunctor yields a bifunctor. *)
 Global Instance is0bifunctor_compose {A B C D : Type}
   `{IsGraph A, IsGraph B, Is1Cat C, Is1Cat D}
-  (F : A -> B -> C) `{bf : !Is0Bifunctor F}
+  (F : A -> B -> C) {bf : Is0Bifunctor F}
   (G : C -> D) `{!Is0Functor G, !Is1Functor G}
   : Is0Bifunctor (fun a b => G (F a b)).
 Proof.
@@ -146,7 +146,7 @@ Defined.
 Global Instance is1bifunctor_compose {A B C D : Type}
   `{Is1Cat A, Is1Cat B, Is1Cat C, Is1Cat D}
   (F : A -> B -> C) (G : C -> D) `{!Is0Functor G, !Is1Functor G}
-  `{!Is0Bifunctor F, bf : !Is1Bifunctor F}
+  `{!Is0Bifunctor F} {bf : Is1Bifunctor F}
   : Is1Bifunctor (fun a b => G (F a b)).
 Proof.
   nrapply Build_Is1Bifunctor.

From 31562d05d1d3ff9851aa7a7c8b5225906b137bd3 Mon Sep 17 00:00:00 2001
From: gio256 <102917377+gio256@users.noreply.github.com>
Date: Thu, 14 Mar 2024 10:48:07 -0600
Subject: [PATCH 25/25] WildCat/Yoneda.v: add comment

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

diff --git a/theories/WildCat/Yoneda.v b/theories/WildCat/Yoneda.v
index 503a81dece4..82b6ea503d3 100644
--- a/theories/WildCat/Yoneda.v
+++ b/theories/WildCat/Yoneda.v
@@ -63,6 +63,7 @@ Definition fun01_hom {A} `{Is01Cat A}
 Definition opyon {A : Type} `{IsGraph A} (a : A) : A -> Type
   := fun b => (a $-> b).
 
+(** We prove this explicitly instead of using the bifunctor instance above so that we can apply [fmap] in each argument independently without mapping an identity in the other. *)
 Global Instance is0functor_opyon {A : Type} `{Is01Cat A} (a : A)
   : Is0Functor (opyon a).
 Proof.