From b0266b6e767debd2399c092d5a9aae8bb9a3da48 Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Sun, 5 May 2024 16:50:09 +0100
Subject: [PATCH 01/10] redefine Bifunctor

<!-- ps-id: 9856989b-6e5b-458b-8525-b00e49d88729 -->

Signed-off-by: Ali Caglayan <alizter@gmail.com>
---
 theories/Algebra/AbSES/Ext.v       |  16 +-
 theories/Algebra/AbSES/SixTerm.v   |   3 +-
 theories/Homotopy/Join/Core.v      |   5 +-
 theories/Homotopy/Join/JoinAssoc.v |  15 +-
 theories/Homotopy/Smash.v          |   2 -
 theories/WildCat/Bifunctor.v       | 385 ++++++++++++++++-------------
 theories/WildCat/Monoidal.v        |  29 +--
 theories/WildCat/Products.v        |  81 ++----
 theories/WildCat/Yoneda.v          |   8 +-
 9 files changed, 259 insertions(+), 285 deletions(-)

diff --git a/theories/Algebra/AbSES/Ext.v b/theories/Algebra/AbSES/Ext.v
index ae54b254dd1..4c86d00c455 100644
--- a/theories/Algebra/AbSES/Ext.v
+++ b/theories/Algebra/AbSES/Ext.v
@@ -63,7 +63,7 @@ Defined.
 
 (** ** The bifunctor [ab_ext] *)
 
-Definition ab_ext `{Univalence} (B A : AbGroup@{u}) : AbGroup.
+Definition ab_ext `{Univalence} (B : AbGroup@{u}^op) (A : AbGroup@{u}) : AbGroup.
 Proof.
   snrapply (Build_AbGroup (grp_ext B A)).
   intros E F.
@@ -127,10 +127,14 @@ Defined.
 Global Instance is1bifunctor_abext `{Univalence}
   : Is1Bifunctor (A:=AbGroup^op) ab_ext.
 Proof.
-  snrapply Build_Is1Bifunctor.
+  snrapply Build_Is1Bifunctor'.
   1,2: exact _.
-  intros A B.
-  exact (bifunctor_isbifunctor (Ext : AbGroup^op -> AbGroup -> pType)).
+  intros A B f C D g.
+  intros x.
+  strip_truncations; cbn.
+  pose proof (bifunctor_coh (Ext : AbGroup^op -> AbGroup -> pType) f g (tr x)) as X.
+  cbn in X.
+  exact X.
 Defined.
 
 (** We can push out a fixed extension while letting the map vary, and this defines a group homomorphism. *)
@@ -139,10 +143,10 @@ Definition abses_pushout_ext `{Univalence}
   : GroupHomomorphism (ab_hom A G) (ab_ext B G).
 Proof.
   snrapply Build_GroupHomomorphism.
