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 ae54b254dd1..317a9f4cd35 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 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.
@@ -121,16 +121,16 @@ 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.
-  exact (bifunctor_isbifunctor (Ext : AbGroup^op -> AbGroup -> pType)).
+  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. *)
diff --git a/theories/Homotopy/Join/Core.v b/theories/Homotopy/Join/Core.v
index 1dc3b578789..50b7d943cd5 100644
--- a/theories/Homotopy/Join/Core.v
+++ b/theories/Homotopy/Join/Core.v
@@ -562,7 +562,8 @@ Section FunctorJoin.
 
   Global Instance is0bifunctor_join : Is0Bifunctor Join.
   Proof.
-    rapply Build_Is0Bifunctor'.
+    snrapply Build_Is0Bifunctor'.
+    1,2: exact _.
     apply Build_Is0Functor.
     intros A B [f g].
     exact (functor_join f g).
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..cc26c8374cf 100644
--- a/theories/Homotopy/Smash.v
+++ b/theories/Homotopy/Smash.v
@@ -353,7 +353,8 @@ Defined.
 
 Global Instance is0bifunctor_smash : Is0Bifunctor Smash.
 Proof.
-  rapply Build_Is0Bifunctor'.
+  snrapply Build_Is0Bifunctor'.
+  1,2: exact _.
   nrapply Build_Is0Functor.
   intros [X Y] [A B] [f g].
   exact (functor_smash f g).
diff --git a/theories/WildCat/Bifunctor.v b/theories/WildCat/Bifunctor.v
index dd6c4667ccc..998fe9a2597 100644
--- a/theories/WildCat/Bifunctor.v
+++ b/theories/WildCat/Bifunctor.v
@@ -1,65 +1,44 @@
 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 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
+(** 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);
+  is0functor01_bifunctor :: forall a, Is0Functor (F a);
+  is0functor10_bifunctor :: forall b, Is0Functor (flip F b);
 }.
 
-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)).
+(** 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)}
+  : Is0Bifunctor F.
 Proof.
-  rapply Build_Is0Bifunctor.
+  snrapply Build_Is0Bifunctor.
+  - exact _.
+  - exact (is0functor_functor_uncurried01 (uncurry F)).
+  - exact (is0functor_functor_uncurried10 (uncurry F)).
 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)).
+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.
-  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)^$).
+  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.
 
-(** 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).
-
-(** ** Bifunctor lemmas *)
-
 (** *** 1-functorial action *)
 
 (** [fmap] in the first argument. *)
@@ -74,44 +53,88 @@ 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. *)
-Definition fmap11 {A B C : Type} `{IsGraph A, IsGraph B, Is01Cat C}
+(** [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
-  := fmap01 F _ g $o fmap10 F f _.
+  := fmap_pair (uncurry F) f g.
 
-(** [fmap11] but with the other choice. *)
-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
-  := fmap10 F f _ $o fmap01 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} := {
 
-(** *** Coherence *)
+  is1functor_bifunctor_uncurried :: Is1Functor (uncurry F);
+  is1functor01_bifunctor :: forall a, Is1Functor (F a);
+  is1functor10_bifunctor :: forall b, Is1Functor (flip F b);
 
-(** 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}
-  {a0 a1 : A} (f : a0 $-> a1) {b0 b1 : B} (g : b0 $-> b1)
-  : fmap11 F f g $== fmap11' F f g.
+  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.
+
+(** 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)}
+  : Is1Bifunctor (Is0Bifunctor := Build_Is0Bifunctor' F) F.
 Proof.
-  rapply bifunctor_isbifunctor.
+  snrapply Build_Is1Bifunctor.
+  - exact _.
+  - exact (is1functor_functor_uncurried01 (uncurry F)).
+  - exact (is1functor_functor_uncurried10 (uncurry F)).
+  - intros a0 a1 f b0 b1 g.
+    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 (_^$ $@ fmap_pair_comp (uncurry F) (Id a0) g f (Id b1)).
+    exact (fmap2_pair (uncurry F) (cat_idr _) (cat_idl _)).
 Defined.
 
-(** [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 _.
+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)^$.
+  - reflexivity.
+Defined.
 
-(** [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 _.
+(** ** Bifunctor lemmas *)
+
+(** *** Coherence *)
+
+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 _ _ _.
 
 (** 2-functorial action *)
 
@@ -125,7 +148,7 @@ 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 _.
+  := 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}
@@ -137,14 +160,14 @@ 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 _.
+  := 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'
-  := fmap20 F p b0 $@@ fmap02 F a1 q.
+  := fmap2_pair (uncurry F) p q.
 
 (** *** Identity preservation *)
 
@@ -160,11 +183,22 @@ 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).
+
+(** [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 *)
 
@@ -184,13 +218,8 @@ 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_pair_comp (uncurry F) _ _ _ _.
 
 (** *** Equivalence preservation *)
 
@@ -210,7 +239,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,54 +259,33 @@ 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 _.
+  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) `{Is1Bifunctor A B C F} : Is1Bifunctor (flip F).
+(F : A -> B -> C) `{H : Is1Bifunctor A B C F}
+  : Is1Bifunctor (flip F).
 Proof.
   snrapply Build_Is1Bifunctor.
-  1,2: exact _.
-  intros a0 a1 f b0 b1 g.
-  symmetry.
-  rapply bifunctor_isbifunctor.
+  - 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.
 
@@ -290,10 +298,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 Build_Is0Bifunctor.
-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}
@@ -301,99 +307,88 @@ 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).
-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).
-Proof.
-  rapply Build_Is0Bifunctor.
-  intros c.
-  change (Is0Functor (flip F c o G)).
-  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)).
-Proof.
-  rapply Build_Is0Bifunctor.
-  intros a.
-  change (Is0Functor (flip F (G a))).
-  exact _.
+  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 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).
+Global Instance is0bifunctor_precompose {A B C D E : Type}
+  `{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)).
 Proof.
