diff --git a/theories/Algebra/Categorical/MonoidObject.v b/theories/Algebra/Categorical/MonoidObject.v
new file mode 100644
index 0000000000..4ba1d54286
--- /dev/null
+++ b/theories/Algebra/Categorical/MonoidObject.v
@@ -0,0 +1,199 @@
+Require Import Basics.Overture Basics.Tactics.
+Require Import WildCat.Core WildCat.Equiv WildCat.Monoidal WildCat.Bifunctor
+  WildCat.NatTrans WildCat.Opposite WildCat.Products.
+Require Import abstract_algebra.
+
+(** * Monoids and Comonoids *)
+
+(** Here we define a monoid internal to a monoidal category. Note that we don't actually need the full monoidal structure so we assume only the parts we need. This allows us to keep the definitions general between various flavours of monoidal category.
+
+Many algebraic theories such as groups and rings may also be internalized, however these specifically require a cartesian monoidal structure. The theory of monoids however has no such requirement and can therefore be developed in much greater generality. This can be used to define a range of objects such as R-algebras, H-spaces, Hopf algebras and more. *)
+
+(** * Monoid objects *)
+
+Section MonoidObject.
+  Context {A : Type} {tensor : A -> A -> A} {unit : A}
+    `{HasEquivs A, !Is0Bifunctor tensor, !Is1Bifunctor tensor}
+    `{!Associator tensor, !LeftUnitor tensor unit, !RightUnitor tensor unit}.
+
+  (** An object [x] of [A] is a monoid object if it comes with the following data: *)
+  Class IsMonoidObject (x : A) := {
+    (** A multiplication map from the tensor product of [x] with itself to [x]. *)
+    mo_mult : tensor x x $-> x;
+    (** A unit of the multplication. *)
+    mo_unit : unit $-> x;
+    (** The multiplication map is associative. *)
+    mo_assoc : mo_mult $o fmap10 tensor mo_mult x $o associator x x x
+        $== mo_mult $o fmap01 tensor x mo_mult;
+    (** The multiplication map is left unital. *)
+    mo_left_unit : mo_mult $o fmap10 tensor mo_unit x $== left_unitor x;
+    (** The multiplication map is right unital. *)
+    mo_right_unit : mo_mult $o fmap01 tensor x mo_unit $== right_unitor x;
+  }.
+
+  Context `{!Braiding tensor}.
+
+  (** An object [x] of [A] is a commutative monoid object if: *)
+  Class IsCommutativeMonoidObject (x : A) := {
+    (** It is a monoid object. *)
+    cmo_mo :: IsMonoidObject x;
+    (** The multiplication map is commutative. *)
+    cmo_comm : mo_mult $o braid x x $== mo_mult;
+  }.
+
+End MonoidObject.
+
+Arguments IsMonoidObject {A} tensor unit {_ _ _ _ _ _ _ _ _ _} x.
+Arguments IsCommutativeMonoidObject {A} tensor unit {_ _ _ _ _ _ _ _ _ _ _} x.
+
+Section ComonoidObject.
+  Context {A : Type} (tensor : A -> A -> A) (unit : A)
+    `{HasEquivs A, !Is0Bifunctor tensor, !Is1Bifunctor tensor}
+    `{!Associator tensor, !LeftUnitor tensor unit, !RightUnitor tensor unit}.
+
+  (** A comonoid object is a monoid object in the opposite category. *)
+  Class IsComonoidObject (x : A)
+    := ismonoid_comonoid_op :: IsMonoidObject (A:=A^op) tensor unit x.
+
+  (** We can build comonoid objects from the following data: *)
+  Definition Build_IsComonoidObject (x : A)
+    (** A comultplication map. *)
+    (co_comult : x $-> tensor x x)
+    (** A counit. *)
+    (co_counit : x $-> unit)
+    (** The comultiplication is coassociative. *)
+    (co_coassoc : associator x x x $o fmap01 tensor x co_comult $o co_comult
+        $== fmap10 tensor co_comult x $o co_comult)
+    (** The comultiplication is left counital. *)
+    (co_left_counit : left_unitor x $o fmap10 tensor co_counit x $o co_comult $== Id x)
+    (** The comultiplication is right counital. *)
+    (co_right_counit : right_unitor x $o fmap01 tensor x co_counit $o co_comult $== Id x)
+    : IsComonoidObject x.
+  Proof.
+    snrapply Build_IsMonoidObject.
+    - exact co_comult.
+    - exact co_counit.
+    - nrapply cate_moveR_eV.
+      symmetry.
+      nrefine (cat_assoc _ _ _ $@ _).
+      rapply co_coassoc.
+    - simpl; nrefine (_ $@ cat_idr _).
+      nrapply cate_moveL_Ve.
+      nrefine (cat_assoc_opp _ _ _ $@ _).
+      exact co_left_counit.
+    - simpl; nrefine (_ $@ cat_idr _).
+      nrapply cate_moveL_Ve.
+      nrefine (cat_assoc_opp _ _ _ $@ _).
+      exact co_right_counit.
+  Defined.
+
+  (** Comultiplication *)
+  Definition co_comult {x : A} `{!IsComonoidObject x} : x $-> tensor x x
+   := mo_mult (A:=A^op) (tensor:=tensor) (unit:=unit) (x:=x).
+
+  (** Counit *)
+  Definition co_counit {x : A} `{!IsComonoidObject x} : x $-> unit
+    := mo_unit (A:=A^op) (tensor:=tensor) (unit:=unit) (x:=x).
+
+  Context `{!Braiding tensor}.
+
+  (** A cocommutative comonoid objects is a commutative monoid object in the opposite category. *)
+  Class IsCocommutativeComonoidObject (x : A)
+    := iscommuatativemonoid_cocomutativemonoid_op
+      :: IsCommutativeMonoidObject (A:=A^op) tensor unit x.
+
+  (** We can build cocommutative comonoid objects from the following data: *)
+  Definition Build_IsCocommutativeComonoidObject (x : A)
+    (** A comonoid. *)
+    `{!IsComonoidObject x}
+    (** Together with a proof of cocommutativity. *)
+    (cco_cocomm : braid x x $o co_comult $== co_comult)
+    : IsCocommutativeComonoidObject x.
+  Proof.
+    snrapply Build_IsCommutativeMonoidObject.
+    - exact _.
+    - exact cco_cocomm.
+  Defined.
+
+End ComonoidObject.
+
+(** ** Monoid enrichment *)
+
+(** A hom [x $-> y] in a cartesian category where [y] is a monoid object has the structure of a monoid. Equivalently, a hom [x $-> y] in a cartesian category where [x] is a comonoid object has the structure of a monoid. *)
+
+Section MonoidEnriched.
+  Context {A : Type} `{HasEquivs A} `{!HasBinaryProducts A}
+    (unit : A) `{!IsTerminal unit} {x y : A}
+    `{!HasMorExt A} `{forall x y, IsHSet (x $-> y)}.
+
+  Section Monoid.
+    Context `{!IsMonoidObject _ _ y}.
+
+    Local Instance sgop_hom : SgOp (x $-> y)
+      := fun f g => mo_mult $o cat_binprod_corec f g.
+
+    Local Instance monunit_hom : MonUnit (x $-> y) := mo_unit $o mor_terminal _ _.
+
+    Local Instance associative_hom : Associative sgop_hom.
+    Proof.
+      intros f g h.
+      unfold sgop_hom.
+      rapply path_hom.
+      refine ((_ $@L cat_binprod_fmap01_corec _ _ _)^$ $@ _).
+      nrefine (cat_assoc_opp _ _ _ $@ _).
+      refine ((mo_assoc $@R _)^$ $@ _).
+      nrefine (_ $@ (_ $@L cat_binprod_fmap10_corec _ _ _)).
+      refine (cat_assoc _ _ _ $@ (_ $@L _) $@ cat_assoc _ _ _).
+      nrapply cat_binprod_associator_corec.
+    Defined.
+
+    Local Instance leftidentity_hom : LeftIdentity sgop_hom mon_unit.
+    Proof.
+      intros f.
+      unfold sgop_hom, mon_unit.
+      rapply path_hom.
+      refine ((_ $@L (cat_binprod_fmap10_corec _ _ _)^$) $@ cat_assoc_opp _ _ _ $@ _).
+      nrefine (((mo_left_unit $@ _) $@R _) $@ _).
+      1: nrapply cate_buildequiv_fun.
+      unfold trans_nattrans.
+      nrefine ((((_ $@R _) $@ _) $@R _) $@ _).
+      1: nrapply cate_buildequiv_fun.
+      1: nrapply cat_binprod_beta_pr1.
+      nrapply cat_binprod_beta_pr2.
+    Defined.
+
+    Local Instance rightidentity_hom : RightIdentity sgop_hom mon_unit.
+    Proof.
+      intros f.
+      unfold sgop_hom, mon_unit.
+      rapply path_hom.
+      refine ((_ $@L (cat_binprod_fmap01_corec _ _ _)^$) $@ cat_assoc_opp _ _ _ $@ _).
+      nrefine (((mo_right_unit $@ _) $@R _) $@ _).
+      1: nrapply cate_buildequiv_fun.
+      nrapply cat_binprod_beta_pr1.
+    Defined.
+
+    Local Instance issemigroup_hom : IsSemiGroup (x $-> y) := {}.
+    Local Instance ismonoid_hom : IsMonoid (x $-> y) := {}.
+
+  End Monoid.
+
+  Context `{!IsCommutativeMonoidObject _ _ y}.
+  Local Existing Instances sgop_hom monunit_hom ismonoid_hom.
+
+  Local Instance commutative_hom : Commutative sgop_hom.
+  Proof.
+    intros f g.
+    unfold sgop_hom.
+    rapply path_hom.
+    refine ((_ $@L _^$) $@ cat_assoc_opp _ _ _ $@ (cmo_comm $@R _)).
+    nrapply cat_binprod_swap_corec. 
+  Defined.
+
+  Local Instance iscommutativemonoid_hom : IsCommutativeMonoid (x $-> y) := {}.
+
+End MonoidEnriched.
+
+
+
+
diff --git a/theories/WildCat/Adjoint.v b/theories/WildCat/Adjoint.v
index 68d865e06e..ef4ef9965f 100644
--- a/theories/WildCat/Adjoint.v
+++ b/theories/WildCat/Adjoint.v
@@ -388,7 +388,7 @@ Proof.
   snrapply Build_Adjunction_natequiv_nat_right.
   { intros y.
     refine (natequiv_compose (natequiv_adjunction_l adj _) _).
-    rapply (natequiv_postwhisker _ (natequiv_op _ _ e)). }
+    rapply (natequiv_postwhisker _ (natequiv_op e)). }
   intros x.
   rapply is1natural_comp.
 Defined.