-  1: exact (fun f => fmap01 (A:=AbGroup^op) Ext' _ f (tr E)).
+  1: exact (fun f => fmap (Ext' (_ : AbGroup^op)) f (tr E)).
   intros f g; cbn.
   nrapply (ap tr).
-  exact (baer_sum_distributive_pushouts f g).
+  exact (baer_sum_distributive_pushouts (E:=E) f g).
 Defined.
 
 (** ** Extensions ending in a projective are trivial *)
diff --git a/theories/Algebra/AbSES/SixTerm.v b/theories/Algebra/AbSES/SixTerm.v
index 34a8ccb7e9d..4bbde9d4dd6 100644
--- a/theories/Algebra/AbSES/SixTerm.v
+++ b/theories/Algebra/AbSES/SixTerm.v
@@ -98,7 +98,8 @@ Proof.
       destruct g as [g k].
     exists g.
     apply path_sigma_hprop; cbn.
-    exact k^.
+    elim k^. 
+    by apply equiv_path_grouphomomorphism.
 Defined.
 
 (** *** Exactness of [ab_hom A G -> Ext1 B G -> Ext1 E G]. *)
diff --git a/theories/Homotopy/Join/Core.v b/theories/Homotopy/Join/Core.v
index 1dc3b578789..d869d2be5f6 100644
--- a/theories/Homotopy/Join/Core.v
+++ b/theories/Homotopy/Join/Core.v
@@ -562,7 +562,7 @@ Section FunctorJoin.
 
   Global Instance is0bifunctor_join : Is0Bifunctor Join.
   Proof.
-    rapply Build_Is0Bifunctor'.
+    rapply Build_Is0Functor.
     apply Build_Is0Functor.
     intros A B [f g].
     exact (functor_join f g).
@@ -570,8 +570,7 @@ Section FunctorJoin.
 
   Global Instance is1bifunctor_join : Is1Bifunctor Join.
   Proof.
-    snrapply Build_Is1Bifunctor'.
-    nrapply Build_Is1Functor.
+    snrapply Build_Is1Functor.
     - intros A B f g [p q].
       exact (functor2_join p q).
     - intros A; exact functor_join_idmap.
diff --git a/theories/Homotopy/Join/JoinAssoc.v b/theories/Homotopy/Join/JoinAssoc.v
index 70689296307..cd0630a95e0 100644
--- a/theories/Homotopy/Join/JoinAssoc.v
+++ b/theories/Homotopy/Join/JoinAssoc.v
@@ -266,20 +266,7 @@ Proof.
   - intros A B C.
     apply join_assoc.
   - intros [[A B] C] [[A' B'] C'] [[f g] h]; cbn.
-    (* This is awkward because Monoidal.v works with a tensor that is separately a functor in each variable. *)
-    intro x.
-    rhs_V nrapply functor_join_compose.
-    rhs_V nrapply functor2_join.
-    2: reflexivity.
-    2: nrapply functor_join_compose.
-    cbn.
-    rhs_V nrapply join_assoc_nat; cbn.
-    apply ap.
-    lhs_V nrapply functor_join_compose.
-    lhs_V nrapply functor_join_compose.
-    apply functor2_join.
-    1: reflexivity.
-    symmetry; nrapply functor_join_compose.
+    apply join_assoc_nat.
 Defined.
 
 (** ** The Triangle Law *)
diff --git a/theories/Homotopy/Smash.v b/theories/Homotopy/Smash.v
index 60600c0bd70..4bcb8b00d71 100644
--- a/theories/Homotopy/Smash.v
+++ b/theories/Homotopy/Smash.v
@@ -353,7 +353,6 @@ Defined.
 
 Global Instance is0bifunctor_smash : Is0Bifunctor Smash.
 Proof.
-  rapply Build_Is0Bifunctor'.
   nrapply Build_Is0Functor.
   intros [X Y] [A B] [f g].
   exact (functor_smash f g).
@@ -361,7 +360,6 @@ Defined.
 
 Global Instance is1bifunctor_smash : Is1Bifunctor Smash.
 Proof.
-  snrapply Build_Is1Bifunctor'.
   snrapply Build_Is1Functor.
   - intros [X Y] [A B] [f g] [h i] [p q].
     exact (functor_smash_homotopic p q).
diff --git a/theories/WildCat/Bifunctor.v b/theories/WildCat/Bifunctor.v
index dd6c4667ccc..156fda37071 100644
--- a/theories/WildCat/Bifunctor.v
+++ b/theories/WildCat/Bifunctor.v
@@ -1,117 +1,191 @@
 Require Import Basics.Overture Basics.Tactics.
-Require Import Types.Forall.
+Require Import Types.Forall Types.Prod.
 Require Import WildCat.Core WildCat.Prod WildCat.Equiv WildCat.NatTrans WildCat.Square.
 
 (** * Bifunctors between WildCats *)
 
 (** ** Definition *)
 
-Class Is0Bifunctor {A B C : Type} `{IsGraph A, IsGraph B, IsGraph C}
-  (F : A -> B -> C)
-  := {
-  bifunctor_is0functor01 :: forall a, Is0Functor (F a);
-  bifunctor_is0functor10 :: forall b, Is0Functor (flip F b);
-}.
+Class Is0Bifunctor {A B C : Type}
+  `{IsGraph A, IsGraph B, IsGraph C} (F : A -> B -> C)
+  := is0functor_bifunctor_uncurried :: Is0Functor (uncurry F).
+
+Global Instance is0functor01_bifunctor {A B C : Type}
+  `{Is01Cat A, IsGraph B, IsGraph C} (F : A -> B -> C) `{!Is0Bifunctor F}
+  : forall a, Is0Functor (F a).
+Proof.
+  intros a.
+  snrapply Build_Is0Functor.
+  intros b b' g.
+  change (uncurry F (a, b) $-> uncurry F (a, b')).
+  refine (fmap (uncurry F) (_, _)).
+  - exact (Id a).
+  - exact g.
+Defined.
+
+Global Instance is0functor10_bifunctor {A B C : Type}
+  `{IsGraph A, Is01Cat B, IsGraph C} (F : A -> B -> C) `{!Is0Bifunctor F}
+  : forall b, Is0Functor (flip F b).
+Proof.
+  intros b.
+  snrapply Build_Is0Functor.
+  intros a a' f.
+  change (uncurry F (a, b) $-> uncurry F (a', b)).
+  refine (fmap (uncurry F) (_, _)).
+  - exact f.
+  - exact (Id b).
+Defined.
 
-Class Is1Bifunctor {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
+Definition Build_Is0Bifunctor {A B C : Type}
+  `{IsGraph A, IsGraph B, Is01Cat C} (F : A -> B -> C)
+  `{!forall a, Is0Functor (F a), !forall b, Is0Functor (flip F b)}
+  : Is0Bifunctor F.
+Proof.
+  snrapply Build_Is0Functor.
+  intros [a b] [a' b'] [f g].
+  change (F a b $-> F a' b').
+  exact (fmap (flip F b') f $o fmap (F a) g).
+Defined.
+
+Class Is1Bifunctor {A B C : Type}
+  `{Is1Cat A, Is1Cat B, Is1Cat C} (F : A -> B -> C) `{!Is0Bifunctor F}
+  := is1functor_bifunctor_uncurried :: Is1Functor (uncurry F).
+
+Arguments Is1Bifunctor {A B C _ _ _ _ _ _ _ _ _ _ _ _} F {Is0Bifunctor} : rename.
+
+(* Class Is1Bifunctor {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
   (F : A -> B -> C) `{!Is0Bifunctor F}
   := {
   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.
-
-(** 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)).
+Global Instance is1functor01_bifunctor {A B C : Type} (F : A -> B -> C)
+  `{Is1Bifunctor A B C F}
+  : forall a, Is1Functor (F a).
 Proof.
-  rapply Build_Is0Bifunctor.
+  intros a.
+  snrapply Build_Is1Functor.
+  - intros b b' g g' p.
+    refine (fmap2 (uncurry F) (_, _)).
+    + exact (Id (Id a)).
+    + exact p.
+  - intros b.
+    exact (fmap_id (uncurry F) _).
+  - intros b b' b'' f g.
+    srefine (fmap2 (uncurry F) _ $@ _). 
+    + exact (Id a $o Id a, g $o f).
+    + exact ((cat_idl _)^$, Id _).
+    + exact (fmap_comp (uncurry F) (a := (a, b)) (b := (a, b')) (c := (a, b''))
+        (Id a, f) (Id a, g)).
 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)).
+Global Instance is1functor10_bifunctor {A B C : Type} (F : A -> B -> C)
+  `{Is1Bifunctor A B C F}
+  : forall b, Is1Functor (flip F 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)^$).
+  intros b.
+  snrapply Build_Is1Functor.
+  - intros a a' f f' p.
+    refine (fmap2 (uncurry F) (_, _)).
+    + exact p.
+    + exact (Id (Id b)).
+  - intros a.
+    exact (fmap_id (uncurry F) _).
+  - intros a a' a'' f g.
+    srefine (fmap2 (uncurry F) _ $@ _).
+    + exact (g $o f, Id b $o Id b).
+    + exact (Id _, (cat_idr _)^$).
+    + exact (fmap_comp (uncurry F) (a := (a, b)) (b := (a', b)) (c := (a'', b))
+        (f, Id b) (g, Id b)).
 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).
+Definition Build_Is1Bifunctor {A B C : Type}
+  `{Is1Cat A, Is1Cat B, Is1Cat C} (F : A -> B -> C)
+  `{!forall a, Is0Functor (F a), !forall b, Is0Functor (flip F b)}
+  `{!forall a, Is1Functor (F a), !forall b, Is1Functor (flip F b)}
+  (bifunctor_coh : forall a0 a1 (f : a0 $-> a1) b0 b1 (g : b0 $-> b1),
+    fmap (F a1) g $o fmap (flip F b0) f $== fmap (flip F b1) f $o fmap (F a0) g)
+  : Is1Bifunctor (Is0Bifunctor := Build_Is0Bifunctor F) F.
+Proof.
+  snrapply Build_Is1Functor.
+  - intros [a b] [a' b'] [f g] [f' g'] [p p']; unfold fst, snd in * |- .
+    exact (fmap2 (F a) p' $@@ fmap2 (flip F b') p).
+  - intros [a b].
+    exact ((fmap_id (F a) b $@@ fmap_id (flip F b) _) $@ cat_idr _).
+  - intros [a b] [a' b'] [a'' b''] [f g] [f' g']; unfold fst, snd in * |- . 
+    refine ((fmap_comp (F a) g g' $@@ fmap_comp (flip F b'') f f') $@ _).
+    nrefine (cat_assoc_opp _ _ _ $@ (_ $@R _) $@ cat_assoc _ _ _).
+    refine (cat_assoc _ _ _ $@ (_ $@L _^$) $@ cat_assoc_opp _ _ _).
+    nrapply bifunctor_coh.
+Defined.
 
 (** ** Bifunctor lemmas *)
 
 (** *** 1-functorial action *)
 
 (** [fmap] in the first argument. *)
-Definition fmap10 {A B C : Type} `{IsGraph A, IsGraph B, IsGraph C}
+Definition fmap10 {A B C : Type} `{IsGraph A, Is01Cat 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} `{IsGraph A, IsGraph B, IsGraph C}
+Definition fmap01 {A B C : Type} `{Is01Cat 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.
 
 (** [fmap] in both arguments. Note that we made a choice in the order in which to compose, but the bifunctor coherence condition says that both ways 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
-  := fmap01 F _ g $o fmap10 F f _.
-
-(** [fmap11] but with the other choice. *)
-Definition fmap11' {A B C : Type} `{IsGraph A, IsGraph B, Is01Cat C}
+Definition fmap11 {A B C : Type} `{IsGraph A, IsGraph B, IsGraph 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
-  := fmap10 F f _ $o fmap01 F _ g.
+  := fmap (uncurry F) (a := (a0, b0)) (b := (a1, b1)) (f, g).
 
 (** *** Coherence *)
 
-(** The bifunctor coherence condition becomes a 2-cell between the two choices for [fmap11]. *)
-Definition fmap11_coh {A B C : Type}
-  (F : A -> B -> C) `{Is1Bifunctor A B C F}
+Definition fmap11_is_fmap01_fmap10 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
+  (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
+  {a0 a1 : A} (f : a0 $-> a1) {b0 b1 : B} (g : b0 $-> b1)
+  : fmap11 F f g $== fmap01 F a1 g $o fmap10 F f b0.
+Proof.
+  refine (fmap2 (uncurry F) _^$ $@ fmap_comp (uncurry F)
+    (a := (a0, b0)) (b := (a1, b0)) (c := (a1, b1)) (f, Id b0) (Id a1, g)).
+  exact (cat_idl _, cat_idr _).
+Defined.
+
+Definition fmap11_is_fmap10_fmap01 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
+  (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
   {a0 a1 : A} (f : a0 $-> a1) {b0 b1 : B} (g : b0 $-> b1)
-  : fmap11 F f g $== fmap11' F f g.
+  : fmap11 F f g $== fmap10 F f b1 $o fmap01 F a0 g.
 Proof.
-  rapply bifunctor_isbifunctor.
+  refine (fmap2 (uncurry F) _^$ $@ fmap_comp (uncurry F)
+    (a := (a0, b0)) (b := (a0, b1)) (c := (a1, b1)) (Id a0, g) (f, Id b1)).
+  exact (cat_idr _, cat_idl _).
 Defined.
 
+Definition bifunctor_coh {A B C : Type}
+  (F : A -> B -> C) `{Is1Bifunctor A B C F}
+  {a0 a1 : A} (f : a0 $-> a1) {b0 b1 : B} (g : b0 $-> b1)
+  : fmap01 F a1 g $o fmap10 F f b0 $== fmap10 F f b1 $o fmap01 F a0 g
+  := (fmap11_is_fmap01_fmap10 _ _ _)^$ $@ fmap11_is_fmap10_fmap01 _ _ _.
+
 (** [fmap11] with right map the identity gives [fmap10]. *)
 Definition fmap10_is_fmap11 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
   (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
   {a0 a1 : A} (f : a0 $-> a1) (b : B)
   : fmap11 F f (Id b) $== fmap10 F f b
-  := (fmap_id _ _ $@R _) $@ cat_idl _.
+  := Id _.
 
 (** [fmap11] with left map the identity gives [fmap01]. *)
 Definition fmap01_is_fmap11 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
   (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
   (a : A) {b0 b1 : B} (g : b0 $-> b1)
   : fmap11 F (Id a) g $== fmap01 F a g
-  := (_ $@L fmap_id _ _) $@ cat_idr _.
+  := Id _.
 
 (** 2-functorial action *)
 
@@ -124,8 +198,11 @@ Definition fmap02 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
 Definition fmap12 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
   (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
   {a0 a1 : A} (f : a0 $-> a1) {b0 b1 : B} {g g' : b0 $-> b1} (q : g $== g')
-  : fmap11 F f g $== fmap11 F f g'
-  := fmap02 F _ q $@R _.
+  : fmap11 F f g $== fmap11 F f g'.
+Proof.
+  refine (fmap2 (uncurry F) _).
+  exact (Id _, q).
+Defined.
 
 Definition fmap20 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
   (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
@@ -136,15 +213,21 @@ Definition fmap20 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
 Definition fmap21 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
   (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
   {a0 a1 : A} {f f' : a0 $-> a1} (p : f $== f') {b0 b1 : B} (g : b0 $-> b1)
-  : fmap11 F f g $== fmap11 F f' g
-  := _ $@L fmap20 F p _.
+  : fmap11 F f g $== fmap11 F f' g.
+Proof.
+  refine (fmap2 (uncurry F) _).
+  exact (p, Id _).
+Defined.
 
 Definition fmap22 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
   (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
   {a0 a1 : A} {f f' : a0 $-> a1} (p : f $== f')
   {b0 b1 : B} {g g' : b0 $-> b1} (q : g $== g')
-  : fmap11 F f g $== fmap11 F f' g'
-  := fmap20 F p b0 $@@ fmap02 F a1 q.
+  : fmap11 F f g $== fmap11 F f' g'.
+Proof.
+  refine (fmap2 (uncurry F) _).
+  exact (p, q).
+Defined.
 
 (** *** Identity preservation *)
 
@@ -160,11 +243,8 @@ Definition fmap10_id {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
 
 Definition fmap11_id {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
   (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F} (a : A) (b : B)
-  : fmap11 F (Id a) (Id b) $== Id (F a b).
-Proof.
-  refine ((_ $@@ _) $@ cat_idr _).
-  1,2: rapply fmap_id.
-Defined.
+  : fmap11 F (Id a) (Id b) $== Id (F a b)
+  := fmap_id (uncurry F) (a, b).
 
 (** *** Composition preservation *)
 
@@ -184,13 +264,9 @@ Definition fmap11_comp {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
   (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
   {a0 a1 a2 : A} (g : a1 $-> a2) (f : a0 $-> a1)
   {b0 b1 b2 : B} (k : b1 $-> b2) (h : b0 $-> b1)
-  : fmap11 F (g $o f) (k $o h) $== fmap11 F g k $o fmap11 F f h.
-Proof.
-  refine ((fmap10_comp F _ _ _ $@@ fmap01_comp F _ _ _) $@ _).
-  refine (cat_assoc _ _ _ $@ (_ $@L _) $@ (cat_assoc _ _ _)^$).
-  refine ((cat_assoc _ _ _)^$ $@ (_ $@R _) $@ cat_assoc _ _ _).
-  rapply fmap11_coh.
-Defined.
+  : fmap11 F (g $o f) (k $o h) $== fmap11 F g k $o fmap11 F f h
+  := fmap_comp (uncurry F)
+    (a := (a0, b0)) (b := (a1, b1)) (c := (a2, b2)) (_, _) (_, _).
 
 (** *** Equivalence preservation *)
 
@@ -210,7 +286,7 @@ 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)
-  := compose_catie' _ _.
+  := iemap (uncurry F) (a := (a0, b0)) (b := (_, _)) (f, g).
 
 Definition emap10 {A B C : Type} `{HasEquivs A, Is1Cat B, HasEquivs C}
   (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
@@ -230,56 +306,43 @@ Definition emap11 {A B C : Type} `{HasEquivs A, HasEquivs B, HasEquivs C}
   : F a0 b0 $<~> F a1 b1
   := Build_CatEquiv (fmap11 F f g).
 
-(** *** Uncurrying *)
-
-(** 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 (flip F _) _ $@@ fmap_id (F _) _ $@ _).
-    apply cat_idl.
-  - intros x y z f g.
-    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 _).
-Defined.
-
 (** ** Flipping bifunctors *)
 
 Definition is0bifunctor_flip {A B C : Type}
-  (F : A -> B -> C) `{Is0Bifunctor A B C F} : Is0Bifunctor (flip F).
+  (F : A -> B -> C) `{Is01Cat A, Is01Cat B, Is01Cat C, !Is0Bifunctor F}
+  : Is0Bifunctor (flip F).
 Proof.
-  snrapply Build_Is0Bifunctor; exact _.
+  change (Is0Functor (uncurry F o equiv_prod_symm _ _)).
+  exact _.
 Defined.
 Hint Immediate is0bifunctor_flip : typeclass_instances.
 
 Definition is1bifunctor_flip {A B C : Type}
-  (F : A -> B -> C) `{Is1Bifunctor A B C F} : Is1Bifunctor (flip F).
+(F : A -> B -> C) `{H : Is1Bifunctor A B C F}
+  : Is1Bifunctor (flip F).
+Proof.
+  change (Is1Functor (uncurry F o equiv_prod_symm _ _)).
+  exact _.
+Defined.
+Hint Immediate is1bifunctor_flip : typeclass_instances.
+
+(** Here is an alternative constructor that uses [fmap01] and [fmap10] instead. *)
+Definition Build_Is1Bifunctor' {A B C : Type}
+  `{Is1Cat A, Is1Cat B, Is1Cat C} (F : A -> B -> C)
+  `{!forall a, Is0Functor (F a), !forall b, Is0Functor (flip F b)}
+  `{!forall a, Is1Functor (F a), !forall b, Is1Functor (flip F b)}
+  (Is0Bifunctor_F := Build_Is0Bifunctor F)
+  (bifunctor_coh : forall a0 a1 (f : a0 $-> a1) b0 b1 (g : b0 $-> b1),
+    fmap01 F a1 g $o fmap10 F f b0 $== fmap10 F f b1 $o fmap01 F a0 g)
+  : Is1Bifunctor F.
 Proof.
   snrapply Build_Is1Bifunctor.
   1,2: exact _.
   intros a0 a1 f b0 b1 g.
-  symmetry.
-  rapply bifunctor_isbifunctor.
+  refine ((_ $@@ _)^$ $@ bifunctor_coh a0 a1 f b0 b1 g $@ (_ $@@ _)).
+  1,4: exact ((_ $@L fmap_id (F _) _) $@ cat_idr _).
+  1,2: exact (( fmap_id (flip F _) _ $@R _) $@ cat_idl _).
 Defined.
-Hint Immediate is1bifunctor_flip : typeclass_instances.
 
 (** ** Composition of bifunctors *)
 
@@ -287,12 +350,12 @@ Hint Immediate is1bifunctor_flip : typeclass_instances.
 
 (** Restricting a functor along a bifunctor yields a bifunctor. *)
 Global Instance is0bifunctor_postcompose {A B C D : Type}
-  `{IsGraph A, IsGraph B, IsGraph C, IsGraph D}
+  `{Is01Cat A, Is01Cat B, Is01Cat C, Is01Cat D}
   (F : A -> B -> C) {bf : Is0Bifunctor F}
   (G : C -> D) `{!Is0Functor G}
   : Is0Bifunctor (fun a b => G (F a b)).
 Proof.
-  rapply Build_Is0Bifunctor.
+  rapply is0functor_compose.
 Defined.
 
 Global Instance is1bifunctor_postcompose {A B C D : Type}
@@ -301,73 +364,37 @@ Global Instance is1bifunctor_postcompose {A B C D : Type}
   `{!Is0Bifunctor F} {bf : Is1Bifunctor F}
   : Is1Bifunctor (fun a b => G (F a b)).
 Proof.
-  nrapply Build_Is1Bifunctor.
-  1,2: exact _.
-  intros a0 a1 f b0 b1 g.
-  refine ((fmap_comp G _ _)^$ $@ _ $@ fmap_comp G _ _).
-  rapply fmap2.
-  exact (bifunctor_isbifunctor F f g).
+  rapply is1functor_compose.
 Defined.
 
-Global Instance is0bifunctor_precompose {A B C D : Type}
-  `{IsGraph A, IsGraph B, IsGraph C, IsGraph D}
-  (G : A -> B) (F : B -> C -> D) `{!Is0Functor G, !Is0Bifunctor F}
-  : Is0Bifunctor (fun a b => F (G a) b).
+Global Instance is0bifunctor_precompose {A B C D E : Type}
+  `{Is01Cat A, Is01Cat B, Is01Cat C, Is01Cat D, Is01Cat E}
+  (G : A -> B) (K : E -> C) (F : B -> C -> D)
+  `{!Is0Functor G, !Is0Bifunctor F, !Is0Functor K}
+  : Is0Bifunctor (fun a b => F (G a) (K b)).
 Proof.
-  rapply Build_Is0Bifunctor.
-  intros c.
-  change (Is0Functor (flip F c o G)).
+  change (Is0Functor (uncurry F o functor_prod G K)).
   exact _.
 Defined.
 
-Global Instance is0bifunctor_precompose' {A B C D : Type}
-  `{IsGraph A, IsGraph B, IsGraph C, IsGraph D}
-  (G : A -> C) (F : B -> C -> D) `{!Is0Functor G, !Is0Bifunctor F}
-  : Is0Bifunctor (fun a b => F a (G b)).
+Global Instance is1bifunctor_precompose {A B C D E : Type}
+  `{Is1Cat A, Is1Cat B, Is1Cat C, Is1Cat D, Is1Cat E}
+  (G : A -> B) (K : E -> C) (F : B -> C -> D)
+  `{!Is0Functor G, !Is1Functor G, !Is0Bifunctor F, !Is1Bifunctor F,
+    !Is0Functor K, !Is1Functor K}
+  : Is1Bifunctor (fun a b => F (G a) (K b)).
 Proof.
-  rapply Build_Is0Bifunctor.
-  intros a.
-  change (Is0Functor (flip F (G a))).
+  change (Is1Functor (uncurry F o functor_prod G K)).
   exact _.
 Defined.
 
-Global Instance is1bifunctor_precompose {A B C D : Type}
-  `{Is1Cat A, Is1Cat B, Is1Cat C, Is1Cat D}
-  (G : A -> B) (F : B -> C -> D)
-  `{!Is0Functor G, !Is1Functor G, !Is0Bifunctor F, !Is1Bifunctor F}
-  : Is1Bifunctor (fun a b => F (G a) b).
-Proof.
-  nrapply Build_Is1Bifunctor.
-  - exact _.
-  - unfold flip.
-    change (forall c, Is1Functor (flip F c o G)).
-    exact _.
-  - intros ? ? ?; apply (bifunctor_isbifunctor F).
-Defined.
-
-Global Instance is1bifunctor_precompose' {A B C D : Type}
-  `{Is1Cat A, Is1Cat B, Is1Cat C, Is1Cat D}
-  (G : A -> C) (F : B -> C -> D)
-  `{!Is0Functor G, !Is1Functor G, !Is0Bifunctor F, !Is1Bifunctor F}
-  : Is1Bifunctor (fun b a => F b (G a)).
-Proof.
-  nrapply Build_Is1Bifunctor.
-  - exact _.
-  - unfold flip.
-    change (forall a, Is1Functor (fun b => F b (G a))).
-    exact _.
-  - intros a a' f b b' g.
-    simpl.
-    apply (bifunctor_isbifunctor F).
-Defined.
-
 Global Instance is0functor_uncurry_uncurry_left {A B C D E}
   (F : A -> B -> C) (G : C -> D -> E)
   `{Is01Cat A, Is01Cat B, Is01Cat C, Is01Cat D, Is01Cat E,
     !Is0Bifunctor F, !Is0Bifunctor G}
   : Is0Functor (uncurry (uncurry (fun x y z => G (F x y) z))).
 Proof.
-  rapply is0functor_uncurry_bifunctor.
+  exact _.
 Defined.
 
 Global Instance is0functor_uncurry_uncurry_right {A B C D E}
@@ -376,20 +403,26 @@ Global Instance is0functor_uncurry_uncurry_right {A B C D E}
     !Is0Bifunctor F, !Is0Bifunctor G}
   : Is0Functor (uncurry (uncurry (fun x y z => G x (F y z)))).
 Proof.
-  apply is0functor_uncurry_bifunctor.
-  nrapply Build_Is0Bifunctor.
-  1: exact _.
-  intros b.
-  change (Is0Functor (uncurry (fun x y => G x (F y b)))).
-  apply is0functor_uncurry_bifunctor.
-  apply (is0bifunctor_precompose' (flip F b) G).
+  snrapply Build_Is0Functor.
+  intros cab cab' [[h f] g].
+  exact (fmap11 G h (fmap11 F f g)).
 Defined.
 
+Definition fmap11_square {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
+  (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
+  {a00 a20 a02 a22 : A} {f10 : a00 $-> a20} {f12 : a02 $-> a22}
+  {f01 : a00 $-> a02} {f21 : a20 $-> a22}
+  {b00 b20 b02 b22 : B} {g10 : b00 $-> b20} {g12 : b02 $-> b22}
+  {g01 : b00 $-> b02} {g21 : b20 $-> b22}
+  (p : Square f01 f21 f10 f12) (q : Square g01 g21 g10 g12)
+  : Square (fmap11 F f01 g01) (fmap11 F f21 g21) (fmap11 F f10 g10) (fmap11 F f12 g12)
+  := (fmap11_comp F _ _ _ _)^$ $@ fmap22 F p q $@ fmap11_comp F _ _ _ _.
+
 (** ** Natural transformations between bifunctors *)
 
 (** We can show that an uncurried natural transformation between uncurried bifunctors by composing the naturality square in each variable. *)
-Global Instance is1natural_uncurry {A B C : Type}
-  `{IsGraph A, IsGraph B, Is1Cat C}
+(* Global Instance is1natural_uncurry {A B C : Type}
+  `{Is01Cat A, Is01Cat B, Is1Cat C}
   (F : A -> B -> C)
   `{!Is0Bifunctor F}
   (G : A -> B -> C)
@@ -402,5 +435,5 @@ Proof.
   intros [a b] [a' b'] [f f']; cbn in *.
   change (?w $o ?x $== ?y $o ?z) with (Square z w x y).
   unfold fmap11.
-  exact (hconcat (nat_l _ _ _ f) (nat_r _ _ _ f')).
-Defined.
+  epose (hconcat (nat_l _ _ _ f) (nat_r _ _ _ f')).
+Defined. *)
diff --git a/theories/WildCat/Monoidal.v b/theories/WildCat/Monoidal.v
index 2ead4600768..0b03c631fd1 100644
--- a/theories/WildCat/Monoidal.v
+++ b/theories/WildCat/Monoidal.v
@@ -157,9 +157,8 @@ Section Associator.
     : associator x' y' z' $o fmap11 F f (fmap11 F g h)
       $== fmap11 F (fmap11 F f g) h $o associator x y z.
   Proof.
-    nrefine (_ $@ is1natural_associator_uncurried (x, y, z) (x', y', z') (f, g, h)).
-    refine (_ $@L ((_ $@R _) $@ cat_assoc _ _ _ $@ (_ $@L _^$))).
-    1,2: rapply fmap_comp. 
+    destruct assoc as [asso nat].
+    exact (nat (x, y, z) (x', y', z') (f, g, h)).
   Defined.
 
   Local Definition associator_nat_l {x x' : A} (f : x $-> x') (y z : A)
@@ -359,28 +358,20 @@ Section SymmetricBraid.
   Local Definition braid_nat {a b c d} (f : a $-> c) (g : b $-> d)
     : braid c d $o fmap11 F f g $== fmap11 F g f $o braid a b.
   Proof.
-    refine (is1natural_braiding_uncurried (a, b) (c, d) (f, g) $@ _).
-    refine (_ $@R _).
-    rapply fmap11_coh.
+    exact (is1natural_braiding_uncurried (a, b) (c, d) (f, g)).
   Defined.
 
   Local Definition braid_nat_l {a b c} (f : a $-> b)
     : braid b c $o fmap10 F f c $== fmap01 F c f $o braid a c.
   Proof.
-    refine ((_ $@L _^$) $@ _ $@ (_ $@R _)).
-    - rapply fmap10_is_fmap11.
-    - exact (is1natural_braiding_uncurried (a, c) (b, c) (f, Id _)).
-    - exact ((fmap11_coh _ _ _)^$ $@ fmap01_is_fmap11 _ c f).
+    exact (is1natural_braiding_uncurried (a, c) (b, c) (f, Id _)).
   Defined.
 
   (** This is just the inverse of above. *)
   Local Definition braid_nat_r {a b c} (g : b $-> c)
     : braid a c $o fmap01 F a g $== fmap10 F g a $o braid a b.
   Proof.
-    refine ((_ $@L _^$) $@ _ $@ (_ $@R _)).
-    - rapply fmap01_is_fmap11.
-    - exact (is1natural_braiding_uncurried (a, b) (a, c) (Id _ , g)).
-    - exact ((fmap11_coh _ _ _)^$ $@ fmap10_is_fmap11 _ g a).
+    exact (is1natural_braiding_uncurried (a, b) (a, c) (Id _ , g)).
   Defined.
 
 End SymmetricBraid.
@@ -632,15 +623,9 @@ Section TwistConstruction.
       (** The second square is just the naturality of twist. *)
       nrapply vconcat.
       2: apply twist_nat.
-      (** We rewrite one of the edges to make sure a functor application is grouped together. *)
-      nrapply vconcatL.
-      { refine ((cat_assoc _ _ _)^$ $@ (_^$ $@R _)).
-        rapply fmap_comp. }
-      (** This allows us to compose with bifunctor coherence on one side. *)
-      nrapply hconcat.
-      1: rapply fmap11_coh.
       (** Leaving us with a square with a functor application. *)
-      rapply fmap_square.
+      rapply fmap11_square.
+      1: rapply vrefl.
       (** We are finally left with the naturality of braid. *)
       apply braid_nat.
   Defined.
diff --git a/theories/WildCat/Products.v b/theories/WildCat/Products.v
index c051c5128c1..461575b2b4a 100644
--- a/theories/WildCat/Products.v
+++ b/theories/WildCat/Products.v
@@ -440,44 +440,21 @@ Defined.
 Local Instance is0bifunctor_boolrec {A : Type} `{Is1Cat A}
   : Is0Bifunctor (Bool_rec A).
 Proof.
-  snrapply Build_Is0Bifunctor.
-  - intros x.
-    nrapply Build_Is0Functor.
-    intros a b f [|].
-    + reflexivity.
-    + exact f.
-  - intros y.
-    nrapply Build_Is0Functor.
-    intros a b f [|].
-    + exact f.
-    + reflexivity.
+  snrapply Build_Is0Functor.
+  intros [a b] [a' b'] [f g] [ | ].
+  - exact f.
+  - exact g.
 Defined.
 
 Local Instance is1bifunctor_boolrec {A : Type} `{Is1Cat A}
   : Is1Bifunctor (Bool_rec A).
 Proof.
-  nrapply Build_Is1Bifunctor.
-  - intros x.
-    nrapply Build_Is1Functor.
-    + intros a b f g p [|].
-      1: reflexivity.
-      exact p.
-    + intros a [|]; reflexivity.
-    + intros a b c f g [|].
-      1: exact (cat_idl _)^$.
-      reflexivity.
-  - intros y.
-    nrapply Build_Is1Functor.
-    + intros a b f g p [|].
-      1: exact p.
-      reflexivity.
-    + intros a [|]; reflexivity.
-    + 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 _)^$).
+  snrapply Build_Is1Functor.
+  - intros [a b] [a' b'] [f g] [f' g'] [p q] [ | ].
+    + exact p.
+    + exact q.
+  - intros [a b] [ | ]; reflexivity.
+  - intros [a b] [a' b'] [a'' b''] [f f'] [g g'] [ | ]; reflexivity.
 Defined.
 
 (** As a special case of the product functor, restriction along [Bool_rec A] yields bifunctoriality of [cat_binprod]. *)
@@ -502,28 +479,28 @@ Global Instance is0functor_cat_binprod_l {A : Type} `{HasBinaryProducts A}
   (y : A)
   : Is0Functor (fun x => cat_binprod x y).
 Proof.
-  exact (bifunctor_is0functor10 y).
+  exact (is0functor10_bifunctor _ y).
 Defined.
 
 Global Instance is1functor_cat_binprod_l {A : Type} `{HasBinaryProducts A}
   (y : A)
   : Is1Functor (fun x => cat_binprod x y).
 Proof.
-  exact (bifunctor_is1functor10 y).
+  exact (is1functor10_bifunctor _ y).
 Defined.
 
 Global Instance is0functor_cat_binprod_r {A : Type} `{HasBinaryProducts A}
   (x : A)
   : Is0Functor (fun y => cat_binprod x y).
 Proof.
-  exact (bifunctor_is0functor01 x).
+  exact (is0functor01_bifunctor _ x).
 Defined.
 
 Global Instance is1functor_cat_binprod_r {A : Type} `{HasBinaryProducts A}
   (x : A)
   : Is1Functor (fun y => cat_binprod x y).
 Proof.
-  exact (bifunctor_is1functor01 x).
+  exact (is1functor01_bifunctor _ x).
 Defined.
 
 (** [cat_binprod_corec] is also functorial in each morphsism. *)
@@ -558,12 +535,8 @@ Definition cat_pr1_fmap10_binprod {A : Type} `{HasBinaryProducts A}
 
 Definition cat_pr1_fmap11_binprod {A : Type} `{HasBinaryProducts A}
   {w x y z : A} (f : w $-> y) (g : x $-> z)
-  : cat_pr1 $o fmap11 (fun x y => cat_binprod x y) f g $== f $o cat_pr1.
-Proof.
-  refine ((cat_assoc _ _ _)^$ $@ (_ $@R _) $@ cat_assoc _ _ _ $@ _).
-  1: nrapply cat_binprod_beta_pr1.
-  exact (cat_idl _ $@ cat_binprod_beta_pr1 _ _).
-Defined.
+  : cat_pr1 $o fmap11 (fun x y => cat_binprod x y) f g $== f $o cat_pr1
+  := cat_binprod_beta_pr1 _ _.
 
 Definition cat_pr2_fmap01_binprod {A : Type} `{HasBinaryProducts A}
   (a : A) {x y : A} (g : x $-> y)
@@ -577,12 +550,8 @@ Definition cat_pr2_fmap10_binprod {A : Type} `{HasBinaryProducts A}
 
 Definition cat_pr2_fmap11_binprod {A : Type} `{HasBinaryProducts A}
   {w x y z : A} (f : w $-> y) (g : x $-> z)
-  : cat_pr2 $o fmap11 (fun x y => cat_binprod x y) f g $== g $o cat_pr2.
-Proof.
-  refine ((cat_assoc _ _ _)^$ $@ (_ $@R _) $@ cat_assoc _ _ _ $@ (_ $@L _)).
-  1: nrapply cat_binprod_beta_pr2.
-  nrapply cat_pr2_fmap10_binprod.
-Defined.
+  : cat_pr2 $o fmap11 (fun x y => cat_binprod x y) f g $== g $o cat_pr2
+  := cat_binprod_beta_pr2 _ _.
 
 (** *** Symmetry of binary products *)
 
@@ -644,8 +613,7 @@ Section Symmetry.
     - snrapply Build_Braiding.
       + exact cat_binprod_swap.
       + intros [a b] [c d] [f g]; cbn in f, g.
-        nrefine (cat_binprod_swap_nat f g $@ (_ $@R _)).
-        rapply fmap11_coh.
+        exact(cat_binprod_swap_nat f g).
     - exact cat_binprod_swap_cat_binprod_swap.
   Defined.
 
@@ -732,12 +700,11 @@ Section Associativity.
       2: nrapply cat_pr2_fmap11_binprod.
       refine (_ $@ (_ $@L _^$) $@ (cat_assoc _ _ _)^$).
       2: nrapply cat_binprod_beta_pr2.
-      nrefine (_ $@ cat_assoc_opp _ _ _).
-      nrefine (_ $@ (_ $@L _)).
-      2: rapply fmap11_coh.
-      nrefine (cat_assoc_opp _ _ _ $@ (_ $@R _) $@ cat_assoc _ _ _).
-      refine ((fmap01_comp _ _ _ _)^$ $@ fmap02 _ _ _ $@ fmap01_comp _ _ _ _).
-      nrapply cat_pr2_fmap11_binprod.
+      refine (_^$ $@ _ $@ _).
+      1,3: rapply fmap11_comp.
+      rapply fmap22.
+      1: exact (cat_idl _ $@ (cat_idr _)^$).
+      nrapply cat_binprod_beta_pr2.
   Defined.
 
   Local Existing Instance symmetricbraiding_binprod.
diff --git a/theories/WildCat/Yoneda.v b/theories/WildCat/Yoneda.v
index 82b6ea503d3..f66af222d70 100644
--- a/theories/WildCat/Yoneda.v
+++ b/theories/WildCat/Yoneda.v
@@ -45,12 +45,12 @@ Defined.
 
 Global Instance is0bifunctor_hom {A} `{Is01Cat A}
   : Is0Bifunctor (A:=A^op) (B:=A) (C:=Type) (@Hom A _)
-  := is0bifunctor_functor_uncurried _.
+  := is0functor_hom.
 
 (** 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:=A^op) (B:=A) (C:=Type) (@Hom A _)
-  := is1bifunctor_functor_uncurried _.
+  := is1functor_hom.
 
 Definition fun01_hom {A} `{Is01Cat A}
   : Fun01 (A^op * A) Type
@@ -256,11 +256,11 @@ 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 _.
+  := is0functor_hom_0gpd.
 
 Global Instance is1bifunctor_hom_0gpd {A : Type} `{Is1Cat A}
   : Is1Bifunctor (A:=A^op) (B:=A) (C:=ZeroGpd) (opyon_0gpd (A:=A))
-  := is1bifunctor_functor_uncurried _.
+  := is1functor_hom_0gpd.
 
 Global Instance is0functor_opyon_0gpd {A : Type} `{Is1Cat A} (a : A)
   : Is0Functor (opyon_0gpd a).

From 10940caa88c2c40424d23c441ac536056e1468e1 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Sun, 5 May 2024 13:57:24 -0400
Subject: [PATCH 02/10] AbSES/Ext: adjust universe variables to make it build

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

diff --git a/theories/Algebra/AbSES/Ext.v b/theories/Algebra/AbSES/Ext.v
index 4c86d00c455..6d67b9a265d 100644
--- a/theories/Algebra/AbSES/Ext.v
+++ b/theories/Algebra/AbSES/Ext.v
@@ -63,9 +63,9 @@ Defined.
 
 (** ** The bifunctor [ab_ext] *)
 
-Definition ab_ext `{Univalence} (B : AbGroup@{u}^op) (A : AbGroup@{u}) : AbGroup.
+Definition ab_ext@{u v|u < v} `{Univalence} (B : AbGroup@{u}^op) (A : AbGroup@{u}) : AbGroup@{v}.
 Proof.
-  snrapply (Build_AbGroup (grp_ext B A)).
+  snrapply (Build_AbGroup (grp_ext@{u v} B A)).
   intros E F.
   strip_truncations; cbn.
   apply ap.

From fddabf67b88527bd3376985c9b5896ff5bc17f9b Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Mon, 6 May 2024 02:07:51 +0100
Subject: [PATCH 03/10] review comments, more simplification, cleanup commented
 out proofs

Signed-off-by: Ali Caglayan <alizter@gmail.com>
---
 theories/Homotopy/Join/Core.v |  1 -
 theories/WildCat/Bifunctor.v  | 48 ++++++++++-------------------------
 theories/WildCat/Monoidal.v   | 41 ++++++++----------------------
 3 files changed, 24 insertions(+), 66 deletions(-)

diff --git a/theories/Homotopy/Join/Core.v b/theories/Homotopy/Join/Core.v
index d869d2be5f6..dc1a34c1465 100644
--- a/theories/Homotopy/Join/Core.v
+++ b/theories/Homotopy/Join/Core.v
@@ -562,7 +562,6 @@ Section FunctorJoin.
 
   Global Instance is0bifunctor_join : Is0Bifunctor Join.
   Proof.
-    rapply Build_Is0Functor.
     apply Build_Is0Functor.
     intros A B [f g].
     exact (functor_join f g).
diff --git a/theories/WildCat/Bifunctor.v b/theories/WildCat/Bifunctor.v
index 156fda37071..ea198198014 100644
--- a/theories/WildCat/Bifunctor.v
+++ b/theories/WildCat/Bifunctor.v
@@ -53,15 +53,6 @@ Class Is1Bifunctor {A B C : Type}
 
 Arguments Is1Bifunctor {A B C _ _ _ _ _ _ _ _ _ _ _ _} F {Is0Bifunctor} : rename.
 
-(* Class Is1Bifunctor {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
-  (F : A -> B -> C) `{!Is0Bifunctor F}
-  := {
-  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
-}. *)
-
 Global Instance is1functor01_bifunctor {A B C : Type} (F : A -> B -> C)
   `{Is1Bifunctor A B C F}
   : forall a, Is1Functor (F a).
@@ -173,20 +164,6 @@ Definition bifunctor_coh {A B C : Type}
   : fmap01 F a1 g $o fmap10 F f b0 $== fmap10 F f b1 $o fmap01 F a0 g
   := (fmap11_is_fmap01_fmap10 _ _ _)^$ $@ fmap11_is_fmap10_fmap01 _ _ _.
 
-(** [fmap11] with right map the identity gives [fmap10]. *)
-Definition fmap10_is_fmap11 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
-  (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
-  {a0 a1 : A} (f : a0 $-> a1) (b : B)
-  : fmap11 F f (Id b) $== fmap10 F f b
-  := Id _.
-
-(** [fmap11] with left map the identity gives [fmap01]. *)
-Definition fmap01_is_fmap11 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
-  (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
-  (a : A) {b0 b1 : B} (g : b0 $-> b1)
-  : fmap11 F (Id a) g $== fmap01 F a g
-  := Id _.
-
 (** 2-functorial action *)
 
 Definition fmap02 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
@@ -350,7 +327,7 @@ Defined.
 
 (** Restricting a functor along a bifunctor yields a bifunctor. *)
 Global Instance is0bifunctor_postcompose {A B C D : Type}
-  `{Is01Cat A, Is01Cat B, Is01Cat C, Is01Cat D}
+  `{IsGraph A, IsGraph B, IsGraph C, IsGraph D}
   (F : A -> B -> C) {bf : Is0Bifunctor F}
   (G : C -> D) `{!Is0Functor G}
   : Is0Bifunctor (fun a b => G (F a b)).
@@ -368,7 +345,7 @@ Proof.
 Defined.
 
 Global Instance is0bifunctor_precompose {A B C D E : Type}
-  `{Is01Cat A, Is01Cat B, Is01Cat C, Is01Cat D, Is01Cat E}
+  `{IsGraph A, IsGraph B, IsGraph C, IsGraph D, IsGraph E}
   (G : A -> B) (K : E -> C) (F : B -> C -> D)
   `{!Is0Functor G, !Is0Bifunctor F, !Is0Functor K}
   : Is0Bifunctor (fun a b => F (G a) (K b)).
@@ -390,7 +367,7 @@ Defined.
 
 Global Instance is0functor_uncurry_uncurry_left {A B C D E}
   (F : A -> B -> C) (G : C -> D -> E)
-  `{Is01Cat A, Is01Cat B, Is01Cat C, Is01Cat D, Is01Cat E,
+  `{IsGraph A, IsGraph B, IsGraph C, IsGraph D, IsGraph E,
     !Is0Bifunctor F, !Is0Bifunctor G}
   : Is0Functor (uncurry (uncurry (fun x y z => G (F x y) z))).
 Proof.
@@ -399,7 +376,7 @@ Defined.
 
 Global Instance is0functor_uncurry_uncurry_right {A B C D E}
   (F : A -> B -> D) (G : C -> D -> E)
-  `{Is01Cat A, Is01Cat B, Is01Cat C, Is01Cat D, Is01Cat E,
+  `{IsGraph A, IsGraph B, IsGraph C, IsGraph D, IsGraph E,
     !Is0Bifunctor F, !Is0Bifunctor G}
   : Is0Functor (uncurry (uncurry (fun x y z => G x (F y z)))).
 Proof.
@@ -421,12 +398,12 @@ Definition fmap11_square {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
 (** ** Natural transformations between bifunctors *)
 
 (** We can show that an uncurried natural transformation between uncurried bifunctors by composing the naturality square in each variable. *)
-(* Global Instance is1natural_uncurry {A B C : Type}
-  `{Is01Cat A, Is01Cat B, Is1Cat C}
+Global Instance is1natural_uncurry {A B C : Type}
+  `{Is1Cat A, Is1Cat B, Is1Cat C}
   (F : A -> B -> C)
-  `{!Is0Bifunctor F}
+  `{!Is0Bifunctor F, !Is1Bifunctor F}
   (G : A -> B -> C)
-  `{!Is0Bifunctor G}
+  `{!Is0Bifunctor G, !Is1Bifunctor G}
   (alpha : uncurry F $=> uncurry G)
   (nat_l : forall b, Is1Natural (flip F b) (flip G b) (fun x : A => alpha (x, b)))
   (nat_r : forall a, Is1Natural (F a) (G a) (fun y : B => alpha (a, y)))
@@ -434,6 +411,9 @@ Definition fmap11_square {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
 Proof.
   intros [a b] [a' b'] [f f']; cbn in *.
   change (?w $o ?x $== ?y $o ?z) with (Square z w x y).
-  unfold fmap11.
-  epose (hconcat (nat_l _ _ _ f) (nat_r _ _ _ f')).
-Defined. *)
+  nrapply vconcatL.
+  1: rapply (fmap11_is_fmap01_fmap10 F).
+  nrapply vconcatR.
+  2: rapply (fmap11_is_fmap01_fmap10 G).
+  exact (hconcat (nat_l _ _ _ f) (nat_r _ _ _ f')).
+Defined.
diff --git a/theories/WildCat/Monoidal.v b/theories/WildCat/Monoidal.v
index 0b03c631fd1..2ab1f483d77 100644
--- a/theories/WildCat/Monoidal.v
+++ b/theories/WildCat/Monoidal.v
@@ -165,30 +165,23 @@ Section Associator.
     : associator x' y z $o fmap10 F f (F y z)
       $== fmap10 F (fmap10 F f y) z $o associator x y z.
   Proof.
-    refine ((_ $@L _^$) $@ _ $@ (_ $@R _)).
-    2: rapply (associator_nat f (Id _) (Id _)).
-    - exact (fmap12 _ _ (fmap11_id _ _ _) $@ fmap10_is_fmap11 _ _ _).
-    - exact (fmap21 _ (fmap10_is_fmap11 _ _ _) _ $@ fmap10_is_fmap11 _ _ _).
+    refine ((_ $@L _^$) $@ associator_nat f (Id _) (Id _)).
+    exact (fmap12 _ _ (fmap11_id _ _ _)).
   Defined.
 
   Local Definition associator_nat_m (x : A) {y y' : A} (g : y $-> y') (z : A)
     : associator x y' z $o fmap01 F x (fmap10 F g z)
       $== fmap10 F (fmap01 F x g) z $o associator x y z.
   Proof.
-    refine ((_ $@L _^$) $@ _ $@ (_ $@R _)).
-    2: nrapply (associator_nat (Id _) g (Id _)).
-    - exact (fmap12 _ _ (fmap10_is_fmap11 _ _ _) $@ fmap01_is_fmap11 _ _ _).
-    - exact (fmap21 _ (fmap01_is_fmap11 _ _ _) _ $@ fmap10_is_fmap11 _ _ _).
+    exact (associator_nat (Id _) g (Id _)).
   Defined.
 
   Local Definition associator_nat_r (x y : A) {z z' : A} (h : z $-> z')
     : associator x y z' $o fmap01 F x (fmap01 F y h)
       $== fmap01 F (F x y) h $o associator x y z.
   Proof.
-    refine ((_ $@L _^$) $@ _ $@ (_ $@R _)).
-    2: nrapply (associator_nat (Id _) (Id _) h).
-    - exact (fmap12 _ _ (fmap01_is_fmap11 _ _ _) $@ fmap01_is_fmap11 _ _ _).
-    - exact (fmap21 _ (fmap11_id _ _ _) _ $@ fmap01_is_fmap11 F _ _).
+    nrefine (associator_nat (Id _) (Id _) h $@ (_ $@R _)).
+    exact (fmap21 _ (fmap11_id _ _ _) _ ).
   Defined.
 
 End Associator.
@@ -456,33 +449,23 @@ Section TwistConstruction.
     : twist a' b c $o fmap10 cat_tensor f (cat_tensor b c)
       $== fmap01 cat_tensor b (fmap10 cat_tensor f c) $o twist a b c.
   Proof.
-    refine ((_ $@L _^$) $@ twist_nat a a' b b c c f (Id _) (Id _) $@ (_ $@R _)).
-    - refine (fmap12 _ _ _ $@ fmap10_is_fmap11 _ _ _).
-      rapply fmap11_id.
-    - refine (fmap12 _ _ _ $@ fmap01_is_fmap11 _ _ _).
-      rapply fmap10_is_fmap11.
+    refine ((_ $@L _^$) $@ twist_nat a a' b b c c f (Id _) (Id _)).
+    exact (fmap12 _ _ (fmap11_id _ _ _)).
   Defined.
 
   Local Definition twist_nat_m a {b b'} (g : b $-> b') c
     : twist a b' c $o fmap01 cat_tensor a (fmap10 cat_tensor g c)
       $== fmap10 cat_tensor g (cat_tensor a c) $o twist a b c.
   Proof.
-    refine ((_ $@L _^$) $@ twist_nat a a b b' c c (Id _) g (Id _) $@ (_ $@R _)).
-    - refine (fmap12 _ _ _ $@ fmap01_is_fmap11 _ _ _).
-      rapply fmap10_is_fmap11.
-    - refine (fmap12 _ _ _ $@ fmap10_is_fmap11 _ _ _).
-      rapply fmap11_id.
+    nrefine (twist_nat a a b b' c c (Id _) g (Id _) $@ (_ $@R _)).
+    exact (fmap12 _ _ (fmap11_id _ _ _)).
   Defined.
 
   Local Definition twist_nat_r a b {c c'} (h : c $-> c')
     : twist a b c' $o fmap01 cat_tensor a (fmap01 cat_tensor b h)
       $== fmap01 cat_tensor b (fmap01 cat_tensor a h) $o twist a b c.
   Proof.
-    refine ((_ $@L _^$) $@ twist_nat a a b b c c' (Id _) (Id _) h $@ (_ $@R _)).
-    - refine (fmap12 _ _ _ $@ fmap01_is_fmap11 _ _ _).
-      rapply fmap01_is_fmap11.
-    - refine (fmap12 _ _ _ $@ fmap01_is_fmap11 _ _ _).
-      rapply fmap01_is_fmap11.
+    exact (twist_nat a a b b c c' (Id _) (Id _) h).
   Defined.
 
   (** *** Movement lemmas *)
@@ -645,10 +628,6 @@ Section TwistConstruction.
         change (?w $o ?x $== ?y $o ?z) with (Square z w x y).
         nrapply vconcat.
         2: rapply (isnat right_unitor f).
-        nrapply vconcatL.
-        1: symmetry; rapply fmap01_is_fmap11.
-        nrapply vconcatR.
-        2: symmetry; rapply fmap10_is_fmap11.
         rapply braid_nat.
     - intros a.
       rapply compose_catie'.

From 988faaa0bc6e6a671fa3d9a5bba6a18b71059165 Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Mon, 6 May 2024 20:45:11 +0100
Subject: [PATCH 04/10] best-of-both-worlds bifunctor definition

Signed-off-by: Ali Caglayan <alizter@gmail.com>
---
 theories/Algebra/AbGroups/AbHom.v |   4 +-
 theories/Algebra/AbSES/BaerSum.v  |   8 +-
 theories/Algebra/AbSES/Ext.v      |   4 +-
 theories/Homotopy/Join/Core.v     |   3 +
 theories/Homotopy/Smash.v         |   3 +
 theories/WildCat/Bifunctor.v      | 331 ++++++++++++++++++++----------
 theories/WildCat/Monoidal.v       |  44 +++-
 theories/WildCat/Products.v       |  11 +-
 theories/WildCat/Yoneda.v         |  30 ++-
 9 files changed, 294 insertions(+), 144 deletions(-)

diff --git a/theories/Algebra/AbGroups/AbHom.v b/theories/Algebra/AbGroups/AbHom.v
index 90880e2d074..3edd6877a43 100644
--- a/theories/Algebra/AbGroups/AbHom.v
+++ b/theories/Algebra/AbGroups/AbHom.v
@@ -92,13 +92,13 @@ Defined.
 Global Instance is0bifunctor_ab_hom `{Funext}
   : Is0Bifunctor (ab_hom : Group^op -> AbGroup -> AbGroup).
 Proof.
-  rapply Build_Is0Bifunctor.
+  rapply Build_Is0Bifunctor''.
 Defined.
 
 Global Instance is1bifunctor_ab_hom `{Funext}
   : Is1Bifunctor (ab_hom : Group^op -> AbGroup -> AbGroup).
 Proof.
-  nrapply Build_Is1Bifunctor.
+  nrapply Build_Is1Bifunctor''.
   1,2: exact _.
   intros A A' f B B' g phi; cbn.
   by apply equiv_path_grouphomomorphism.
diff --git a/theories/Algebra/AbSES/BaerSum.v b/theories/Algebra/AbSES/BaerSum.v
index b77b057b127..e804c762aca 100644
--- a/theories/Algebra/AbSES/BaerSum.v
+++ b/theories/Algebra/AbSES/BaerSum.v
@@ -54,13 +54,13 @@ Defined.
 Global Instance is0bifunctor_abses' `{Univalence}
   : Is0Bifunctor (AbSES' : AbGroup^op -> AbGroup -> Type).
 Proof.
-  rapply Build_Is0Bifunctor.
+  rapply Build_Is0Bifunctor''.
 Defined.
 
 Global Instance is1bifunctor_abses' `{Univalence}
   : Is1Bifunctor (AbSES' : AbGroup^op -> AbGroup -> Type).
 Proof.
-  snrapply Build_Is1Bifunctor.
+  snrapply Build_Is1Bifunctor''.
   1,2: exact _.
   intros ? ? g ? ? f E; cbn.
   exact (abses_pushout_pullback_reorder E f g).
@@ -232,13 +232,13 @@ Defined.
 Global Instance is0bifunctor_abses `{Univalence}
   : Is0Bifunctor (AbSES : AbGroup^op -> AbGroup -> pType).
 Proof.
-  rapply Build_Is0Bifunctor.
+  rapply Build_Is0Bifunctor''.
 Defined.
 
 Global Instance is1bifunctor_abses `{Univalence}
   : Is1Bifunctor (AbSES : AbGroup^op -> AbGroup -> pType).
 Proof.
-  snrapply Build_Is1Bifunctor.
+  snrapply Build_Is1Bifunctor''.
   1,2: exact _.
   intros ? ? f ? ? g.
   rapply hspace_phomotopy_from_homotopy.
diff --git a/theories/Algebra/AbSES/Ext.v b/theories/Algebra/AbSES/Ext.v
index 6d67b9a265d..03030e91923 100644
--- a/theories/Algebra/AbSES/Ext.v
+++ b/theories/Algebra/AbSES/Ext.v
@@ -121,13 +121,13 @@ Defined.
 Global Instance is0bifunctor_abext `{Univalence}
   : Is0Bifunctor (A:=AbGroup^op) ab_ext.
 Proof.
-  rapply Build_Is0Bifunctor.
+  rapply Build_Is0Bifunctor''.
 Defined.
 
 Global Instance is1bifunctor_abext `{Univalence}
   : Is1Bifunctor (A:=AbGroup^op) ab_ext.
 Proof.
-  snrapply Build_Is1Bifunctor'.
+  snrapply Build_Is1Bifunctor''.
   1,2: exact _.
   intros A B f C D g.
   intros x.
diff --git a/theories/Homotopy/Join/Core.v b/theories/Homotopy/Join/Core.v
index dc1a34c1465..2fa52e4b4a8 100644
--- a/theories/Homotopy/Join/Core.v
+++ b/theories/Homotopy/Join/Core.v
@@ -562,6 +562,8 @@ Section FunctorJoin.
 
   Global Instance is0bifunctor_join : Is0Bifunctor Join.
   Proof.
+    snrapply Build_Is0Bifunctor'.
+    1,2: exact _.
     apply Build_Is0Functor.
     intros A B [f g].
     exact (functor_join f g).
@@ -569,6 +571,7 @@ Section FunctorJoin.
 
   Global Instance is1bifunctor_join : Is1Bifunctor Join.
   Proof.
+    snrapply Build_Is1Bifunctor'.
     snrapply Build_Is1Functor.
     - intros A B f g [p q].
       exact (functor2_join p q).
diff --git a/theories/Homotopy/Smash.v b/theories/Homotopy/Smash.v
index 4bcb8b00d71..cc26c8374cf 100644
--- a/theories/Homotopy/Smash.v
+++ b/theories/Homotopy/Smash.v
@@ -353,6 +353,8 @@ Defined.
 
 Global Instance is0bifunctor_smash : Is0Bifunctor Smash.
 Proof.
+  snrapply Build_Is0Bifunctor'.
+  1,2: exact _.
   nrapply Build_Is0Functor.
   intros [X Y] [A B] [f g].
   exact (functor_smash f g).
@@ -360,6 +362,7 @@ Defined.
 
 Global Instance is1bifunctor_smash : Is1Bifunctor Smash.
 Proof.
+  snrapply Build_Is1Bifunctor'.
   snrapply Build_Is1Functor.
   - intros [X Y] [A B] [f g] [h i] [p q].
     exact (functor_smash_homotopic p q).
diff --git a/theories/WildCat/Bifunctor.v b/theories/WildCat/Bifunctor.v
index ea198198014..86f4ce1d077 100644
--- a/theories/WildCat/Bifunctor.v
+++ b/theories/WildCat/Bifunctor.v
@@ -7,10 +7,49 @@ Require Import WildCat.Core WildCat.Prod WildCat.Equiv WildCat.NatTrans WildCat.
 (** ** Definition *)
 
 Class Is0Bifunctor {A B C : Type}
-  `{IsGraph A, IsGraph B, IsGraph C} (F : A -> B -> C)
-  := is0functor_bifunctor_uncurried :: Is0Functor (uncurry F).
+  `{IsGraph A, IsGraph B, IsGraph C} (F : A -> B -> C) := {
+  is0functor_bifunctor_uncurried :: Is0Functor (uncurry F);
+  is0functor01_bifunctor :: forall a, Is0Functor (F a);
+  is0functor10_bifunctor :: forall b, Is0Functor (flip F b);
+}.
+
+Definition Build_Is0Bifunctor' {A B C : Type}
+  `{Is01Cat A, Is01Cat B, IsGraph C} (F : A -> B -> C)
+  `{!Is0Functor (uncurry F)}
+  : Is0Bifunctor F.
+Proof.
+  snrapply Build_Is0Bifunctor.
+  - exact _.
+  - intros a.
+    snrapply Build_Is0Functor.
+    intros b b' g.
+    change (uncurry F (a, b) $-> uncurry F (a, b')).
+    refine (fmap (uncurry F) (_, _)).
+    + exact (Id a).
+    + exact g.
+  - intros b.
+    snrapply Build_Is0Functor.
+    intros a a' f.
+    change (uncurry F (a, b) $-> uncurry F (a', b)).
+    refine (fmap (uncurry F) (_, _)).
+    + exact f.
+    + exact (Id b).
+Defined.
+
+Definition Build_Is0Bifunctor'' {A B C : Type}
+  `{IsGraph A, IsGraph B, Is01Cat C} (F : A -> B -> C)
+  `{!forall a, Is0Functor (F a), !forall b, Is0Functor (flip F b)}
+  : Is0Bifunctor F.
+Proof.
+  snrapply Build_Is0Bifunctor.
+  2,3: exact _.
+  snrapply Build_Is0Functor.
+  intros [a b] [a' b'] [f g].
+  change (F a b $-> F a' b').
+  exact (fmap (flip F b') f $o fmap (F a) g).
+Defined.
 
-Global Instance is0functor01_bifunctor {A B C : Type}
+(* Global Instance is0functor01_bifunctor {A B C : Type}
   `{Is01Cat A, IsGraph B, IsGraph C} (F : A -> B -> C) `{!Is0Bifunctor F}
   : forall a, Is0Functor (F a).
 Proof.
@@ -21,9 +60,9 @@ Proof.
   refine (fmap (uncurry F) (_, _)).
   - exact (Id a).
   - exact g.
-Defined.
+Defined. *)
 
-Global Instance is0functor10_bifunctor {A B C : Type}
+(* Global Instance is0functor10_bifunctor {A B C : Type}
   `{IsGraph A, Is01Cat B, IsGraph C} (F : A -> B -> C) `{!Is0Bifunctor F}
   : forall b, Is0Functor (flip F b).
 Proof.
@@ -34,9 +73,9 @@ Proof.
   refine (fmap (uncurry F) (_, _)).
   - exact f.
   - exact (Id b).
-Defined.
+Defined. *)
 
-Definition Build_Is0Bifunctor {A B C : Type}
+(* Definition Build_Is0Bifunctor {A B C : Type}
   `{IsGraph A, IsGraph B, Is01Cat C} (F : A -> B -> C)
   `{!forall a, Is0Functor (F a), !forall b, Is0Functor (flip F b)}
   : Is0Bifunctor F.
@@ -45,86 +84,18 @@ Proof.
   intros [a b] [a' b'] [f g].
   change (F a b $-> F a' b').
   exact (fmap (flip F b') f $o fmap (F a) g).
-Defined.
-
-Class Is1Bifunctor {A B C : Type}
-  `{Is1Cat A, Is1Cat B, Is1Cat C} (F : A -> B -> C) `{!Is0Bifunctor F}
-  := is1functor_bifunctor_uncurried :: Is1Functor (uncurry F).
-
-Arguments Is1Bifunctor {A B C _ _ _ _ _ _ _ _ _ _ _ _} F {Is0Bifunctor} : rename.
-
-Global Instance is1functor01_bifunctor {A B C : Type} (F : A -> B -> C)
-  `{Is1Bifunctor A B C F}
-  : forall a, Is1Functor (F a).
-Proof.
-  intros a.
-  snrapply Build_Is1Functor.
-  - intros b b' g g' p.
-    refine (fmap2 (uncurry F) (_, _)).
-    + exact (Id (Id a)).
-    + exact p.
-  - intros b.
-    exact (fmap_id (uncurry F) _).
-  - intros b b' b'' f g.
-    srefine (fmap2 (uncurry F) _ $@ _). 
-    + exact (Id a $o Id a, g $o f).
-    + exact ((cat_idl _)^$, Id _).
-    + exact (fmap_comp (uncurry F) (a := (a, b)) (b := (a, b')) (c := (a, b''))
-        (Id a, f) (Id a, g)).
-Defined.
-
-Global Instance is1functor10_bifunctor {A B C : Type} (F : A -> B -> C)
-  `{Is1Bifunctor A B C F}
-  : forall b, Is1Functor (flip F b).
-Proof.
-  intros b.
-  snrapply Build_Is1Functor.
-  - intros a a' f f' p.
-    refine (fmap2 (uncurry F) (_, _)).
-    + exact p.
-    + exact (Id (Id b)).
-  - intros a.
-    exact (fmap_id (uncurry F) _).
-  - intros a a' a'' f g.
-    srefine (fmap2 (uncurry F) _ $@ _).
-    + exact (g $o f, Id b $o Id b).
-    + exact (Id _, (cat_idr _)^$).
-    + exact (fmap_comp (uncurry F) (a := (a, b)) (b := (a', b)) (c := (a'', b))
-        (f, Id b) (g, Id b)).
-Defined.
-
-Definition Build_Is1Bifunctor {A B C : Type}
-  `{Is1Cat A, Is1Cat B, Is1Cat C} (F : A -> B -> C)
-  `{!forall a, Is0Functor (F a), !forall b, Is0Functor (flip F b)}
-  `{!forall a, Is1Functor (F a), !forall b, Is1Functor (flip F b)}
-  (bifunctor_coh : forall a0 a1 (f : a0 $-> a1) b0 b1 (g : b0 $-> b1),
-    fmap (F a1) g $o fmap (flip F b0) f $== fmap (flip F b1) f $o fmap (F a0) g)
-  : Is1Bifunctor (Is0Bifunctor := Build_Is0Bifunctor F) F.
-Proof.
-  snrapply Build_Is1Functor.
-  - intros [a b] [a' b'] [f g] [f' g'] [p p']; unfold fst, snd in * |- .
-    exact (fmap2 (F a) p' $@@ fmap2 (flip F b') p).
-  - intros [a b].
-    exact ((fmap_id (F a) b $@@ fmap_id (flip F b) _) $@ cat_idr _).
-  - intros [a b] [a' b'] [a'' b''] [f g] [f' g']; unfold fst, snd in * |- . 
-    refine ((fmap_comp (F a) g g' $@@ fmap_comp (flip F b'') f f') $@ _).
-    nrefine (cat_assoc_opp _ _ _ $@ (_ $@R _) $@ cat_assoc _ _ _).
-    refine (cat_assoc _ _ _ $@ (_ $@L _^$) $@ cat_assoc_opp _ _ _).
-    nrapply bifunctor_coh.
-Defined.
-
-(** ** Bifunctor lemmas *)
+Defined. *)
 
 (** *** 1-functorial action *)
 
 (** [fmap] in the first argument. *)
-Definition fmap10 {A B C : Type} `{IsGraph A, Is01Cat B, IsGraph C}
+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, IsGraph B, IsGraph C}
+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.
@@ -136,9 +107,120 @@ Definition fmap11 {A B C : Type} `{IsGraph A, IsGraph B, IsGraph C}
   : F a0 b0 $-> F a1 b1
   := fmap (uncurry F) (a := (a0, b0)) (b := (a1, b1)) (f, g).
 
+Class Is1Bifunctor {A B C : Type}
+  `{Is1Cat A, Is1Cat B, Is1Cat C} (F : A -> B -> C) `{!Is0Bifunctor F} := {
+
+  is1functor_bifunctor_uncurried :: Is1Functor (uncurry F);
+  is1functor01_bifunctor :: forall a, Is1Functor (F a);
+  is1functor10_bifunctor :: forall b, Is1Functor (flip F b);
+
+  fmap11_is_fmap01_fmap10 {a0 a1} (f : a0 $-> a1) {b0 b1} (g : b0 $-> b1)
+    : fmap11 F f g $== fmap01 F a1 g $o fmap10 F f b0;
+  fmap11_is_fmap10_fmap01 {a0 a1} (f : a0 $-> a1) {b0 b1} (g : b0 $-> b1)
+    : fmap11 F f g $== fmap10 F f b1 $o fmap01 F a0 g;
+}.
+
+Arguments Is1Bifunctor {A B C _ _ _ _ _ _ _ _ _ _ _ _} F {Is0Bifunctor} : rename.
+Arguments Build_Is1Bifunctor {A B C _ _ _ _ _ _ _ _ _ _ _ _} F {_} _ _ _ _ _.
+Arguments fmap11_is_fmap01_fmap10 {A B C _ _ _ _ _ _ _ _ _ _ _ _} F
+  {Is0Bifunctor Is1Bifunctor} {a0 a1} f {b0 b1} g : rename.
+Arguments fmap11_is_fmap10_fmap01 {A B C _ _ _ _ _ _ _ _ _ _ _ _} F
+  {Is0Bifunctor Is1Bifunctor} {a0 a1} f {b0 b1} g : rename.
+
+Definition Build_Is1Bifunctor' {A B C : Type}
+  `{Is1Cat A, Is1Cat B, Is1Cat C} (F : A -> B -> C)
+  `{!Is0Functor (uncurry F), !Is1Functor (uncurry F)}
+  : Is1Bifunctor (Is0Bifunctor := Build_Is0Bifunctor' F) F.
+Proof.
+  snrapply Build_Is1Bifunctor.
+  - exact _.
+  - intros a.
+    snrapply Build_Is1Functor.
+    + intros b b' g g' p.
+      refine (fmap2 (uncurry F) _).
+      exact (Id (Id a), p).
+    + intros b.
+      exact (fmap_id (uncurry F) _).
+    + intros b b' b'' f g.
+      srefine (fmap2 (uncurry F) _ $@ _). 
+      * exact (Id a $o Id a, g $o f).
+      * exact ((cat_idl _)^$, Id _).
+      * exact (fmap_comp (uncurry F) (a := (a, b)) (b := (a, b')) (c := (a, b''))
+          (Id a, f) (Id a, g)).
+  - intros b.
+    snrapply Build_Is1Functor.
+    + intros a a' f f' p.
+      refine (fmap2 (uncurry F) _).
+      exact (p, Id (Id b)).
+    + intros a.
+      exact (fmap_id (uncurry F) _).
+    + intros a a' a'' f g.
+      srefine (fmap2 (uncurry F) _ $@ _).
+      * exact (g $o f, Id b $o Id b).
+      * exact (Id _, (cat_idr _)^$).
+      * exact (fmap_comp (uncurry F) (a := (a, b)) (b := (a', b)) (c := (a'', b))
+          (f, Id b) (g, Id b)).
+  - intros a0 a1 f b0 b1 g.
+    refine (fmap2 (uncurry F) _^$ $@ fmap_comp (uncurry F)
+      (a := (a0, b0)) (b := (a1, b0)) (c := (a1, b1)) (f, Id b0) (Id a1, g)).
+    exact (cat_idl _, cat_idr _).
+  - intros a0 a1 f b0 b1 g.
+    refine (fmap2 (uncurry F) _^$ $@ fmap_comp (uncurry F)
+      (a := (a0, b0)) (b := (a0, b1)) (c := (a1, b1)) (Id a0, g) (f, Id b1)).
+    exact (cat_idr _, cat_idl _).
+Defined.
+
+Definition Build_Is1Bifunctor'' {A B C : Type}
+  `{Is1Cat A, Is1Cat B, Is1Cat C} (F : A -> B -> C)
+  `{!forall a, Is0Functor (F a), !forall b, Is0Functor (flip F b)}
+  (Is0Bifunctor_F := Build_Is0Bifunctor'' F)
+  `{!forall a, Is1Functor (F a), !forall b, Is1Functor (flip F b)}
+  (bifunctor_coh : forall a0 a1 (f : a0 $-> a1) b0 b1 (g : b0 $-> b1),
+    fmap01 F a1 g $o fmap10 F f b0 $== fmap10 F f b1 $o fmap01 F a0 g)
+  : Is1Bifunctor F.
+Proof.
+  snrapply Build_Is1Bifunctor.
+  - snrapply Build_Is1Functor.
+    + intros [a b] [a' b'] [f g] [f' g'] [p p']; unfold fst, snd in * |- .
+      exact (fmap2 (F a) p' $@@ fmap2 (flip F b') p).
+    + intros [a b].
+      exact ((fmap_id (F a) b $@@ fmap_id (flip F b) _) $@ cat_idr _).
+    + intros [a b] [a' b'] [a'' b''] [f g] [f' g']; unfold fst, snd in * |- . 
+      refine ((fmap_comp (F a) g g' $@@ fmap_comp (flip F b'') f f') $@ _).
+      nrefine (cat_assoc_opp _ _ _ $@ (_ $@R _) $@ cat_assoc _ _ _).
+      refine (cat_assoc _ _ _ $@ (_ $@L _^$) $@ cat_assoc_opp _ _ _).
+      nrapply bifunctor_coh.
+  - exact _.
+  - exact _.
+  - intros a0 a1 f b0 b1 g.
+    exact (bifunctor_coh a0 a1 f b0 b1 g)^$.
+  - intros a0 a1 f b0 b1 g.
+    reflexivity.
+Defined.
+
+(** Here is an alternative constructor that uses [fmap01] and [fmap10] instead. *)
+(* Definition Build_Is1Bifunctor' {A B C : Type}
+  `{Is1Cat A, Is1Cat B, Is1Cat C} (F : A -> B -> C)
+  `{!forall a, Is0Functor (F a), !forall b, Is0Functor (flip F b)}
+  `{!forall a, Is1Functor (F a), !forall b, Is1Functor (flip F b)}
+  (Is0Bifunctor_F := Build_Is0Bifunctor F)
+  (bifunctor_coh : forall a0 a1 (f : a0 $-> a1) b0 b1 (g : b0 $-> b1),
+    fmap01 F a1 g $o fmap10 F f b0 $== fmap10 F f b1 $o fmap01 F a0 g)
+  : Is1Bifunctor F.
+Proof.
+  snrapply Build_Is1Bifunctor.
+  1,2: exact _.
+  intros a0 a1 f b0 b1 g.
+  refine ((_ $@@ _)^$ $@ bifunctor_coh a0 a1 f b0 b1 g $@ (_ $@@ _)).
+  1,4: exact ((_ $@L fmap_id (F _) _) $@ cat_idr _).
+  1,2: exact (( fmap_id (flip F _) _ $@R _) $@ cat_idl _).
+Defined. *)
+
+(** ** Bifunctor lemmas *)
+
 (** *** Coherence *)
 
-Definition fmap11_is_fmap01_fmap10 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
+(* Definition fmap11_is_fmap01_fmap10 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
   (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
   {a0 a1 : A} (f : a0 $-> a1) {b0 b1 : B} (g : b0 $-> b1)
   : fmap11 F f g $== fmap01 F a1 g $o fmap10 F f b0.
@@ -146,9 +228,9 @@ Proof.
   refine (fmap2 (uncurry F) _^$ $@ fmap_comp (uncurry F)
     (a := (a0, b0)) (b := (a1, b0)) (c := (a1, b1)) (f, Id b0) (Id a1, g)).
   exact (cat_idl _, cat_idr _).
-Defined.
+Defined. *)
 
-Definition fmap11_is_fmap10_fmap01 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
+(* Definition fmap11_is_fmap10_fmap01 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
   (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
   {a0 a1 : A} (f : a0 $-> a1) {b0 b1 : B} (g : b0 $-> b1)
   : fmap11 F f g $== fmap10 F f b1 $o fmap01 F a0 g.
@@ -156,7 +238,7 @@ Proof.
   refine (fmap2 (uncurry F) _^$ $@ fmap_comp (uncurry F)
     (a := (a0, b0)) (b := (a0, b1)) (c := (a1, b1)) (Id a0, g) (f, Id b1)).
   exact (cat_idr _, cat_idl _).
-Defined.
+Defined. *)
 
 Definition bifunctor_coh {A B C : Type}
   (F : A -> B -> C) `{Is1Bifunctor A B C F}
@@ -223,6 +305,20 @@ Definition fmap11_id {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
   : fmap11 F (Id a) (Id b) $== Id (F a b)
   := fmap_id (uncurry F) (a, b).
 
+(** [fmap11] with left map the identity gives [fmap01]. *)
+Definition fmap01_is_fmap11 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
+  (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
+  (a : A) {b0 b1 : B} (g : b0 $-> b1)
+  : fmap11 F (Id a) g $== fmap01 F a g
+  := fmap11_is_fmap01_fmap10 _ _ _ $@ (_ $@L fmap10_id _ _ _) $@ cat_idr _.
+
+(** [fmap11] with right map the identity gives [fmap10]. *)
+Definition fmap10_is_fmap11 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
+  (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
+  {a0 a1 : A} (f : a0 $-> a1) (b : B)
+  : fmap11 F f (Id b) $== fmap10 F f b
+  := fmap11_is_fmap01_fmap10 _ _ _ $@ (fmap01_id _ _ _ $@R _) $@ cat_idl _.
+
 (** *** Composition preservation *)
 
 Definition fmap01_comp {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
@@ -289,37 +385,29 @@ Definition is0bifunctor_flip {A B C : Type}
   (F : A -> B -> C) `{Is01Cat A, Is01Cat B, Is01Cat C, !Is0Bifunctor F}
   : Is0Bifunctor (flip F).
 Proof.
-  change (Is0Functor (uncurry F o equiv_prod_symm _ _)).
-  exact _.
+  snrapply Build_Is0Bifunctor.
+  - change (Is0Functor (uncurry F o equiv_prod_symm _ _)).
+    exact _.
+  - exact _.
+  - exact _.
 Defined.
 Hint Immediate is0bifunctor_flip : typeclass_instances.
 
 Definition is1bifunctor_flip {A B C : Type}
 (F : A -> B -> C) `{H : Is1Bifunctor A B C F}
   : Is1Bifunctor (flip F).
-Proof.
-  change (Is1Functor (uncurry F o equiv_prod_symm _ _)).
-  exact _.
-Defined.
-Hint Immediate is1bifunctor_flip : typeclass_instances.
-
-(** Here is an alternative constructor that uses [fmap01] and [fmap10] instead. *)
-Definition Build_Is1Bifunctor' {A B C : Type}
-  `{Is1Cat A, Is1Cat B, Is1Cat C} (F : A -> B -> C)
-  `{!forall a, Is0Functor (F a), !forall b, Is0Functor (flip F b)}
-  `{!forall a, Is1Functor (F a), !forall b, Is1Functor (flip F b)}
-  (Is0Bifunctor_F := Build_Is0Bifunctor F)
-  (bifunctor_coh : forall a0 a1 (f : a0 $-> a1) b0 b1 (g : b0 $-> b1),
-    fmap01 F a1 g $o fmap10 F f b0 $== fmap10 F f b1 $o fmap01 F a0 g)
-  : Is1Bifunctor F.
 Proof.
   snrapply Build_Is1Bifunctor.
-  1,2: exact _.
-  intros a0 a1 f b0 b1 g.
-  refine ((_ $@@ _)^$ $@ bifunctor_coh a0 a1 f b0 b1 g $@ (_ $@@ _)).
-  1,4: exact ((_ $@L fmap_id (F _) _) $@ cat_idr _).
-  1,2: exact (( fmap_id (flip F _) _ $@R _) $@ cat_idl _).
+  - change (Is1Functor (uncurry F o equiv_prod_symm _ _)).
+    exact _.
+  - exact _.
+  - exact _.
+  - intros b0 b1 g a0 a1 f.
+    exact (fmap11_is_fmap10_fmap01 F f g).
+  - intros b0 b1 g a0 a1 f.
+    exact (fmap11_is_fmap01_fmap10 F f g).
 Defined.
+Hint Immediate is1bifunctor_flip : typeclass_instances.
 
 (** ** Composition of bifunctors *)
 
@@ -330,10 +418,8 @@ Global Instance is0bifunctor_postcompose {A B C D : Type}
   `{IsGraph A, IsGraph B, IsGraph C, IsGraph D}
   (F : A -> B -> C) {bf : Is0Bifunctor F}
   (G : C -> D) `{!Is0Functor G}
-  : Is0Bifunctor (fun a b => G (F a b)).
-Proof.
-  rapply is0functor_compose.
-Defined.
+  : Is0Bifunctor (fun a b => G (F a b))
+  := {}.
 
 Global Instance is1bifunctor_postcompose {A B C D : Type}
   `{Is1Cat A, Is1Cat B, Is1Cat C, Is1Cat D}
@@ -341,7 +427,12 @@ Global Instance is1bifunctor_postcompose {A B C D : Type}
   `{!Is0Bifunctor F} {bf : Is1Bifunctor F}
   : Is1Bifunctor (fun a b => G (F a b)).
 Proof.
-  rapply is1functor_compose.
+  snrapply Build_Is1Bifunctor.
+  1-3: exact _.
+  - intros a0 a1 f b0 b1 g.
+    exact (fmap2 G (fmap11_is_fmap01_fmap10 F f g) $@ fmap_comp G _ _).
+  - intros a0 a1 f b0 b1 g.
+    exact (fmap2 G (fmap11_is_fmap10_fmap01 F f g) $@ fmap_comp G _ _).
 Defined.
 
 Global Instance is0bifunctor_precompose {A B C D E : Type}
@@ -350,8 +441,13 @@ Global Instance is0bifunctor_precompose {A B C D E : Type}
   `{!Is0Functor G, !Is0Bifunctor F, !Is0Functor K}
   : Is0Bifunctor (fun a b => F (G a) (K b)).
 Proof.
-  change (Is0Functor (uncurry F o functor_prod G K)).
-  exact _.
+  snrapply Build_Is0Bifunctor.
+  - change (Is0Functor (uncurry F o functor_prod G K)).
+    exact _.
+  - exact _.
+  - intros e.
+    change (Is0Functor (flip F (K e) o G)).
+    exact _.
 Defined.
 
 Global Instance is1bifunctor_precompose {A B C D E : Type}
@@ -361,8 +457,17 @@ Global Instance is1bifunctor_precompose {A B C D E : Type}
     !Is0Functor K, !Is1Functor K}
   : Is1Bifunctor (fun a b => F (G a) (K b)).
 Proof.
-  change (Is1Functor (uncurry F o functor_prod G K)).
-  exact _.
+  snrapply Build_Is1Bifunctor.
+  - change (Is1Functor (uncurry F o functor_prod G K)).
+    exact _.
+  - exact _.
+  - intros e.
+    change (Is1Functor (flip F (K e) o G)).
+    exact _.
+  - intros a0 a1 f b0 b1 g.
+    exact (fmap11_is_fmap01_fmap10 F (fmap G f) (fmap K g)).
+  - intros a0 a1 f b0 b1 g.
+    exact (fmap11_is_fmap10_fmap01 F (fmap G f) (fmap K g)).
 Defined.
 
 Global Instance is0functor_uncurry_uncurry_left {A B C D E}
diff --git a/theories/WildCat/Monoidal.v b/theories/WildCat/Monoidal.v
index 2ab1f483d77..38abf2de889 100644
--- a/theories/WildCat/Monoidal.v
+++ b/theories/WildCat/Monoidal.v
@@ -165,23 +165,30 @@ Section Associator.
     : associator x' y z $o fmap10 F f (F y z)
       $== fmap10 F (fmap10 F f y) z $o associator x y z.
   Proof.
-    refine ((_ $@L _^$) $@ associator_nat f (Id _) (Id _)).
-    exact (fmap12 _ _ (fmap11_id _ _ _)).
+    refine ((_ $@L _^$) $@ _ $@ (_ $@R _)).
+    2: rapply (associator_nat f (Id _) (Id _)).
+    - exact (fmap12 _ _ (fmap11_id _ _ _) $@ fmap10_is_fmap11 _ _ _).
+    - exact (fmap21 _ (fmap10_is_fmap11 _ _ _) _ $@ fmap10_is_fmap11 _ _ _).
   Defined.
 
   Local Definition associator_nat_m (x : A) {y y' : A} (g : y $-> y') (z : A)
     : associator x y' z $o fmap01 F x (fmap10 F g z)
       $== fmap10 F (fmap01 F x g) z $o associator x y z.
   Proof.
-    exact (associator_nat (Id _) g (Id _)).
+    refine ((_ $@L _^$) $@ _ $@ (_ $@R _)).
+    2: nrapply (associator_nat (Id _) g (Id _)).
+    - exact (fmap12 _ _ (fmap10_is_fmap11 _ _ _) $@ fmap01_is_fmap11 _ _ _).
+    - exact (fmap21 _ (fmap01_is_fmap11 _ _ _) _ $@ fmap10_is_fmap11 _ _ _).
   Defined.
 
   Local Definition associator_nat_r (x y : A) {z z' : A} (h : z $-> z')
     : associator x y z' $o fmap01 F x (fmap01 F y h)
       $== fmap01 F (F x y) h $o associator x y z.
   Proof.
-    nrefine (associator_nat (Id _) (Id _) h $@ (_ $@R _)).
-    exact (fmap21 _ (fmap11_id _ _ _) _ ).
+    refine ((_ $@L _^$) $@ _ $@ (_ $@R _)).
+    2: nrapply (associator_nat (Id _) (Id _) h).
+    - exact (fmap12 _ _ (fmap01_is_fmap11 _ _ _) $@ fmap01_is_fmap11 _ _ _).
+    - exact (fmap21 _ (fmap11_id _ _ _) _ $@ fmap01_is_fmap11 F _ _).
   Defined.
 
 End Associator.
@@ -357,6 +364,7 @@ Section SymmetricBraid.
   Local Definition braid_nat_l {a b c} (f : a $-> b)
     : braid b c $o fmap10 F f c $== fmap01 F c f $o braid a c.
   Proof.
+    refine ((_ $@L (fmap10_is_fmap11 _ _ _)^$) $@ _ $@ (fmap01_is_fmap11 _ _ _ $@R _)).
     exact (is1natural_braiding_uncurried (a, c) (b, c) (f, Id _)).
   Defined.
 
@@ -364,6 +372,7 @@ Section SymmetricBraid.
   Local Definition braid_nat_r {a b c} (g : b $-> c)
     : braid a c $o fmap01 F a g $== fmap10 F g a $o braid a b.
   Proof.
+    refine ((_ $@L (fmap01_is_fmap11 _ _ _)^$) $@ _ $@ (fmap10_is_fmap11 _ _ _ $@R _)).
     exact (is1natural_braiding_uncurried (a, b) (a, c) (Id _ , g)).
   Defined.
 
@@ -449,23 +458,33 @@ Section TwistConstruction.
     : twist a' b c $o fmap10 cat_tensor f (cat_tensor b c)
       $== fmap01 cat_tensor b (fmap10 cat_tensor f c) $o twist a b c.
   Proof.
-    refine ((_ $@L _^$) $@ twist_nat a a' b b c c f (Id _) (Id _)).
-    exact (fmap12 _ _ (fmap11_id _ _ _)).
+    refine ((_ $@L _^$) $@ twist_nat a a' b b c c f (Id _) (Id _) $@ (_ $@R _)).
+    - refine (fmap12 _ _ _ $@ fmap10_is_fmap11 _ _ _).
+      rapply fmap11_id.
+    - refine (fmap12 _ _ _ $@ fmap01_is_fmap11 _ _ _).
+      rapply fmap10_is_fmap11.
   Defined.
 
   Local Definition twist_nat_m a {b b'} (g : b $-> b') c
     : twist a b' c $o fmap01 cat_tensor a (fmap10 cat_tensor g c)
       $== fmap10 cat_tensor g (cat_tensor a c) $o twist a b c.
   Proof.
-    nrefine (twist_nat a a b b' c c (Id _) g (Id _) $@ (_ $@R _)).
-    exact (fmap12 _ _ (fmap11_id _ _ _)).
+    refine ((_ $@L _^$) $@ twist_nat a a b b' c c (Id _) g (Id _) $@ (_ $@R _)).
+    - refine (fmap12 _ _ _ $@ fmap01_is_fmap11 _ _ _).
+      rapply fmap10_is_fmap11.
+    - refine (fmap12 _ _ _ $@ fmap10_is_fmap11 _ _ _).
+      rapply fmap11_id.
   Defined.
 
   Local Definition twist_nat_r a b {c c'} (h : c $-> c')
     : twist a b c' $o fmap01 cat_tensor a (fmap01 cat_tensor b h)
       $== fmap01 cat_tensor b (fmap01 cat_tensor a h) $o twist a b c.
   Proof.
-    exact (twist_nat a a b b c c' (Id _) (Id _) h).
+    refine ((_ $@L _^$) $@ twist_nat a a b b c c' (Id _) (Id _) h $@ (_ $@R _)).
+    - refine (fmap12 _ _ _ $@ fmap01_is_fmap11 _ _ _).
+      rapply fmap01_is_fmap11.
+    - refine (fmap12 _ _ _ $@ fmap01_is_fmap11 _ _ _).
+      rapply fmap01_is_fmap11.
   Defined.
 
   (** *** Movement lemmas *)
@@ -606,6 +625,9 @@ Section TwistConstruction.
       (** The second square is just the naturality of twist. *)
       nrapply vconcat.
       2: apply twist_nat.
+      nrapply hconcatL.
+      2: nrapply hconcatR.
+      1,3: symmetry; rapply fmap01_is_fmap11.
       (** Leaving us with a square with a functor application. *)
       rapply fmap11_square.
       1: rapply vrefl.
@@ -628,7 +650,7 @@ Section TwistConstruction.
         change (?w $o ?x $== ?y $o ?z) with (Square z w x y).
         nrapply vconcat.
         2: rapply (isnat right_unitor f).
-        rapply braid_nat.
+        rapply braid_nat_r.
     - intros a.
       rapply compose_catie'.
       rapply catie_braid.
diff --git a/theories/WildCat/Products.v b/theories/WildCat/Products.v
index 461575b2b4a..002ef175a61 100644
--- a/theories/WildCat/Products.v
+++ b/theories/WildCat/Products.v
@@ -440,6 +440,8 @@ Defined.
 Local Instance is0bifunctor_boolrec {A : Type} `{Is1Cat A}
   : Is0Bifunctor (Bool_rec A).
 Proof.
+  snrapply Build_Is0Bifunctor'.
+  1,2: exact _.
   snrapply Build_Is0Functor.
   intros [a b] [a' b'] [f g] [ | ].
   - exact f.
@@ -449,6 +451,7 @@ Defined.
 Local Instance is1bifunctor_boolrec {A : Type} `{Is1Cat A}
   : Is1Bifunctor (Bool_rec A).
 Proof.
+  snrapply Build_Is1Bifunctor'.
   snrapply Build_Is1Functor.
   - intros [a b] [a' b'] [f g] [f' g'] [p q] [ | ].
     + exact p.
@@ -479,28 +482,28 @@ Global Instance is0functor_cat_binprod_l {A : Type} `{HasBinaryProducts A}
   (y : A)
   : Is0Functor (fun x => cat_binprod x y).
 Proof.
-  exact (is0functor10_bifunctor _ y).
+  exact (is0functor10_bifunctor y).
 Defined.
 
 Global Instance is1functor_cat_binprod_l {A : Type} `{HasBinaryProducts A}
   (y : A)
   : Is1Functor (fun x => cat_binprod x y).
 Proof.
-  exact (is1functor10_bifunctor _ y).
+  exact (is1functor10_bifunctor y).
 Defined.
 
 Global Instance is0functor_cat_binprod_r {A : Type} `{HasBinaryProducts A}
   (x : A)
   : Is0Functor (fun y => cat_binprod x y).
 Proof.
-  exact (is0functor01_bifunctor _ x).
+  exact (is0functor01_bifunctor x).
 Defined.
 
 Global Instance is1functor_cat_binprod_r {A : Type} `{HasBinaryProducts A}
   (x : A)
   : Is1Functor (fun y => cat_binprod x y).
 Proof.
-  exact (is1functor01_bifunctor _ x).
+  exact (is1functor01_bifunctor x).
 Defined.
 
 (** [cat_binprod_corec] is also functorial in each morphsism. *)
diff --git a/theories/WildCat/Yoneda.v b/theories/WildCat/Yoneda.v
index f66af222d70..93053cec156 100644
--- a/theories/WildCat/Yoneda.v
+++ b/theories/WildCat/Yoneda.v
@@ -44,13 +44,20 @@ Proof.
 Defined.
 
 Global Instance is0bifunctor_hom {A} `{Is01Cat A}
-  : Is0Bifunctor (A:=A^op) (B:=A) (C:=Type) (@Hom A _)
-  := is0functor_hom.
+  : Is0Bifunctor (A:=A^op) (B:=A) (C:=Type) (@Hom A _).
+Proof.
+  nrapply Build_Is0Bifunctor'.
+  1-2: exact _.
+  exact is0functor_hom.
+Defined.
 
 (** 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:=A^op) (B:=A) (C:=Type) (@Hom A _)
-  := is1functor_hom.
+  : Is1Bifunctor (A:=A^op) (B:=A) (C:=Type) (@Hom A _).
+Proof.
+  nrapply Build_Is1Bifunctor'.
+  exact is1functor_hom.
+Defined.
 
 Definition fun01_hom {A} `{Is01Cat A}
   : Fun01 (A^op * A) Type
@@ -255,12 +262,19 @@ Proof.
 Defined.
 
 Global Instance is0bifunctor_hom_0gpd {A : Type} `{Is1Cat A}
-  : Is0Bifunctor (A:=A^op) (B:=A) (C:=ZeroGpd) (opyon_0gpd (A:=A))
-  := is0functor_hom_0gpd.
+  : Is0Bifunctor (A:=A^op) (B:=A) (C:=ZeroGpd) (opyon_0gpd (A:=A)).
+Proof.
+  snrapply Build_Is0Bifunctor'.
+  1,2: exact _.
+  exact is0functor_hom_0gpd.
+Defined.
 
 Global Instance is1bifunctor_hom_0gpd {A : Type} `{Is1Cat A}
-  : Is1Bifunctor (A:=A^op) (B:=A) (C:=ZeroGpd) (opyon_0gpd (A:=A))
-  := is1functor_hom_0gpd.
+  : Is1Bifunctor (A:=A^op) (B:=A) (C:=ZeroGpd) (opyon_0gpd (A:=A)).
+Proof.
+  snrapply Build_Is1Bifunctor'.
+  exact is1functor_hom_0gpd.
+Defined.
 
 Global Instance is0functor_opyon_0gpd {A : Type} `{Is1Cat A} (a : A)
   : Is0Functor (opyon_0gpd a).

From dd7d652398e7fbc8d42afd51fb6ccb2833d5871c Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Mon, 6 May 2024 20:53:33 +0100
Subject: [PATCH 05/10] cleanup dead code and revert changes in AbSES

Signed-off-by: Ali Caglayan <alizter@gmail.com>
---
 theories/Algebra/AbSES/Ext.v     | 12 ++---
 theories/Algebra/AbSES/SixTerm.v |  3 +-
 theories/Homotopy/Join/Core.v    |  2 +-
 theories/WildCat/Bifunctor.v     | 75 --------------------------------
 4 files changed, 6 insertions(+), 86 deletions(-)

diff --git a/theories/Algebra/AbSES/Ext.v b/theories/Algebra/AbSES/Ext.v
index 03030e91923..317a9f4cd35 100644
--- a/theories/Algebra/AbSES/Ext.v
+++ b/theories/Algebra/AbSES/Ext.v
@@ -129,12 +129,8 @@ Global Instance is1bifunctor_abext `{Univalence}
 Proof.
   snrapply Build_Is1Bifunctor''.
   1,2: exact _.
-  intros A B f C D g.
-  intros x.
-  strip_truncations; cbn.
-  pose proof (bifunctor_coh (Ext : AbGroup^op -> AbGroup -> pType) f g (tr x)) as X.
-  cbn in X.
-  exact X.
+  intros A B.
+  exact (bifunctor_coh (Ext : AbGroup^op -> AbGroup -> pType)).
 Defined.
 
 (** We can push out a fixed extension while letting the map vary, and this defines a group homomorphism. *)
@@ -143,10 +139,10 @@ Definition abses_pushout_ext `{Univalence}
   : GroupHomomorphism (ab_hom A G) (ab_ext B G).
 Proof.
   snrapply Build_GroupHomomorphism.
-  1: exact (fun f => fmap (Ext' (_ : AbGroup^op)) f (tr E)).
+  1: exact (fun f => fmap01 (A:=AbGroup^op) Ext' _ f (tr E)).
   intros f g; cbn.
   nrapply (ap tr).
-  exact (baer_sum_distributive_pushouts (E:=E) f g).
+  exact (baer_sum_distributive_pushouts f g).
 Defined.
 
 (** ** Extensions ending in a projective are trivial *)
diff --git a/theories/Algebra/AbSES/SixTerm.v b/theories/Algebra/AbSES/SixTerm.v
index 4bbde9d4dd6..0a3a4113b2f 100644
--- a/theories/Algebra/AbSES/SixTerm.v
+++ b/theories/Algebra/AbSES/SixTerm.v
@@ -98,8 +98,7 @@ Proof.
       destruct g as [g k].
     exists g.
     apply path_sigma_hprop; cbn.
-    elim k^. 
-    by apply equiv_path_grouphomomorphism.
+    exact k^. 
 Defined.
 
 (** *** Exactness of [ab_hom A G -> Ext1 B G -> Ext1 E G]. *)
diff --git a/theories/Homotopy/Join/Core.v b/theories/Homotopy/Join/Core.v
index 2fa52e4b4a8..50b7d943cd5 100644
--- a/theories/Homotopy/Join/Core.v
+++ b/theories/Homotopy/Join/Core.v
@@ -572,7 +572,7 @@ Section FunctorJoin.
   Global Instance is1bifunctor_join : Is1Bifunctor Join.
   Proof.
     snrapply Build_Is1Bifunctor'.
-    snrapply Build_Is1Functor.
+    nrapply Build_Is1Functor.
     - intros A B f g [p q].
       exact (functor2_join p q).
     - intros A; exact functor_join_idmap.
diff --git a/theories/WildCat/Bifunctor.v b/theories/WildCat/Bifunctor.v
index 86f4ce1d077..4de0ebc8096 100644
--- a/theories/WildCat/Bifunctor.v
+++ b/theories/WildCat/Bifunctor.v
@@ -49,43 +49,6 @@ Proof.
   exact (fmap (flip F b') f $o fmap (F a) g).
 Defined.
 
-(* Global Instance is0functor01_bifunctor {A B C : Type}
-  `{Is01Cat A, IsGraph B, IsGraph C} (F : A -> B -> C) `{!Is0Bifunctor F}
-  : forall a, Is0Functor (F a).
-Proof.
-  intros a.
-  snrapply Build_Is0Functor.
-  intros b b' g.
-  change (uncurry F (a, b) $-> uncurry F (a, b')).
-  refine (fmap (uncurry F) (_, _)).
-  - exact (Id a).
-  - exact g.
-Defined. *)
-
-(* Global Instance is0functor10_bifunctor {A B C : Type}
-  `{IsGraph A, Is01Cat B, IsGraph C} (F : A -> B -> C) `{!Is0Bifunctor F}
-  : forall b, Is0Functor (flip F b).
-Proof.
-  intros b.
-  snrapply Build_Is0Functor.
-  intros a a' f.
-  change (uncurry F (a, b) $-> uncurry F (a', b)).
-  refine (fmap (uncurry F) (_, _)).
-  - exact f.
-  - exact (Id b).
-Defined. *)
-
-(* Definition Build_Is0Bifunctor {A B C : Type}
-  `{IsGraph A, IsGraph B, Is01Cat C} (F : A -> B -> C)
-  `{!forall a, Is0Functor (F a), !forall b, Is0Functor (flip F b)}
-  : Is0Bifunctor F.
-Proof.
-  snrapply Build_Is0Functor.
-  intros [a b] [a' b'] [f g].
-  change (F a b $-> F a' b').
-  exact (fmap (flip F b') f $o fmap (F a) g).
-Defined. *)
-
 (** *** 1-functorial action *)
 
 (** [fmap] in the first argument. *)
@@ -198,48 +161,10 @@ Proof.
     reflexivity.
 Defined.
 
-(** Here is an alternative constructor that uses [fmap01] and [fmap10] instead. *)
-(* Definition Build_Is1Bifunctor' {A B C : Type}
-  `{Is1Cat A, Is1Cat B, Is1Cat C} (F : A -> B -> C)
-  `{!forall a, Is0Functor (F a), !forall b, Is0Functor (flip F b)}
-  `{!forall a, Is1Functor (F a), !forall b, Is1Functor (flip F b)}
-  (Is0Bifunctor_F := Build_Is0Bifunctor F)
-  (bifunctor_coh : forall a0 a1 (f : a0 $-> a1) b0 b1 (g : b0 $-> b1),
-    fmap01 F a1 g $o fmap10 F f b0 $== fmap10 F f b1 $o fmap01 F a0 g)
-  : Is1Bifunctor F.
-Proof.
-  snrapply Build_Is1Bifunctor.
-  1,2: exact _.
-  intros a0 a1 f b0 b1 g.
-  refine ((_ $@@ _)^$ $@ bifunctor_coh a0 a1 f b0 b1 g $@ (_ $@@ _)).
-  1,4: exact ((_ $@L fmap_id (F _) _) $@ cat_idr _).
-  1,2: exact (( fmap_id (flip F _) _ $@R _) $@ cat_idl _).
-Defined. *)
-
 (** ** Bifunctor lemmas *)
 
 (** *** Coherence *)
 
-(* Definition fmap11_is_fmap01_fmap10 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
-  (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
-  {a0 a1 : A} (f : a0 $-> a1) {b0 b1 : B} (g : b0 $-> b1)
-  : fmap11 F f g $== fmap01 F a1 g $o fmap10 F f b0.
-Proof.
-  refine (fmap2 (uncurry F) _^$ $@ fmap_comp (uncurry F)
-    (a := (a0, b0)) (b := (a1, b0)) (c := (a1, b1)) (f, Id b0) (Id a1, g)).
-  exact (cat_idl _, cat_idr _).
-Defined. *)
-
-(* Definition fmap11_is_fmap10_fmap01 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
-  (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
-  {a0 a1 : A} (f : a0 $-> a1) {b0 b1 : B} (g : b0 $-> b1)
-  : fmap11 F f g $== fmap10 F f b1 $o fmap01 F a0 g.
-Proof.
-  refine (fmap2 (uncurry F) _^$ $@ fmap_comp (uncurry F)
-    (a := (a0, b0)) (b := (a0, b1)) (c := (a1, b1)) (Id a0, g) (f, Id b1)).
-  exact (cat_idr _, cat_idl _).
-Defined. *)
-
 Definition bifunctor_coh {A B C : Type}
   (F : A -> B -> C) `{Is1Bifunctor A B C F}
   {a0 a1 : A} (f : a0 $-> a1) {b0 b1 : B} (g : b0 $-> b1)

From bc36433ea43b50377b85edec187bcfd04488e995 Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Mon, 6 May 2024 20:54:42 +0100
Subject: [PATCH 06/10] whitespace

Signed-off-by: Ali Caglayan <alizter@gmail.com>
---
 theories/Algebra/AbSES/SixTerm.v | 2 +-
 theories/WildCat/Bifunctor.v     | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/Algebra/AbSES/SixTerm.v b/theories/Algebra/AbSES/SixTerm.v
index 0a3a4113b2f..34a8ccb7e9d 100644
--- a/theories/Algebra/AbSES/SixTerm.v
+++ b/theories/Algebra/AbSES/SixTerm.v
@@ -98,7 +98,7 @@ Proof.
       destruct g as [g k].
     exists g.
     apply path_sigma_hprop; cbn.
-    exact k^. 
+    exact k^.
 Defined.
 
 (** *** Exactness of [ab_hom A G -> Ext1 B G -> Ext1 E G]. *)
diff --git a/theories/WildCat/Bifunctor.v b/theories/WildCat/Bifunctor.v
index 4de0ebc8096..e66798ce0c9 100644
--- a/theories/WildCat/Bifunctor.v
+++ b/theories/WildCat/Bifunctor.v
@@ -105,7 +105,7 @@ Proof.
     + intros b.
       exact (fmap_id (uncurry F) _).
     + intros b b' b'' f g.
-      srefine (fmap2 (uncurry F) _ $@ _). 
+      srefine (fmap2 (uncurry F) _ $@ _).
       * exact (Id a $o Id a, g $o f).
       * exact ((cat_idl _)^$, Id _).
       * exact (fmap_comp (uncurry F) (a := (a, b)) (b := (a, b')) (c := (a, b''))
@@ -148,7 +148,7 @@ Proof.
       exact (fmap2 (F a) p' $@@ fmap2 (flip F b') p).
     + intros [a b].
       exact ((fmap_id (F a) b $@@ fmap_id (flip F b) _) $@ cat_idr _).
-    + intros [a b] [a' b'] [a'' b''] [f g] [f' g']; unfold fst, snd in * |- . 
+    + intros [a b] [a' b'] [a'' b''] [f g] [f' g']; unfold fst, snd in * |- .
       refine ((fmap_comp (F a) g g' $@@ fmap_comp (flip F b'') f f') $@ _).
       nrefine (cat_assoc_opp _ _ _ $@ (_ $@R _) $@ cat_assoc _ _ _).
       refine (cat_assoc _ _ _ $@ (_ $@L _^$) $@ cat_assoc_opp _ _ _).

From a9a576199716b51ee427de866e57ff5950595667 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Tue, 7 May 2024 10:03:10 -0400
Subject: [PATCH 07/10] Bifunctor.v: add comments and simplify some proofs

---
 theories/WildCat/Bifunctor.v | 53 +++++++-----------------------------
 1 file changed, 10 insertions(+), 43 deletions(-)

diff --git a/theories/WildCat/Bifunctor.v b/theories/WildCat/Bifunctor.v
index e66798ce0c9..7d00d13a750 100644
--- a/theories/WildCat/Bifunctor.v
+++ b/theories/WildCat/Bifunctor.v
@@ -6,6 +6,7 @@ Require Import WildCat.Core WildCat.Prod WildCat.Equiv WildCat.NatTrans WildCat.
 
 (** ** Definition *)
 
+(** We choose to store redundant information in the class, so that depending on how an instance is constructed, we will get the expected implementations of [fmap10], [fmap01] and [fmap11]. *)
 Class Is0Bifunctor {A B C : Type}
   `{IsGraph A, IsGraph B, IsGraph C} (F : A -> B -> C) := {
   is0functor_bifunctor_uncurried :: Is0Functor (uncurry F);
@@ -13,6 +14,7 @@ Class Is0Bifunctor {A B C : Type}
   is0functor10_bifunctor :: forall b, Is0Functor (flip F b);
 }.
 
+(** We provide two alternate constructors, allow the user to provide just the first field or the last two fields. *)
 Definition Build_Is0Bifunctor' {A B C : Type}
   `{Is01Cat A, Is01Cat B, IsGraph C} (F : A -> B -> C)
   `{!Is0Functor (uncurry F)}
@@ -20,20 +22,8 @@ Definition Build_Is0Bifunctor' {A B C : Type}
 Proof.
   snrapply Build_Is0Bifunctor.
   - exact _.
-  - intros a.
-    snrapply Build_Is0Functor.
-    intros b b' g.
-    change (uncurry F (a, b) $-> uncurry F (a, b')).
-    refine (fmap (uncurry F) (_, _)).
-    + exact (Id a).
-    + exact g.
-  - intros b.
-    snrapply Build_Is0Functor.
-    intros a a' f.
-    change (uncurry F (a, b) $-> uncurry F (a', b)).
-    refine (fmap (uncurry F) (_, _)).
-    + exact f.
-    + exact (Id b).
+  - exact (is0functor_functor_uncurried01 (uncurry F)).
+  - exact (is0functor_functor_uncurried10 (uncurry F)).
 Defined.
 
 Definition Build_Is0Bifunctor'' {A B C : Type}
@@ -63,13 +53,14 @@ Definition fmap01 {A B C : Type} `{IsGraph A, IsGraph B, IsGraph C}
   : F a b0 $-> F a b1
   := fmap (F a) g.
 
-(** [fmap] in both arguments. Note that we made a choice in the order in which to compose, but the bifunctor coherence condition says that both ways agree. *)
+(** [fmap] in both arguments. *)
 Definition fmap11 {A B C : Type} `{IsGraph A, IsGraph B, IsGraph 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 (uncurry F) (a := (a0, b0)) (b := (a1, b1)) (f, g).
 
+(** As with [Is0Bifunctor], we store redundant information.  In addition, we store the proofs that they are consistent with each other. *)
 Class Is1Bifunctor {A B C : Type}
   `{Is1Cat A, Is1Cat B, Is1Cat C} (F : A -> B -> C) `{!Is0Bifunctor F} := {
 
@@ -90,6 +81,7 @@ Arguments fmap11_is_fmap01_fmap10 {A B C _ _ _ _ _ _ _ _ _ _ _ _} F
 Arguments fmap11_is_fmap10_fmap01 {A B C _ _ _ _ _ _ _ _ _ _ _ _} F
   {Is0Bifunctor Is1Bifunctor} {a0 a1} f {b0 b1} g : rename.
 
+(** We again provide two alternate constructors. *)
 Definition Build_Is1Bifunctor' {A B C : Type}
   `{Is1Cat A, Is1Cat B, Is1Cat C} (F : A -> B -> C)
   `{!Is0Functor (uncurry F), !Is1Functor (uncurry F)}
@@ -97,32 +89,8 @@ Definition Build_Is1Bifunctor' {A B C : Type}
 Proof.
   snrapply Build_Is1Bifunctor.
   - exact _.
-  - intros a.
-    snrapply Build_Is1Functor.
-    + intros b b' g g' p.
-      refine (fmap2 (uncurry F) _).
-      exact (Id (Id a), p).
-    + intros b.
-      exact (fmap_id (uncurry F) _).
-    + intros b b' b'' f g.
-      srefine (fmap2 (uncurry F) _ $@ _).
-      * exact (Id a $o Id a, g $o f).
-      * exact ((cat_idl _)^$, Id _).
-      * exact (fmap_comp (uncurry F) (a := (a, b)) (b := (a, b')) (c := (a, b''))
-          (Id a, f) (Id a, g)).
-  - intros b.
-    snrapply Build_Is1Functor.
-    + intros a a' f f' p.
-      refine (fmap2 (uncurry F) _).
-      exact (p, Id (Id b)).
-    + intros a.
-      exact (fmap_id (uncurry F) _).
-    + intros a a' a'' f g.
-      srefine (fmap2 (uncurry F) _ $@ _).
-      * exact (g $o f, Id b $o Id b).
-      * exact (Id _, (cat_idr _)^$).
-      * exact (fmap_comp (uncurry F) (a := (a, b)) (b := (a', b)) (c := (a'', b))
-          (f, Id b) (g, Id b)).
+  - exact (is1functor_functor_uncurried01 (uncurry F)).
+  - exact (is1functor_functor_uncurried10 (uncurry F)).
   - intros a0 a1 f b0 b1 g.
     refine (fmap2 (uncurry F) _^$ $@ fmap_comp (uncurry F)
       (a := (a0, b0)) (b := (a1, b0)) (c := (a1, b1)) (f, Id b0) (Id a1, g)).
@@ -157,8 +125,7 @@ Proof.
   - exact _.
   - intros a0 a1 f b0 b1 g.
     exact (bifunctor_coh a0 a1 f b0 b1 g)^$.
-  - intros a0 a1 f b0 b1 g.
-    reflexivity.
+  - reflexivity.
 Defined.
 
 (** ** Bifunctor lemmas *)

From 10bcb54862236dec5004a7301e6278fd792454a5 Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Tue, 7 May 2024 17:38:30 +0100
Subject: [PATCH 08/10] typo

Signed-off-by: Ali Caglayan <alizter@gmail.com>
---
 theories/WildCat/Bifunctor.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/WildCat/Bifunctor.v b/theories/WildCat/Bifunctor.v
index 7d00d13a750..29564bfaa23 100644
--- a/theories/WildCat/Bifunctor.v
+++ b/theories/WildCat/Bifunctor.v
@@ -14,7 +14,7 @@ Class Is0Bifunctor {A B C : Type}
   is0functor10_bifunctor :: forall b, Is0Functor (flip F b);
 }.
 
-(** We provide two alternate constructors, allow the user to provide just the first field or the last two fields. *)
+(** We provide two alternate constructors, allowing the user to provide just the first field or the last two fields. *)
 Definition Build_Is0Bifunctor' {A B C : Type}
   `{Is01Cat A, Is01Cat B, IsGraph C} (F : A -> B -> C)
   `{!Is0Functor (uncurry F)}

From 01daaf6d8b2f5f6bebb2ecb34b5dd4d7db88620d Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Tue, 7 May 2024 23:03:21 +0100
Subject: [PATCH 09/10] abstract out fmap_pair in Prod.v

Signed-off-by: Ali Caglayan <alizter@gmail.com>
---
 theories/WildCat/Bifunctor.v | 36 ++++++++++++------------------------
 theories/WildCat/Prod.v      | 24 ++++++++++++++++++++++++
 2 files changed, 36 insertions(+), 24 deletions(-)

diff --git a/theories/WildCat/Bifunctor.v b/theories/WildCat/Bifunctor.v
index 29564bfaa23..998fe9a2597 100644
--- a/theories/WildCat/Bifunctor.v
+++ b/theories/WildCat/Bifunctor.v
@@ -58,7 +58,7 @@ Definition fmap11 {A B C : Type} `{IsGraph A, IsGraph B, IsGraph 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 (uncurry F) (a := (a0, b0)) (b := (a1, b1)) (f, g).
+  := fmap_pair (uncurry F) f g.
 
 (** As with [Is0Bifunctor], we store redundant information.  In addition, we store the proofs that they are consistent with each other. *)
 Class Is1Bifunctor {A B C : Type}
@@ -92,13 +92,11 @@ Proof.
   - exact (is1functor_functor_uncurried01 (uncurry F)).
   - exact (is1functor_functor_uncurried10 (uncurry F)).
   - intros a0 a1 f b0 b1 g.
-    refine (fmap2 (uncurry F) _^$ $@ fmap_comp (uncurry F)
-      (a := (a0, b0)) (b := (a1, b0)) (c := (a1, b1)) (f, Id b0) (Id a1, g)).
-    exact (cat_idl _, cat_idr _).
+    refine (_^$ $@ fmap_pair_comp (uncurry F) f (Id b0) (Id a1) g).
+    exact (fmap2_pair (uncurry F) (cat_idl _) (cat_idr _)).
   - intros a0 a1 f b0 b1 g.
-    refine (fmap2 (uncurry F) _^$ $@ fmap_comp (uncurry F)
-      (a := (a0, b0)) (b := (a0, b1)) (c := (a1, b1)) (Id a0, g) (f, Id b1)).
-    exact (cat_idr _, cat_idl _).
+    refine (_^$ $@ fmap_pair_comp (uncurry F) (Id a0) g f (Id b1)).
+    exact (fmap2_pair (uncurry F) (cat_idr _) (cat_idl _)).
 Defined.
 
 Definition Build_Is1Bifunctor'' {A B C : Type}
@@ -149,11 +147,8 @@ Definition fmap02 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
 Definition fmap12 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
   (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
   {a0 a1 : A} (f : a0 $-> a1) {b0 b1 : B} {g g' : b0 $-> b1} (q : g $== g')
-  : fmap11 F f g $== fmap11 F f g'.
-Proof.
-  refine (fmap2 (uncurry F) _).
-  exact (Id _, q).
-Defined.
+  : fmap11 F f g $== fmap11 F f g'
+  := fmap2_pair (uncurry F) (Id _) q.
 
 Definition fmap20 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
   (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
@@ -164,21 +159,15 @@ Definition fmap20 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
 Definition fmap21 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
   (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
   {a0 a1 : A} {f f' : a0 $-> a1} (p : f $== f') {b0 b1 : B} (g : b0 $-> b1)
-  : fmap11 F f g $== fmap11 F f' g.
-Proof.
-  refine (fmap2 (uncurry F) _).
-  exact (p, Id _).
-Defined.
+  : fmap11 F f g $== fmap11 F f' g
+  := fmap2_pair (uncurry F) p (Id _).
 
 Definition fmap22 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
   (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
   {a0 a1 : A} {f f' : a0 $-> a1} (p : f $== f')
   {b0 b1 : B} {g g' : b0 $-> b1} (q : g $== g')
-  : fmap11 F f g $== fmap11 F f' g'.
-Proof.
-  refine (fmap2 (uncurry F) _).
-  exact (p, q).
-Defined.
+  : fmap11 F f g $== fmap11 F f' g'
+  := fmap2_pair (uncurry F) p q.
 
 (** *** Identity preservation *)
 
@@ -230,8 +219,7 @@ Definition fmap11_comp {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
   {a0 a1 a2 : A} (g : a1 $-> a2) (f : a0 $-> a1)
   {b0 b1 b2 : B} (k : b1 $-> b2) (h : b0 $-> b1)
   : fmap11 F (g $o f) (k $o h) $== fmap11 F g k $o fmap11 F f h
-  := fmap_comp (uncurry F)
-    (a := (a0, b0)) (b := (a1, b1)) (c := (a2, b2)) (_, _) (_, _).
+  := fmap_pair_comp (uncurry F) _ _ _ _.
 
 (** *** Equivalence preservation *)
 
diff --git a/theories/WildCat/Prod.v b/theories/WildCat/Prod.v
index dfa66fbb4e8..8b5ddd17fa8 100644
--- a/theories/WildCat/Prod.v
+++ b/theories/WildCat/Prod.v
@@ -227,3 +227,27 @@ Definition fmap11_uncurry {A B C : Type} `{IsGraph A, IsGraph B, IsGraph C}
   {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).
+
+Definition fmap_pair {A B C : Type}  
+  `{IsGraph A, IsGraph B, IsGraph C}  
+  (F : A * B -> C) `{!Is0Functor F}  
+  {a0 a1 : A} (f : a0 $-> a1) {b0 b1 : B} (g : b0 $-> b1)  
+  : F (a0, b0) $-> F (a1, b1)  
+  := fmap (a:=(a0,b0)) (b:=(a1,b1)) F (f,g).  
+
+Definition fmap_pair_comp {A B C : Type}  
+  `{Is1Cat A, Is1Cat B, Is1Cat C}  
+  (F : A * B -> C) `{!Is0Functor F, !Is1Functor F}  
+  {a0 a1 a2 : A} {b0 b1 b2 : B}
+  (f : a0 $-> a1) (h : b0 $-> b1) (g : a1 $-> a2) (i : b1 $-> b2)  
+  : fmap_pair F (g $o f) (i $o h)
+    $== fmap_pair F g i $o fmap_pair F f h
+  := fmap_comp (a:=(a0,b0)) (b:=(a1,b1)) (c:=(a2,b2)) F (f,h) (g,i).
+
+Definition fmap2_pair {A B C : Type}
+  `{Is1Cat A, Is1Cat B, Is1Cat C}
+  (F : A * B -> C) `{!Is0Functor F, !Is1Functor F}
+  {a0 a1 : A} {f f' : a0 $-> a1} (p : f $== f')
+  {b0 b1 : B} {g g' : b0 $-> b1} (q : g $== g')
+  : fmap_pair F f g $== fmap_pair F f' g'
+  := fmap2 F (a:=(a0,b0)) (b:=(a1,b1)) (f:=(f,g)) (g:=(f',g')) (p,q).

From f235f5370410c09ee4dda788ad62894105bcba09 Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Tue, 7 May 2024 23:09:03 +0100
Subject: [PATCH 10/10] adjust spacing

Signed-off-by: Ali Caglayan <alizter@gmail.com>
---
 theories/WildCat/Prod.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/WildCat/Prod.v b/theories/WildCat/Prod.v
index 8b5ddd17fa8..8a4b08b23f5 100644
--- a/theories/WildCat/Prod.v
+++ b/theories/WildCat/Prod.v
@@ -233,7 +233,7 @@ Definition fmap_pair {A B C : Type}
   (F : A * B -> C) `{!Is0Functor F}  
   {a0 a1 : A} (f : a0 $-> a1) {b0 b1 : B} (g : b0 $-> b1)  
   : F (a0, b0) $-> F (a1, b1)  
-  := fmap (a:=(a0,b0)) (b:=(a1,b1)) F (f,g).  
+  := fmap (a := (a0, b0)) (b := (a1, b1)) F (f, g).  
 
 Definition fmap_pair_comp {A B C : Type}  
   `{Is1Cat A, Is1Cat B, Is1Cat C}  
@@ -242,7 +242,7 @@ Definition fmap_pair_comp {A B C : Type}
   (f : a0 $-> a1) (h : b0 $-> b1) (g : a1 $-> a2) (i : b1 $-> b2)  
   : fmap_pair F (g $o f) (i $o h)
     $== fmap_pair F g i $o fmap_pair F f h
-  := fmap_comp (a:=(a0,b0)) (b:=(a1,b1)) (c:=(a2,b2)) F (f,h) (g,i).
+  := fmap_comp (a := (a0, b0)) (b := (a1, b1)) (c := (a2, b2)) F (f, h) (g, i).
 
 Definition fmap2_pair {A B C : Type}
   `{Is1Cat A, Is1Cat B, Is1Cat C}
@@ -250,4 +250,4 @@ Definition fmap2_pair {A B C : Type}
   {a0 a1 : A} {f f' : a0 $-> a1} (p : f $== f')
   {b0 b1 : B} {g g' : b0 $-> b1} (q : g $== g')
   : fmap_pair F f g $== fmap_pair F f' g'
-  := fmap2 F (a:=(a0,b0)) (b:=(a1,b1)) (f:=(f,g)) (g:=(f',g')) (p,q).
+  := fmap2 F (a := (a0, b0)) (b := (a1, b1)) (f := (f, g)) (g := (f' ,g')) (p, q).