-  nrapply Build_Is1Bifunctor.
+  snrapply Build_Is0Bifunctor.
+  - change (Is0Functor (uncurry F o functor_prod G K)).
+    exact _.
   - exact _.
-  - unfold flip.
-    change (forall c, Is1Functor (flip F c o G)).
+  - intros e.
+    change (Is0Functor (flip F (K e) 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)).
+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.
-  nrapply Build_Is1Bifunctor.
+  snrapply Build_Is1Bifunctor.
+  - change (Is1Functor (uncurry F o functor_prod G K)).
+    exact _.
   - exact _.
-  - unfold flip.
-    change (forall a, Is1Functor (fun b => F b (G a))).
+  - intros e.
+    change (Is1Functor (flip F (K e) o G)).
     exact _.
-  - intros a a' f b b' g.
-    simpl.
-    apply (bifunctor_isbifunctor F).
+  - 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}
   (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.
-  rapply is0functor_uncurry_bifunctor.
+  exact _.
 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.
-  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}
+  `{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)))
@@ -401,6 +396,9 @@ Global Instance is1natural_uncurry {A B C : Type}
 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.
+  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 2ead4600768..38abf2de889 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,22 @@ 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).
+    refine ((_ $@L (fmap10_is_fmap11 _ _ _)^$) $@ _ $@ (fmap01_is_fmap11 _ _ _ $@R _)).
+    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).
+    refine ((_ $@L (fmap01_is_fmap11 _ _ _)^$) $@ _ $@ (fmap10_is_fmap11 _ _ _ $@R _)).
+    exact (is1natural_braiding_uncurried (a, b) (a, c) (Id _ , g)).
   Defined.
 
 End SymmetricBraid.
@@ -632,15 +625,12 @@ 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.
+      nrapply hconcatL.
+      2: nrapply hconcatR.
+      1,3: symmetry; rapply fmap01_is_fmap11.
       (** 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.
@@ -660,11 +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).
-        nrapply vconcatL.
-        1: symmetry; rapply fmap01_is_fmap11.
-        nrapply vconcatR.
-        2: symmetry; rapply fmap10_is_fmap11.
-        rapply braid_nat.
+        rapply braid_nat_r.
     - intros a.
       rapply compose_catie'.
       rapply catie_braid.
diff --git a/theories/WildCat/Prod.v b/theories/WildCat/Prod.v
index dfa66fbb4e8..8a4b08b23f5 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).
diff --git a/theories/WildCat/Products.v b/theories/WildCat/Products.v
index c051c5128c1..002ef175a61 100644
--- a/theories/WildCat/Products.v
+++ b/theories/WildCat/Products.v
@@ -440,44 +440,24 @@ 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_Is0Bifunctor'.
+  1,2: exact _.
+  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_Is1Bifunctor'.
+  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 +482,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 +538,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 +553,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 +616,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 +703,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..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 _)
-  := is0bifunctor_functor_uncurried _.
+  : 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 _)
-  := is1bifunctor_functor_uncurried _.
+  : 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))
-  := is0bifunctor_functor_uncurried _.
+  : 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))
-  := is1bifunctor_functor_uncurried _.
+  : 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).