diff --git a/theories/Algebra/Categorical/MonoidObject.v b/theories/Algebra/Categorical/MonoidObject.v
new file mode 100644
index 0000000000..976ce013ab
--- /dev/null
+++ b/theories/Algebra/Categorical/MonoidObject.v
@@ -0,0 +1,197 @@
+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. Various 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..cbc350f43a 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)
@@ -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,71 @@ 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 : B -> A -> C} `{!Is0Bifunctor G, !Is1Bifunctor G}
+  : NatTrans (uncurry F) (uncurry (flip G))
+    -> NatTrans (uncurry (flip F)) (uncurry 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.
+
+Definition nattrans_flip' {A B C : Type}
+  `{Is1Cat A, Is1Cat B, Is1Cat C}
+  {F : A -> B -> C} `{!Is0Bifunctor F, !Is1Bifunctor F}
+  {G : B -> A -> C} `{!Is0Bifunctor G, !Is1Bifunctor G}
+  : NatTrans (uncurry (flip F)) (uncurry G)
+    -> NatTrans (uncurry F) (uncurry (flip G))
+  := nattrans_flip (F:=flip F) (G:=flip G).
+
+(** ** 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}.