diff --git a/theories/WildCat/Bifunctor.v b/theories/WildCat/Bifunctor.v
index 65d56eaec8..f26347dfb3 100644
--- a/theories/WildCat/Bifunctor.v
+++ b/theories/WildCat/Bifunctor.v
@@ -1,6 +1,7 @@
 Require Import Basics.Overture Basics.Tactics.
 Require Import Types.Forall Types.Prod.
-Require Import WildCat.Core WildCat.Prod WildCat.Equiv WildCat.NatTrans WildCat.Square.
+Require Import WildCat.Core WildCat.Prod WildCat.Equiv WildCat.NatTrans
+  WildCat.Square WildCat.Opposite.
 
 (** * Bifunctors between WildCats *)
 
@@ -14,6 +15,11 @@ Class Is0Bifunctor {A B C : Type}
   is0functor10_bifunctor :: forall b, Is0Functor (flip F b);
 }.
 
+Arguments Is0Bifunctor {A B C _ _ _} F.
+Arguments is0functor_bifunctor_uncurried {A B C _ _ _} F {_}.
+Arguments is0functor01_bifunctor {A B C _ _ _} F {_} a : rename.
+Arguments is0functor10_bifunctor {A B C _ _ _} F {_} b : rename.
+
 (** 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)
@@ -32,7 +38,7 @@ Definition Build_Is0Bifunctor'' {A B C : Type}
   : Is0Bifunctor F.
 Proof.
   (* The first condition follows from [is0functor_prod_is0functor]. *)
-  rapply Build_Is0Bifunctor.
+  nrapply Build_Is0Bifunctor; exact _.
 Defined.
 
 (** *** 1-functorial action *)
@@ -72,6 +78,9 @@ Class Is1Bifunctor {A B C : Type}
 
 Arguments Is1Bifunctor {A B C _ _ _ _ _ _ _ _ _ _ _ _} F {Is0Bifunctor} : rename.
 Arguments Build_Is1Bifunctor {A B C _ _ _ _ _ _ _ _ _ _ _ _} F {_} _ _ _ _ _.
+Arguments is1functor_bifunctor_uncurried {A B C _ _ _ _ _ _ _ _ _ _ _ _} F {_ _}.
+Arguments is1functor01_bifunctor {A B C _ _ _ _ _ _ _ _ _ _ _ _} F {_ _} a : rename.
+Arguments is1functor10_bifunctor {A B C _ _ _ _ _ _ _ _ _ _ _ _} F {_ _} b : rename.
 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
@@ -285,14 +294,14 @@ 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))
+  : Is0Bifunctor (fun a b => G (F a b)) | 10
   := {}.
 
 Global Instance is1bifunctor_postcompose {A B C D : Type}
   `{Is1Cat A, Is1Cat B, Is1Cat C, Is1Cat D}
   (F : A -> B -> C) (G : C -> D) `{!Is0Functor G, !Is1Functor G}
   `{!Is0Bifunctor F} {bf : Is1Bifunctor F}
-  : Is1Bifunctor (fun a b => G (F a b)).
+  : Is1Bifunctor (fun a b => G (F a b)) | 10.
 Proof.
   snrapply Build_Is1Bifunctor.
   1-3: exact _.
@@ -306,7 +315,7 @@ 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)).
+  : Is0Bifunctor (fun a b => F (G a) (K b)) | 10.
 Proof.
   snrapply Build_Is0Bifunctor.
   - change (Is0Functor (uncurry F o functor_prod G K)).
@@ -322,7 +331,7 @@ Global Instance is1bifunctor_precompose {A B C D E : Type}
   (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)).
+  : Is1Bifunctor (fun a b => F (G a) (K b)) | 10.
 Proof.
   snrapply Build_Is1Bifunctor.
   - change (Is1Functor (uncurry F o functor_prod G K)).
@@ -372,10 +381,8 @@ Definition fmap11_square {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
 (** 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}
   `{Is1Cat A, Is1Cat B, Is1Cat C}
-  (F : A -> B -> C)
-  `{!Is0Bifunctor F, !Is1Bifunctor F}
-  (G : A -> B -> C)
-  `{!Is0Bifunctor G, !Is1Bifunctor G}
+  (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
+  (G : A -> B -> C) `{!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)))
@@ -389,3 +396,63 @@ Proof.
   2: rapply (fmap11_is_fmap01_fmap10 G).
   exact (hconcat (nat_l _ _ _ f) (nat_r _ _ _ f')).
 Defined.
+
+(** Flipping a natural transformation between bifunctors. *)
+Definition nattrans_flip {A B C : Type}
+  `{Is1Cat A, Is1Cat B, Is1Cat C}
+  {F : A -> B -> C} `{!Is0Bifunctor F, !Is1Bifunctor F}
+  {G : A -> B -> C} `{!Is0Bifunctor G, !Is1Bifunctor G}
+  : NatTrans (uncurry F) (uncurry G)
+    -> NatTrans (uncurry (flip F)) (uncurry (flip G)).
+Proof.
+  intros [alpha nat].
+  snrapply Build_NatTrans.
+  - exact (alpha o equiv_prod_symm _ _).
+  - intros [b a] [b' a'] [g f].
+    exact (nat (a, b) (a', b') (f, g)).
+Defined.
+
+(** ** Opposite Bifunctors *)
+
+(** There are a few more combinations we can do for this, such as profunctors, but we will leave those for later. *)
+
+Global Instance is0bifunctor_op A B C (F : A -> B -> C) `{Is0Bifunctor A B C F}
+  : Is0Bifunctor (F : A^op -> B^op -> C^op).
+Proof.
+  snrapply Build_Is0Bifunctor.
+  - exact (is0functor_op _ _ (uncurry F)).
+  - intros a.
+    nrapply is0functor_op.
+    exact (is0functor01_bifunctor F a).
+  - intros b.
+    nrapply is0functor_op.
+    exact (is0functor10_bifunctor F b).
+Defined.
+
+Global Instance is1bifunctor_op A B C (F : A -> B -> C) `{Is1Bifunctor A B C F}
+  : Is1Bifunctor (F : A^op -> B^op -> C^op).
+Proof.
+  snrapply Build_Is1Bifunctor.
+  - exact (is1functor_op _ _ (uncurry F)).
+  - intros a.
+    nrapply is1functor_op.
+    exact (is1functor01_bifunctor F a).
+  - intros b.
+    nrapply is1functor_op.
+    exact (is1functor10_bifunctor F b).
+  - intros a0 a1 f b0 b1 g; cbn in f, g.
+    exact (fmap11_is_fmap10_fmap01 F f g).
+  - intros a0 a1 f b0 b1 g; cbn in f, g.
+    exact (fmap11_is_fmap01_fmap10 F f g).
+Defined.
+
+Global Instance is0bifunctor_op' A B C (F : A^op -> B^op -> C^op)
+  `{IsGraph A, IsGraph B, IsGraph C, Fop : !Is0Bifunctor (F : A^op -> B^op -> C^op)}
+  : Is0Bifunctor (F : A -> B -> C)
+  := is0bifunctor_op A^op B^op C^op F.
+
+Global Instance is1bifunctor_op' A B C (F : A^op -> B^op -> C^op)
+  `{Is1Cat A, Is1Cat B, Is1Cat C,
+    !Is0Bifunctor (F : A^op -> B^op -> C^op), !Is1Bifunctor (F : A^op -> B^op -> C^op)}
+  : Is1Bifunctor (F : A -> B -> C)
+  := is1bifunctor_op A^op B^op C^op F.
diff --git a/theories/WildCat/Equiv.v b/theories/WildCat/Equiv.v
index 116b0b0e3b..aafc568430 100644
--- a/theories/WildCat/Equiv.v
+++ b/theories/WildCat/Equiv.v
@@ -413,6 +413,13 @@ Proof.
   apply cate_inv_adjointify.
 Defined.
 
+Definition cate_inv_compose' {A} `{HasEquivs A} {a b c : A} (e : a $<~> b) (f : b $<~> c)
+  : cate_fun (f $oE e)^-1$ $== e^-1$ $o f^-1$.
+Proof.
+  nrefine (_ $@ cate_buildequiv_fun _).
+  nrapply cate_inv_compose.
+Defined.
+
 Definition cate_inv_V {A} `{HasEquivs A} {a b : A} (e : a $<~> b)
   : cate_fun (e^-1$)^-1$ $== cate_fun e.
 Proof.
diff --git a/theories/WildCat/Monoidal.v b/theories/WildCat/Monoidal.v
index 38abf2de88..9eea53cfdf 100644
--- a/theories/WildCat/Monoidal.v
+++ b/theories/WildCat/Monoidal.v
@@ -1,6 +1,6 @@
 Require Import Basics.Overture Basics.Tactics Types.Forall.
 Require Import WildCat.Core WildCat.Bifunctor WildCat.Prod WildCat.Equiv.
-Require Import WildCat.NatTrans WildCat.Square.
+Require Import WildCat.NatTrans WildCat.Square WildCat.Opposite.
 
 (** * Monoidal Categories *)
 
@@ -12,21 +12,33 @@ Require Import WildCat.NatTrans WildCat.Square.
 
 (** *** Associators *)
 
-(** A natural equivalence witnessing the associativity of a bifunctor. *)
 Class Associator {A : Type} `{HasEquivs A}
-  (F : A -> A -> A) `{!Is0Bifunctor F, !Is1Bifunctor F} := {
-  (** An isomorphism [associator] witnessing associativity of [F]. *)
-  associator a b c : F a (F b c) $<~> F (F a b) c;
-
-  (** The [associator] is a natural isomorphism. *)
-  is1natural_associator_uncurried
-    :: Is1Natural
-        (fun '(a, b, c) => F a (F b c))
-        (fun '(a, b, c) => F (F a b) c)
-        (fun '(a, b, c) => associator a b c);
-}.
+  (F : A -> A -> A) `{!Is0Bifunctor F, !Is1Bifunctor F}
+  := associator_uncurried
+    : NatEquiv (fun '(a, b, c) => F a (F b c)) (fun '(a, b, c) => F (F a b) c).
+
+Arguments associator_uncurried {A _ _ _ _ _ F _ _ _}.
+
+Definition associator {A : Type} `{HasEquivs A} {F : A -> A -> A}
+  `{!Is0Bifunctor F, !Is1Bifunctor F, !Associator F}
+  : forall a b c, F a (F b c) $<~> F (F a b) c
+  := fun a b c => associator_uncurried (a, b, c).
 Coercion associator : Associator >-> Funclass.
-Arguments associator {A _ _ _ _ _ F _ _ _} a b c.
+
+Definition Build_Associator {A : Type} `{HasEquivs A} (F : A -> A -> A)
+  `{!Is0Bifunctor F, !Is1Bifunctor F}
+  (associator : forall a b c, F a (F b c) $<~> F (F a b) c)
+  (isnat_assoc : Is1Natural
+    (fun '(a, b, c) => F a (F b c))
+    (fun '(a, b, c) => F (F a b) c)
+    (fun '(a, b, c) => associator a b c))
+  : Associator F.
+Proof.
+  snrapply Build_NatEquiv.
+  - intros [[a b] c].
+    exact (associator a b c).
+  - exact isnat_assoc.
+Defined. 
 
 (** *** Unitors *)
 
@@ -69,18 +81,16 @@ Arguments pentagon_identity {A _ _ _ _ _} F {_ _ _}.
 (** *** Braiding *)
 
 Class Braiding {A : Type} `{Is1Cat A}
-  (F : A -> A -> A) `{!Is0Bifunctor F, !Is1Bifunctor F} := {
-  (** A morphism [braid] witnessing the symmetry of [F]. *)
-  braid a b : F a b $-> F b a;
-  (** The [braid] is a natural transformation. *)
-  is1natural_braiding_uncurried
-    : Is1Natural
-      (uncurry F)
-      (uncurry (flip F))
-      (fun '(a, b) => braid a b);
-}.
+  (F : A -> A -> A) `{!Is0Bifunctor F, !Is1Bifunctor F}
+  := braid_uncurried : NatTrans (uncurry F) (uncurry (flip F)).
+
+Arguments braid_uncurried {A _ _ _ _ F _ _ _}.
+    
+Definition braid {A : Type} `{Is1Cat A} {F : A -> A -> A}
+  `{!Is0Bifunctor F, !Is1Bifunctor F, !Braiding F}
+  : forall a b, F a b $-> F b a
+  := fun a b => braid_uncurried (a, b).
 Coercion braid : Braiding >-> Funclass.
-Arguments braid {A _ _ _ _ F _ _ _} a b.
 
 Class SymmetricBraiding {A : Type} `{Is1Cat A}
   (F : A -> A -> A) `{!Is0Bifunctor F, !Is1Bifunctor F} := {
@@ -150,7 +160,8 @@ Class IsSymmetricMonoidal (A : Type) `{HasEquivs A}
 (** *** Theory about [Associator] *)
 
 Section Associator.
-  Context {A : Type} {F : A -> A -> A} `{assoc : Associator A F, !HasEquivs A}.
+  Context {A : Type} `{HasEquivs A} {F : A -> A -> A}
+    `{!Is0Bifunctor F, !Is1Bifunctor F, assoc : !Associator F}.
 
   Local Definition associator_nat {x x' y y' z z'}
     (f : x $-> x') (g : y $-> y') (h : z $-> z')
@@ -191,8 +202,36 @@ Section Associator.
     - exact (fmap21 _ (fmap11_id _ _ _) _ $@ fmap01_is_fmap11 F _ _).
   Defined.
 
+  Global Instance associator_op : Associator (A:=A^op) F
+    := natequiv_inverse (natequiv_op assoc).
+
 End Associator.
 
+(** ** Theory about [LeftUnitor] and [RightUnitor] *)
+
+Section LeftUnitor.
+  Context {A : Type} `{HasEquivs A} {F : A -> A -> A} (unit : A)
+    `{!Is0Bifunctor F, !Is1Bifunctor F, !LeftUnitor F unit, !RightUnitor F unit}.
+
+  Global Instance left_unitor_op : LeftUnitor (A:=A^op) F unit
+    := natequiv_inverse (natequiv_op left_unitor).
+  
+  Global Instance right_unitor_op : RightUnitor (A:=A^op) F unit
+    := natequiv_inverse (natequiv_op right_unitor).
+
+End LeftUnitor.
+
+(** ** Theory about [Braiding] *)
+
+Section Braiding.
+  Context {A : Type} `{HasEquivs A} {F : A -> A -> A}
+    `{!Is0Bifunctor F, !Is1Bifunctor F, braid : !Braiding F}.
+  
+  Global Instance braiding_op : Braiding (A:=A^op) F
+    := (nattrans_op (nattrans_flip braid)).
+
+End Braiding.
+
 (** ** Theory about [SymmetricBraid] *)
 
 Section SymmetricBraid.
@@ -358,14 +397,14 @@ 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.
-    exact (is1natural_braiding_uncurried (a, b) (c, d) (f, g)).
+    exact (isnat braid_uncurried (a := (a, b)) (a' := (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 (fmap10_is_fmap11 _ _ _)^$) $@ _ $@ (fmap01_is_fmap11 _ _ _ $@R _)).
-    exact (is1natural_braiding_uncurried (a, c) (b, c) (f, Id _)).
+    exact (isnat braid_uncurried (a := (a, c)) (a' := (b, c)) (f, Id _)).
   Defined.
 
   (** This is just the inverse of above. *)
@@ -373,11 +412,43 @@ Section SymmetricBraid.
     : 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)).
+    exact (isnat braid_uncurried (a := (a, b)) (a' := (a, c)) (Id _ , g)).
+  Defined.
+  
+  Global Instance symmetricbraiding_op : SymmetricBraiding (A:=A^op) F.
+  Proof.
+    snrapply Build_SymmetricBraiding.
+    - exact _.
+    - intros a b.
+      rapply braid_braid.
   Defined.
 
 End SymmetricBraid.
 
+Global Instance ismonoidal_op {A : Type} (tensor : A -> A -> A) (unit : A)
+  `{IsMonoidal A tensor unit}
+  : IsMonoidal A^op tensor unit.
+Proof.
+  snrapply Build_IsMonoidal.
+  1-5: exact _.
+  - intros a b; unfold op in a, b; simpl.
+    refine (_^$ $@ _ $@ (_ $@L _)).
+    1,3: exact (emap_inv _ _ $@ cate_buildequiv_fun _).
+    nrefine (cate_inv2 _ $@ cate_inv_compose' _ _).
+    refine (cate_buildequiv_fun _ $@ _ $@ ((cate_buildequiv_fun _)^$ $@R _)
+      $@ (cate_buildequiv_fun _)^$).
+    rapply cat_tensor_triangle_identity.
+  - intros a b c d; unfold op in a, b, c, d; simpl.
+    refine (_ $@ ((_ $@L _) $@@ _)).
+    2,3: exact (emap_inv _ _ $@ cate_buildequiv_fun _).
+    refine ((cate_inv_compose' _ _)^$ $@ cate_inv2 _ $@ cate_inv_compose' _ _
+      $@ (_ $@L cate_inv_compose' _ _)). 
+    refine (cate_buildequiv_fun _ $@ _ $@ ((cate_buildequiv_fun _)^$ $@R _)
+      $@ (cate_buildequiv_fun _)^$).
+    refine (_ $@ (cate_buildequiv_fun _ $@@ (cate_buildequiv_fun _ $@R _))^$).
+    rapply cat_tensor_pentagon_identity.
+Defined.
+
 (** ** Building Symmetric Monoidal Categories *)
 
 (** The following construction is what we call the "twist construction". It is a way to build a symmetric monoidal category from simpler pieces than the axioms ask for.
diff --git a/theories/WildCat/NatTrans.v b/theories/WildCat/NatTrans.v
index 8ec964d6e8..07afbadea4 100644
--- a/theories/WildCat/NatTrans.v
+++ b/theories/WildCat/NatTrans.v
@@ -189,6 +189,17 @@ Proof.
   srapply isnat_tr.
 Defined.
 
+Definition nattrans_op {A B : Type} `{Is01Cat A} `{Is1Cat B}
+  {F G : A -> B} `{!Is0Functor F, !Is0Functor G}
+  : NatTrans F G
+  -> NatTrans (A:=A^op) (B:=B^op) (G : A^op -> B^op) (F : A^op -> B^op).
+Proof.
+  intros alpha.
+  snrapply Build_NatTrans.
+  - exact (transformation_op F G alpha).
+  - exact _.
+Defined.
+
 (** Natural equivalences *)
 
 Record NatEquiv {A B : Type} `{IsGraph A} `{HasEquivs B}
@@ -291,7 +302,7 @@ Proof.
 Defined.
 
 Lemma natequiv_op {A B : Type} `{Is01Cat A} `{HasEquivs B}
-  (F G : A -> B) `{!Is0Functor F, !Is0Functor G}
+  {F G : A -> B} `{!Is0Functor F, !Is0Functor G}
   : NatEquiv F G -> NatEquiv (G : A^op -> B^op) F.
 Proof.
   intros [a n].
diff --git a/theories/WildCat/Products.v b/theories/WildCat/Products.v
index 002ef175a6..c3010d0ab8 100644
--- a/theories/WildCat/Products.v
+++ b/theories/WildCat/Products.v
@@ -482,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. *)
@@ -556,6 +556,61 @@ Definition cat_pr2_fmap11_binprod {A : Type} `{HasBinaryProducts A}
   : cat_pr2 $o fmap11 (fun x y => cat_binprod x y) f g $== g $o cat_pr2
   := cat_binprod_beta_pr2 _ _.
 
+(** *** Diagonal *)
+
+(** Annoyingly this doesn't follow directly from the general diagonal since [fun b => if b then x else x] is not definitionally equal to [fun _ => x]. *)
+Definition cat_binprod_diag {A : Type}
+  `{HasEquivs A} (x : A) `{!BinaryProduct x x}
+  : x $-> cat_binprod x x.
+Proof.
+  snrapply cat_binprod_corec; exact (Id _).
+Defined.
+
+Definition cat_binprod_fmap01_corec {A : Type}
+  `{Is1Cat A, !HasBinaryProducts A} {w x y z : A}
+  (f : w $-> z) (g : x $-> y) (h : w $-> x)
+  : fmap01 (fun x y => cat_binprod x y) z g $o cat_binprod_corec f h
+    $== cat_binprod_corec f (g $o h).
+Proof.
+  snrapply cat_binprod_eta_pr.
+  - nrefine (cat_assoc_opp _ _ _ $@ _).
+    refine ((_ $@R _) $@ cat_assoc _ _ _ $@ cat_idl _ $@ _ $@ _^$).
+    1-3: rapply cat_binprod_beta_pr1.
+  - nrefine (cat_assoc_opp _ _ _ $@ _).
+    refine ((_ $@R _) $@ cat_assoc _ _ _ $@ (_ $@L _) $@ _^$).
+    1-3: rapply cat_binprod_beta_pr2.
+Defined.
+
+Definition cat_binprod_fmap10_corec {A : Type}
+  `{Is1Cat A, !HasBinaryProducts A} {w x y z : A}
+  (f : x $-> y) (g : w $-> x) (h : w $-> z)
+  : fmap10 (fun x y => cat_binprod x y) f z $o cat_binprod_corec g h
+    $== cat_binprod_corec (f $o g) h.
+Proof.
+  snrapply cat_binprod_eta_pr.
+  - refine (cat_assoc_opp _ _ _ $@ _).
+    refine ((_ $@R _) $@ cat_assoc _ _ _ $@ (_ $@L _) $@ _^$).
+    1-3: nrapply cat_binprod_beta_pr1.
+  - refine (cat_assoc_opp _ _ _ $@ _).
+    refine ((_ $@R _) $@ cat_assoc _ _ _ $@ cat_idl _ $@ _ $@ _^$).
+    1-3: nrapply cat_binprod_beta_pr2.
+Defined.
+
+Definition cat_binprod_fmap11_corec {A : Type}
+  `{Is1Cat A, !HasBinaryProducts A} {v w x y z : A}
+  (f : w $-> y) (g : x $-> z) (h : v $-> w) (i : v $-> x)
+  : fmap11 (fun x y => cat_binprod x y) f g $o cat_binprod_corec h i
+    $== cat_binprod_corec (f $o h) (g $o i).
+Proof.
+  snrapply cat_binprod_eta_pr.
+  - refine (cat_assoc_opp _ _ _ $@ _).
+    refine ((_ $@R _) $@ cat_assoc _ _ _ $@ (_ $@L _) $@ _^$).
+    1-3: nrapply cat_binprod_beta_pr1.
+  - nrefine (cat_assoc_opp _ _ _ $@ _).
+    refine ((_ $@R _) $@ cat_assoc _ _ _ $@ (_ $@L _) $@ _^$).
+    1-3: rapply cat_binprod_beta_pr2.
+Defined.
+
 (** *** Symmetry of binary products *)
 
 Section Symmetry.
@@ -586,35 +641,30 @@ Section Symmetry.
     all: nrapply cat_binprod_swap_cat_binprod_swap.
   Defined.
 
-  Definition cat_binprod_swap_nat {a b c d : A} (f : a $-> c) (g : b $-> d)
-    : cat_binprod_swap c d $o fmap11 (fun x y : A => cat_binprod x y) f g
-    $== fmap11 (fun x y : A => cat_binprod x y) g f $o cat_binprod_swap a b.
+  Definition cat_binprod_swap_corec {a b c : A} (f : a $-> b) (g : a $-> c)
+    : cat_binprod_swap b c $o cat_binprod_corec f g $== cat_binprod_corec g f.
   Proof.
     nrapply cat_binprod_eta_pr.
-    - nrefine (cat_assoc_opp _ _ _ $@ _).
-      nrefine ((cat_binprod_beta_pr1 _ _ $@R _) $@ _).
-      nrefine (cat_pr2_fmap11_binprod _ _ $@ _).
-      nrefine (_ $@ cat_assoc _ _ _).
-      refine (_ $@ (_^$ $@R _)).
-      2: nrapply cat_pr1_fmap11_binprod.
-      refine ((_ $@L _^$) $@ (cat_assoc _ _ _)^$).
-      nrapply cat_binprod_beta_pr1.
-    - refine ((cat_assoc _ _ _)^$ $@ _).
-      nrefine ((cat_binprod_beta_pr2 _ _ $@R _) $@ _).
-      nrefine (cat_pr1_fmap11_binprod _ _ $@ _).
-      nrefine (_ $@ cat_assoc _ _ _).
-      refine (_ $@ (_^$ $@R _)).
-      2: nrapply cat_pr2_fmap11_binprod.
-      refine ((_ $@L _^$) $@ cat_assoc_opp _ _ _).
+    - refine (cat_assoc_opp _ _ _ $@ (_ $@R _) $@ (_ $@ _^$)).
+      1,3: nrapply cat_binprod_beta_pr1.
       nrapply cat_binprod_beta_pr2.
+    - refine (cat_assoc_opp _ _ _ $@ (_ $@R _) $@ (_ $@ _^$)).
+      1,3: nrapply cat_binprod_beta_pr2.
+      nrapply cat_binprod_beta_pr1.
   Defined.
 
+  Definition cat_binprod_swap_nat {a b c d : A} (f : a $-> c) (g : b $-> d)
+    : cat_binprod_swap c d $o fmap11 (fun x y : A => cat_binprod x y) f g
+    $== fmap11 (fun x y : A => cat_binprod x y) g f $o cat_binprod_swap a b
+    := cat_binprod_swap_corec _ _ $@ (cat_binprod_fmap11_corec _ _ _ _)^$.
+
   Local Instance symmetricbraiding_binprod
     : SymmetricBraiding (fun x y => cat_binprod x y).
   Proof.
     snrapply Build_SymmetricBraiding.
-    - snrapply Build_Braiding.
-      + exact cat_binprod_swap.
+    - snrapply Build_NatTrans.
+      + intros [x y].
+        exact (cat_binprod_swap x y).
       + intros [a b] [c d] [f g]; cbn in f, g.
         exact(cat_binprod_swap_nat f g).
     - exact cat_binprod_swap_cat_binprod_swap.
@@ -655,6 +705,25 @@ Section Associativity.
     nrefine ((_ $@L cat_binprod_beta_pr2 _ _) $@ _).
     nrapply cat_pr2_fmap01_binprod.
   Defined.
+  
+  Definition cat_binprod_twist_corec {w x y z : A}
+    (f : w $-> x) (g : w $-> y) (h : w $-> z)
+    : cat_binprod_twist x y z $o cat_binprod_corec f (cat_binprod_corec g h)
+      $== cat_binprod_corec g (cat_binprod_corec f h).
+  Proof.
+    nrapply cat_binprod_eta_pr.
+    - nrefine (cat_assoc_opp _ _ _ $@ _).
+      refine ((_ $@R _) $@ cat_assoc _ _ _ $@ (_ $@L _) $@ (_ $@ _^$)).
+      1: nrapply cat_binprod_pr1_twist.
+      1: nrapply cat_binprod_beta_pr2.
+      1,2: nrapply cat_binprod_beta_pr1.
+    - refine (cat_assoc_opp _ _ _ $@ (_ $@R _) $@ _ $@ (cat_binprod_beta_pr2 _ _)^$).
+      1: nrapply cat_binprod_beta_pr2.
+      nrefine (cat_binprod_fmap01_corec _ _ _ $@ _).
+      nrapply cat_binprod_corec_eta.
+      1: exact (Id _).
+      nrapply cat_binprod_beta_pr2.
+  Defined.
 
   Lemma cat_binprod_twist_cat_binprod_twist (x y z : A)
     : cat_binprod_twist x y z $o cat_binprod_twist y x z $== Id _.
@@ -753,6 +822,21 @@ Section Associativity.
     nrefine (cat_assoc _ _ _ $@ (_ $@L cat_pr2_fmap01_binprod _ _) $@ _).
     exact (cat_assoc_opp _ _ _ $@ (cat_binprod_beta_pr1 _ _ $@R _)).
   Defined.
+  
+  Definition cat_binprod_associator_corec {w x y z}
+    (f : w $-> x) (g : w $-> y) (h : w $-> z)
+    : associator_binprod x y z $o cat_binprod_corec f (cat_binprod_corec g h)
+      $== cat_binprod_corec (cat_binprod_corec f g) h. 
+  Proof.
+    nrefine ((Monoidal.associator_twist'_unfold _ _ _ _ _ _ _ _ $@R _) $@ _).
+    nrefine ((cat_assoc_opp _ _ _ $@R _) $@ cat_assoc _ _ _ $@ (_ $@L (_ $@ _)) $@ _). 
+    1: nrapply cat_binprod_fmap01_corec.
+    1: rapply (cat_binprod_corec_eta _ _ _ _ (Id _)).
+    1: nrapply cat_binprod_swap_corec.
+    nrefine (cat_assoc _ _ _ $@ (_ $@L _) $@ _).
+    1: nrapply cat_binprod_twist_corec.
+    nrapply cat_binprod_swap_corec.
+  Defined.
 
   Context (unit : A) `{!IsTerminal unit}.