diff --git a/theories/WildCat/Bifunctor.v b/theories/WildCat/Bifunctor.v
index bcfe757789f..dd6c4667ccc 100644
--- a/theories/WildCat/Bifunctor.v
+++ b/theories/WildCat/Bifunctor.v
@@ -103,14 +103,14 @@ Defined.
 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 F f (Id b) $== fmap10 F f b
   := (fmap_id _ _ $@R _) $@ cat_idl _.
 
 (** [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 F (Id a) g $== fmap01 F a g
   := (_ $@L fmap_id _ _) $@ cat_idr _.
 
 (** 2-functorial action *)
diff --git a/theories/WildCat/Coproducts.v b/theories/WildCat/Coproducts.v
index 7548ecc4c8f..34ad81b9829 100644
--- a/theories/WildCat/Coproducts.v
+++ b/theories/WildCat/Coproducts.v
@@ -2,7 +2,8 @@ Require Import Basics.Overture Basics.Tactics Basics.Decidable.
 Require Import Types.Bool.
 Require Import WildCat.Core WildCat.Equiv WildCat.Forall WildCat.NatTrans
                WildCat.Opposite WildCat.Products WildCat.Universe
-               WildCat.Yoneda WildCat.ZeroGroupoid WildCat.PointedCat.
+               WildCat.Yoneda WildCat.ZeroGroupoid WildCat.PointedCat
+               WildCat.Monoidal.
 
 (** * Categories with coproducts *)
 
@@ -226,7 +227,7 @@ Lemma cate_coprod_assoc {A : Type} `{HasEquivs A}
   : cat_bincoprod x (cat_bincoprod y z)
     $<~> cat_bincoprod (cat_bincoprod x y) z.
 Proof.
-  exact (@cate_binprod_assoc A^op _ _ _ _ _ e x y z)^-1$.
+  exact (@associator_binprod A^op _ _ _ _ _ e x y z)^-1$.
 Defined.
 
 (** *** Binary coproduct functor *)
diff --git a/theories/WildCat/Monoidal.v b/theories/WildCat/Monoidal.v
index 7b145cc3dc5..e2e81366f07 100644
--- a/theories/WildCat/Monoidal.v
+++ b/theories/WildCat/Monoidal.v
@@ -1,8 +1,10 @@
-Require Import Basics.Overture.
-Require Import Types.Forall.
-Require Import WildCat.Core WildCat.Bifunctor WildCat.Prod WildCat.Equiv WildCat.NatTrans.
+Require Import Basics.Overture Basics.Tactics Types.Forall.
+Require Import WildCat.Core WildCat.Bifunctor WildCat.Prod WildCat.Equiv.
+Require Import WildCat.NatTrans WildCat.Square.
 
-(** * Monoidal 1-categories *)
+(** * Monoidal Categories *)
+
+(** In this file we define monoidal categories and symmetric monoidal categories. *)
 
 (** ** Typeclasses for common diagrams *)
 
@@ -12,10 +14,10 @@ Require Import WildCat.Core WildCat.Bifunctor WildCat.Prod WildCat.Equiv WildCat
 
 (** A natural equivalence witnessing the associativity of a bifunctor. *)
 Class Associator {A : Type} `{HasEquivs A}
-  (F : A -> A -> A) `{!Is0Bifunctor F, !Is1Bifunctor F} := {   
+  (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
@@ -56,16 +58,52 @@ Arguments triangle_identity {A _ _ _ _ _} F {_ _ _} unit {_}.
 
 Class PentagonIdentity {A : Type} `{HasEquivs A}
   (F : A -> A -> A) `{!Is0Bifunctor F, !Is1Bifunctor F, !Associator F}
-  (unit : A) `{!LeftUnitor F unit, !RightUnitor F unit}
-  (** The pentagon identity for an associator and unitors. *)
+  (** The pentagon identity for an associator. *)
   := pentagon_identity a b c d
     : associator (F a b) c d $o associator a b (F c d)
       $== fmap10 F (associator a b c) d $o associator a (F b c) d
         $o fmap01 F a (associator b c d).
 Coercion pentagon_identity : PentagonIdentity >-> Funclass.
-Arguments pentagon_identity {A _ _ _ _ _} F {_ _ _} unit {_}.
+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);
+}.
+Coercion braid : Braiding >-> Funclass.
+Arguments braid {A _ _ _ _ F _ _ _} a b.
 
-(** ** Definition *)
+Class SymmetricBraiding {A : Type} `{Is1Cat A}
+  (F : A -> A -> A) `{!Is0Bifunctor F, !Is1Bifunctor F} := {
+  braiding_symmetricbraiding :: Braiding F;
+  braid_braid : forall a b, braid a b $o braid b a $== Id (F b a);
+}.
+(** We could have used [::>] in [braiding_symmetricbraiding] instead however due to bug https://github.com/coq/coq/issues/18971 the coercion isn't registered, so we have to register it manually instead. *)
+Coercion braiding_symmetricbraiding : SymmetricBraiding >-> Braiding.
+Arguments braid_braid {A _ _ _ _ F _ _ _} a b.
+
+(** *** Hexagon identity *)
+
+Class HexagonIdentity {A : Type} `{HasEquivs A}
+  (F : A -> A -> A)
+  `{!Is0Bifunctor F, !Is1Bifunctor F, !Associator F, !Braiding F}
+  (** The hexagon identity for an associator and a braiding. *)
+  := hexagon_identity a b c
+    : fmap10 F (braid b a) c $o associator b a c $o fmap01 F b (braid c a)
+      $== associator a b c $o braid (F b c) a $o associator b c a.
+Coercion hexagon_identity : HexagonIdentity >-> Funclass.
+Arguments hexagon_identity {A _ _ _ _ _} F {_ _}.
+
+(** ** Monoidal Categories *)
 
 (** A monoidal 1-category is a 1-category with equivalences together with the following: *)
 Class IsMonoidal (A : Type) `{HasEquivs A}
@@ -87,5 +125,679 @@ Class IsMonoidal (A : Type) `{HasEquivs A}
   (** The triangle identity. *)
   cat_tensor_triangle_identity :: TriangleIdentity cat_tensor cat_tensor_unit;
   (** The pentagon identity. *)
-  cat_tensor_pentagon_identity :: PentagonIdentity cat_tensor cat_tensor_unit;
+  cat_tensor_pentagon_identity :: PentagonIdentity cat_tensor;
 }.
+
+(** TODO: Braided monoidal categories *)
+
+(** ** Symmetric Monoidal Categories *)
+
+(** A symmetric monoidal 1-category is a 1-category with equivalences together with the following: *)
+Class IsSymmetricMonoidal (A : Type) `{HasEquivs A}
+  (** A binary operation [cat_tensor] called the tensor product. *)
+  (cat_tensor : A -> A -> A)
+  (** A unit object [cat_tensor_unit] called the tensor unit. *)
+  (cat_tensor_unit : A)
+  := {
+  (** A monoidal structure with [cat_tensor] and [cat_tensor_unit]. *)
+  issymmetricmonoidal_ismonoidal :: IsMonoidal A cat_tensor cat_tensor_unit;
+  (** A natural transformation [braid] witnessing the symmetry of the tensor product such that [braid] is its own inverse. *)
+  cat_symm_tensor_braiding :: SymmetricBraiding cat_tensor;
+  (** The hexagon identity. *)
+  cat_symm_tensor_hexagon :: HexagonIdentity cat_tensor;
+}.
+
+(** ** Theory about [SymmetricBraid] *)
+
+Section SymmetricBraid.
+  Context {A : Type} {F : A -> A -> A} `{SymmetricBraiding A F, !HasEquivs A}.
+
+  (** [braid] is its own inverse and therefore an equivalence. *)
+  Local Instance catie_braid a b : CatIsEquiv (braid a b)
+    := catie_adjointify (braid a b) (braid b a) (braid_braid a b) (braid_braid b a).
+
+  (** [braide] is the bundled equivalence whose underlying map is [braid]. *)
+  Local Definition braide a b
+    : F a b $<~> F b a
+    := Build_CatEquiv (braid a b).
+
+  Local Definition moveL_braidL a b c f (g : c $-> _)
+    : braid a b $o f $== g -> f $== braid b a $o g.
+  Proof.
+    intros p.
+    apply (cate_monic_equiv (braide a b)).
+    refine ((cate_buildequiv_fun _ $@R _) $@ p $@ _ $@ cat_assoc _ _ _).
+    refine ((cat_idl _)^$ $@ (_^$ $@R _)).
+    refine ((cate_buildequiv_fun _ $@R _) $@ _).
+    apply braid_braid.
+  Defined.
+
+  Local Definition moveL_braidR a b c f (g : _ $-> c)
+    : f $o braid a b $== g -> f $== g $o braid b a.
+  Proof.
+    intros p.
+    apply (cate_epic_equiv (braide a b)).
+    refine (_ $@ (cat_assoc _ _ _)^$).
+    refine (_ $@ (_ $@L ((_ $@L cate_buildequiv_fun _) $@ _)^$)).
+    2: apply braid_braid.
+    refine ((_ $@L _) $@ _ $@ (cat_idr _)^$).
+    1: apply cate_buildequiv_fun.
+    exact p.
+  Defined.
+
+  Local Definition moveR_braidL a b c f (g : c $-> _)
+    : f $== braid b a $o g -> braid a b $o f $== g.
+  Proof.
+    intros p; symmetry; apply moveL_braidL; symmetry; exact p.
+  Defined.
+
+  Local Definition moveR_braidR a b c f (g : _ $-> c)
+    : f $== g $o braid b a -> f $o braid a b $== g.
+  Proof.
+    intros p; symmetry; apply moveL_braidR; symmetry; exact p.
+  Defined.
+
+  Local Definition moveL_fmap01_braidL a b c d f (g : d $-> _)
+    : fmap01 F a (braid b c) $o f $== g
+      -> f $== fmap01 F a (braid c b) $o g.
+  Proof.
+    intros p.
+    apply (cate_monic_equiv (emap01 F a (braide b c))).
+    refine (_ $@ cat_assoc _ _ _).
+    refine (_ $@ (_ $@R _)).
+    2: { refine (_ $@ (_^$ $@R _)).
+      2: apply cate_buildequiv_fun.
+      refine ((fmap_id _ _)^$ $@ fmap2 _ _ $@ fmap_comp _ _ _).
+      refine ((_ $@R _) $@ _)^$.
+      1: apply cate_buildequiv_fun.
+      apply braid_braid. }
+    refine ((_ $@R _) $@ p $@ (cat_idl _)^$).
+    refine (_ $@ fmap2 _ _);
+    apply cate_buildequiv_fun.
+  Defined.
+
+  Local Definition moveL_fmap01_braidR a b c d f (g : _ $-> d)
+    :  f $o fmap01 F a (braid b c) $== g
+      -> f $== g $o fmap01 F a (braid c b).
+  Proof.
+    intros p.
+    apply (cate_epic_equiv (emap01 F a (braide b c))).
+    refine (_ $@ (cat_assoc _ _ _)^$).
+    refine (_ $@ (_ $@L _)).
+    2: { refine (_^$ $@ (_ $@L _^$)).
+      2: apply cate_buildequiv_fun.
+      refine ((fmap_comp _ _ _)^$ $@ fmap2 _ _ $@ fmap_id _ _).
+      refine ((_ $@L _) $@ _).
+      1: apply cate_buildequiv_fun.
+      apply braid_braid. }
+    refine ((_ $@L _) $@ p $@ (cat_idr _)^$).
+    refine (_ $@ fmap2 _ _);
+    apply cate_buildequiv_fun.
+  Defined.
+
+  Local Definition moveR_fmap01_braidL a b c d f (g : d $-> _)
+    : f $== fmap01 F a (braid c b) $o g
+      -> fmap01 F a (braid b c) $o f $== g.
+  Proof.
+    intros p; symmetry; apply moveL_fmap01_braidL; symmetry; exact p.
+  Defined.
+
+  Local Definition moveR_fmap01_braidR a b c d f (g : _ $-> d)
+    : f $== g $o fmap01 F a (braid c b)
+      -> f $o fmap01 F a (braid b c) $== g.
+  Proof.
+    intros p; symmetry; apply moveL_fmap01_braidR; symmetry; exact p.
+  Defined.
+
+  Local Definition moveL_fmap01_fmap01_braidL a b c d e f (g : e $-> _)
+    : fmap01 F a (fmap01 F b (braid c d)) $o f $== g
+      -> f $== fmap01 F a (fmap01 F b (braid d c)) $o g.
+  Proof.
+    intros p.
+    apply (cate_monic_equiv (emap01 F a (emap01 F b (braide c d)))).
+    refine (_ $@ cat_assoc _ _ _).
+    refine (_ $@ (_ $@R _)).
+    2: { refine (_ $@ (_^$ $@R _)).
+      2: apply cate_buildequiv_fun.
+      refine ((fmap_id _ _)^$ $@ fmap2 _ _ $@ fmap_comp _ _ _).
+      refine (_ $@ (_^$ $@R _)).
+      2: apply cate_buildequiv_fun.
+      refine ((fmap_id _ _)^$ $@ fmap2 _ _ $@ fmap_comp _ _ _).
+      refine ((_ $@R _) $@ _)^$.
+      1: apply cate_buildequiv_fun.
+      apply braid_braid. }
+    refine ((_ $@R _) $@ p $@ (cat_idl _)^$).
+    refine (cate_buildequiv_fun _ $@ fmap02 _ _ _).
+    refine (cate_buildequiv_fun _ $@ fmap02 _ _ _).
+    apply cate_buildequiv_fun.
+  Defined.
+
+  Local Definition moveL_fmap01_fmap01_braidR a b c d e f (g : _ $-> e)
+    : f $o fmap01 F a (fmap01 F b (braid c d)) $== g
+      -> f $== g $o fmap01 F a (fmap01 F b (braid d c)).
+  Proof.
+    intros p.
+    apply (cate_epic_equiv (emap01 F a (emap01 F b (braide c d)))).
+    refine (_ $@ (cat_assoc _ _ _)^$).
+    refine (_ $@ (_ $@L _)).
+    2: { refine (_^$ $@ (_ $@L _^$)).
+      2: apply cate_buildequiv_fun.
+      refine ((fmap_comp _ _ _)^$ $@ fmap2 _ _ $@ fmap_id _ _).
+      refine ((_ $@L _) $@ _).
+      1: apply cate_buildequiv_fun.
+      refine ((fmap_comp _ _ _)^$ $@ fmap2 _ _ $@ fmap_id _ _).
+      refine ((_ $@L _) $@ _).
+      1: apply cate_buildequiv_fun.
+      apply braid_braid. }
+    refine ((_ $@L _) $@ p $@ (cat_idr _)^$).
+    refine (cate_buildequiv_fun _ $@ fmap02 _ _ _).
+    refine (cate_buildequiv_fun _ $@ fmap02 _ _ _).
+    apply cate_buildequiv_fun.
+  Defined.
+
+  Local Definition moveR_fmap01_fmap01_braidL a b c d e f (g : e $-> _)
+    : f $== fmap01 F a (fmap01 F b (braid d c)) $o g
+      -> fmap01 F a (fmap01 F b (braid c d)) $o f $== g.
+  Proof.
+    intros p; symmetry; apply moveL_fmap01_fmap01_braidL; symmetry; exact p.
+  Defined.
+
+  Local Definition moveR_fmap01_fmap01_braidR a b c d e f (g : _ $-> e)
+    : f $== g $o fmap01 F a (fmap01 F b (braid d c))
+      -> f $o fmap01 F a (fmap01 F b (braid c d)) $== g.
+  Proof.
+    intros p; symmetry; apply moveL_fmap01_fmap01_braidR; symmetry; exact p.
+  Defined.
+
+  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.
+  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).
+  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).
+  Defined.
+
+End SymmetricBraid.
+
+(** ** 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.
+
+The core observation is that the associator can be broken up into a [braid] and what we call a [twist] map. The twist map takes a right associated triple [(A, (B, C))] and swaps the first two factors [(B, (A, C)]. Together with functoriality of the tensor and the braiding, here termed [braid] we can simplify the axioms we ask for.
+
+For instance, the hexagon identity is about associators, but if we unfold the definition and simplify the diagram, we get a diagram about only twists and braids.
+
+This means in practice, you can show a category has a symmetric monoidal structure by proving some simpler axioms. This idea has been used in TriJoin.v to show the associativity of join for example. *)
+
+Section TwistConstruction.
+  (** The aim of this section is to build a symmetric monoidal category. We do this piecewise so that the separate steps are useful in and of themselves.
+
+  Our basic starting assumption is that we have a category with equivalences, a bifunctor called the tensor product, and a unit object.*)
+  Context (A : Type) `{HasEquivs A}
+    (cat_tensor : A -> A -> A) (cat_tensor_unit : A)
+    `{!Is0Bifunctor cat_tensor, !Is1Bifunctor cat_tensor}
+
+    (** Next we postulate the existence of a [braid] map. This takes a tensor pair and swaps the factors. We also postulate that [braid] is natural in both factors and self-inverse. *)
+    (braid : SymmetricBraiding cat_tensor)
+
+    (** We postulate the existence of a [twist] map. This takes a right associated triple [(A, (B, C))] and swaps the first two factors [(B, (A, C)]. We also postulate that [twist] is natural in all three factors and self-inverse. *)
+    (twist : forall a b c, cat_tensor a (cat_tensor b c) $-> cat_tensor b (cat_tensor a c))
+    (twist_twist : forall a b c, twist a b c $o twist b a c $== Id _)
+    (twist_nat : forall a a' b b' c c' (f : a $-> a') (g : b $-> b') (h : c $-> c'),
+      twist a' b' c' $o fmap11 cat_tensor f (fmap11 cat_tensor g h)
+      $== fmap11 cat_tensor g (fmap11 cat_tensor f h) $o twist a b c)
+
+    (** We assume that there is a natural isomorphism [right_unitor] witnessing the right unit law. The left unit law will be derived from this one. We also assume a coherence called [twist_unitor] which determines how the right_unitor interacts with [braid] and [twist]. This is the basis of the triangle axiom. *)
+    (right_unitor : RightUnitor cat_tensor cat_tensor_unit)
+    (twist_unitor : forall a b, fmap01 cat_tensor a (right_unitor b)
+      $== braid b a $o fmap01 cat_tensor b (right_unitor a) $o twist a b cat_tensor_unit)
+
+    (** The hexagon identity is about the interaction of associators and braids. We will derive this axiom from an analogous one for twists and braids. *)
+    (twist_hexagon : forall a b c,
+      fmap01 cat_tensor c (braid b a) $o twist b c a $o fmap01 cat_tensor b (braid a c)
+      $== twist a c b $o fmap01 cat_tensor a (braid b c) $o twist b a c)
+
+    (** The 9-gon identity. TODO: explain this *)
+    (twist_9_gon : forall a b c d,
+        fmap01 cat_tensor c (braid (cat_tensor a b) d)
+        $o twist (cat_tensor a b) c d
+        $o braid (cat_tensor c d) (cat_tensor a b)
+        $o twist a (cat_tensor c d) b
+        $o fmap01 cat_tensor a (braid b (cat_tensor c d))
+      $== fmap01 cat_tensor c (twist a d b)
+        $o fmap01 cat_tensor c (fmap01 cat_tensor a (braid b d))
+        $o twist a c (cat_tensor b d)
+        $o fmap01 cat_tensor a (twist b c d))
+  .
+
+  (** *** Setup *)
+
+  (** Before starting the proofs, we need to setup some useful definitions and helpful lemmas for working with diagrams. *)
+
+  (** We give notations and abbreviations to the morphisms that will appear in diagrams. This helps us read the goal and understand what is happening, otherwise it is too verbose. *)
+  Declare Scope monoidal_scope.
+  Local Infix "⊗" := cat_tensor (at level 40) : monoidal_scope.
+  Local Infix "⊗R" := (fmap01 cat_tensor) (at level 40) : monoidal_scope.
+  Local Infix "⊗L" := (fmap10 cat_tensor) (at level 40) : monoidal_scope.
+  Local Notation "f ∘ g" := (f $o g) (at level 61, left associativity, format "f  '/' '∘'  g") : monoidal_scope.
+  Local Notation "f $== g :> A" := (GpdHom (A := A) f g)
+    (at level 80, format "'[v' '[v' f ']' '/'  $== '/'  '[v' g ']'  '/' :>  '[' A ']' ']'")
+    : long_path_scope.
+  Local Open Scope monoidal_scope.
+
+  (** [twist] is an equivalence which we will call [twiste]. *)
+  Local Definition twiste a b c
+    : cat_tensor a (cat_tensor b c) $<~> cat_tensor b (cat_tensor a c)
+    := cate_adjointify (twist a b c) (twist b a c)
+        (twist_twist a b c) (twist_twist b a c).
+
+  (** *** Finer naturality *)
+
+  (** The naturality postulates we have for [twist] are natural in all their arguments similtaneously. We show the finer naturality of [twist] in each argument separately as this becomes more useful in practice. *)
+
+  Local Definition twist_nat_l {a a'} (f : a $-> a') b c
+    : twist a' b c $o fmap10 cat_tensor f (cat_tensor b c)
+      $== fmap01 cat_tensor b (fmap10 cat_tensor f c) $o twist a b c.
+  Proof.
+    refine ((_ $@L _^$) $@ twist_nat a a' b b c c f (Id _) (Id _) $@ (_ $@R _)).
+    - refine (fmap12 _ _ _ $@ fmap10_is_fmap11 _ _ _).
+      rapply fmap11_id.
+    - refine (fmap12 _ _ _ $@ fmap01_is_fmap11 _ _ _).
+      rapply fmap10_is_fmap11.
+  Defined.
+
+  Local Definition twist_nat_m a {b b'} (g : b $-> b') c
+    : twist a b' c $o fmap01 cat_tensor a (fmap10 cat_tensor g c)
+      $== fmap10 cat_tensor g (cat_tensor a c) $o twist a b c.
+  Proof.
+    refine ((_ $@L _^$) $@ twist_nat a a b b' c c (Id _) g (Id _) $@ (_ $@R _)).
+    - refine (fmap12 _ _ _ $@ fmap01_is_fmap11 _ _ _).
+      rapply fmap10_is_fmap11.
+    - refine (fmap12 _ _ _ $@ fmap10_is_fmap11 _ _ _).
+      rapply fmap11_id.
+  Defined.
+
+  Local Definition twist_nat_r a b {c c'} (h : c $-> c')
+    : twist a b c' $o fmap01 cat_tensor a (fmap01 cat_tensor b h)
+      $== fmap01 cat_tensor b (fmap01 cat_tensor a h) $o twist a b c.
+  Proof.
+    refine ((_ $@L _^$) $@ twist_nat a a b b c c' (Id _) (Id _) h $@ (_ $@R _)).
+    - refine (fmap12 _ _ _ $@ fmap01_is_fmap11 _ _ _).
+      rapply fmap01_is_fmap11.
+    - refine (fmap12 _ _ _ $@ fmap01_is_fmap11 _ _ _).
+      rapply fmap01_is_fmap11.
+  Defined.
+
+  (** *** Movement lemmas *)
+
+  (** Here we collect lemmas about moving morphisms around in a diagram. We could have created [cate_moveL_eM]-style lemmas for [CatIsEquiv] but this leads to a lot of unnecessary unfolding and duplication. It is typically easier to use a hand crafted lemma for each situation. *)
+
+  (** TODO: A lot of these proofs are copy and pasted between lemmas. We need to work out an efficient way of proving them. *)
+
+  (** **** Moving [twist] *)
+
+  Local Definition moveL_twistL a b c d f (g : d $-> _)
+    : twist a b c $o f $== g -> f $== twist b a c $o g.
+  Proof.
+    intros p.
+    apply (cate_monic_equiv (twiste a b c)).
+    nrefine ((cate_buildequiv_fun _ $@R _) $@ p $@ _ $@ cat_assoc _ _ _).
+    refine ((cat_idl _)^$ $@ (_^$ $@R _)).
+    refine ((cate_buildequiv_fun _ $@R _) $@ _).
+    apply twist_twist.
+  Defined.
+
+  Local Definition moveL_twistR a b c d f (g : _ $-> d)
+    : f $o twist a b c $== g -> f $== g $o twist b a c.
+  Proof.
+    intros p.
+    apply (cate_epic_equiv (twiste a b c)).
+    refine (_ $@ (cat_assoc _ _ _)^$).
+    refine (_ $@ (_ $@L ((_ $@L cate_buildequiv_fun _) $@ _)^$)).
+    2: apply twist_twist.
+    refine ((_ $@L _) $@ _ $@ (cat_idr _)^$).
+    1: apply cate_buildequiv_fun.
+    exact p.
+  Defined.
+
+  Local Definition moveR_twistL a b c d f (g : d $-> _)
+    : f $== twist b a c $o g -> twist a b c $o f $== g.
+  Proof.
+    intros p; symmetry; apply moveL_twistL; symmetry; exact p.
+  Defined.
+
+  Local Definition moveR_twistR a b c d f (g : _ $-> d)
+    : f $== g $o twist b a c -> f $o twist a b c $== g.
+  Proof.
+    intros p; symmetry; apply moveL_twistR; symmetry; exact p.
+  Defined.
+
+  Local Definition moveL_fmap01_twistL a b c d e f (g : e $-> _)
+    : fmap01 cat_tensor a (twist b c d) $o f $== g
+      -> f $== fmap01 cat_tensor a (twist c b d) $o g.
+  Proof.
+    intros p.
+    apply (cate_monic_equiv (emap01 cat_tensor a (twiste b c d))).
+    refine (_ $@ cat_assoc _ _ _).
+    refine (_ $@ (_ $@R _)).
+    2: { refine (_ $@ (_^$ $@R _)).
+      2: apply cate_buildequiv_fun.
+      refine ((fmap_id _ _)^$ $@ fmap2 _ _ $@ fmap_comp _ _ _).
+      refine (_^$ $@ (_^$ $@R _)).
+      2: apply cate_buildequiv_fun.
+      apply twist_twist. }
+    refine ((_ $@R _) $@ p $@ (cat_idl _)^$).
+    refine (cate_buildequiv_fun _ $@ fmap02 _ _ _).
+    apply cate_buildequiv_fun.
+  Defined.
+
+  Local Definition moveL_fmap01_twistR a b c d e f (g : _ $-> e)
+    : f $o fmap01 cat_tensor a (twist b c d) $== g
+      -> f $== g $o fmap01 cat_tensor a (twist c b d).
+  Proof.
+    intros p.
+    apply (cate_epic_equiv (emap01 cat_tensor a (twiste b c d))).
+    refine (_ $@ (cat_assoc _ _ _)^$).
+    refine (_ $@ (_ $@L _)).
+    2: { refine (_^$ $@ (_ $@L _^$)).
+      2: apply cate_buildequiv_fun.
+      refine ((fmap_comp _ _ _)^$ $@ fmap2 _ _ $@ fmap_id _ _).
+      refine ((_ $@L _) $@ _).
+      1: apply cate_buildequiv_fun.
+      apply twist_twist. }
+    refine ((_ $@L _) $@ p $@ (cat_idr _)^$).
+    refine (cate_buildequiv_fun _ $@ fmap02 _ _ _).
+    apply cate_buildequiv_fun.
+  Defined.
+
+  Local Definition moveR_fmap01_twistL a b c d e f (g : e $-> _)
+    : f $== fmap01 cat_tensor a (twist c b d) $o g
+      -> fmap01 cat_tensor a (twist b c d) $o f $== g.
+  Proof.
+    intros p; symmetry; apply moveL_fmap01_twistL; symmetry; exact p.
+  Defined.
+
+  Local Definition moveR_fmap01_twistR a b c d e f (g : _ $-> e)
+    : f $== g $o fmap01 cat_tensor a (twist c b d)
+      -> f $o fmap01 cat_tensor a (twist b c d) $== g.
+  Proof.
+    intros p; symmetry; apply moveL_fmap01_twistR; symmetry; exact p.
+  Defined.
+
+  (** *** The associator *)
+
+  (** Using [braide] and [twiste] we can build an associator. *)
+  Local Definition associator_twist' a b c
+    : cat_tensor a (cat_tensor b c) $<~> cat_tensor (cat_tensor a b) c.
+  Proof.
+    (** We can build the associator out of [braide] and [twiste]. *)
+    refine (braide _ _ $oE _).
+    nrefine (twiste _ _ _ $oE _).
+    exact (emap01 cat_tensor a (braide _ _)).
+  Defined.
+
+  (** We would like to be able to unfold [associator_twist'] to the underlying morphisms. We use this lemma to make that process easier. *)
+  Local Definition associator_twist'_unfold a b c
+    : cate_fun (associator_twist' a b c)
+    $== braid c (cat_tensor a b) $o (twist a c b $o fmap01 cat_tensor a (braid b c)).
+  Proof.
+    refine (cate_buildequiv_fun _ $@ (_ $@@ cate_buildequiv_fun _)).
+    nrefine (cate_buildequiv_fun _ $@ (_ $@@ cate_buildequiv_fun _)).
+    refine (cate_buildequiv_fun _ $@ fmap2 _ _).
+    apply cate_buildequiv_fun.
+  Defined.
+
+  (** Now we can use [associator_twist'] and show that it is a natural equivalence in each variable. *)
+  Local Instance associator_twist : Associator cat_tensor.
+  Proof.
+    snrapply Build_Associator.
+    - exact associator_twist'.
+    - simpl; intros [[a b] c] [[a' b'] c'] [[f g] h]; simpl in f, g, h.
+      (** To prove naturality it will be easier to reason about squares. *)
+      change (?w $o ?x $== ?y $o ?z) with (Square z w x y).
+      (** First we remove all the equivalences from the equation. *)
+      nrapply hconcatL.
+      1: apply associator_twist'_unfold.
+      nrapply hconcatR.
+      2: apply associator_twist'_unfold.
+      (** The first square involving [braid] on its own is a naturality square. *)
+      nrapply vconcat.
+      2: rapply braid_nat.
+      (** The second square is just the naturality of twist. *)
+      nrapply vconcat.
+      2: apply twist_nat.
+      (** We rewrite one of the edges to make sure a functor application is grouped together. *)
+      nrapply vconcatL.
+      { refine ((cat_assoc _ _ _)^$ $@ (_^$ $@R _)).
+        rapply fmap_comp. }
+      (** This allows us to compose with bifunctor coherence on one side. *)
+      nrapply hconcat.
+      1: rapply fmap11_coh.
+      (** Leaving us with a square with a functor application. *)
+      rapply fmap_square.
+      (** We are finally left with the naturality of braid. *)
+      apply braid_nat.
+  Defined.
+
+  (** We abbreviate the associator to [α] for the remainder of the section. *)
+  Local Notation α := associator_twist.
+
+  (** *** Unitors *)
+
+  (** Since we assume the [right_unitor] exists, we can derive the [left_unitor] from it together with [braid]. *)
+  Local Instance left_unitor_twist : LeftUnitor cat_tensor cat_tensor_unit.
+  Proof.
+    snrapply Build_NatEquiv'.
+    - snrapply Build_NatTrans.
+      + exact (fun a => right_unitor a $o braid cat_tensor_unit a).
+      + intros a b f.
+        change (?w $o ?x $== ?y $o ?z) with (Square z w x y).
+        nrapply vconcat.
+        2: rapply (isnat right_unitor f).
+        nrapply vconcatL.
+        1: symmetry; rapply fmap01_is_fmap11.
+        nrapply vconcatR.
+        2: symmetry; rapply fmap10_is_fmap11.
+        rapply braid_nat.
+    - intros a.
+      rapply compose_catie'.
+      rapply catie_braid.
+  Defined.
+
+  (** *** Triangle *)
+
+  (** The triangle identity can easily be proven by rearranging the diagram, cancelling and using naturality of [braid]. *)
+  Local Instance triangle_twist : TriangleIdentity cat_tensor cat_tensor_unit.
+  Proof.
+    intros a b.
+    refine (_ $@ (_ $@L _)^$).
+    2: apply associator_twist'_unfold.
+    refine (fmap02 _ a (cate_buildequiv_fun _) $@ _); cbn.
+    refine (fmap01_comp _ _ _ _ $@ _).
+    do 2 refine (_ $@ cat_assoc _ _ _).
+    refine ((twist_unitor _ _ $@ (_ $@R _)) $@R _).
+    apply braid_nat_r.
+  Defined.
+
+  (** *** Pentagon *)
+
+  Local Open Scope long_path_scope.
+
+  Local Instance pentagon_twist : PentagonIdentity cat_tensor.
+  Proof.
+    clear twist_unitor right_unitor cat_tensor_unit.
+    intros a b c d.
+    refine ((_ $@@ _) $@ _ $@ ((fmap02 _ _ _ $@ _)^$ $@@ (_ $@@ (fmap20 _ _ _ $@ _))^$)).
+    1,2,4,6,7: apply associator_twist'_unfold.
+    2: refine (fmap01_comp _ _ _ _ $@ (_ $@L (fmap01_comp _ _ _ _))).
+    2: refine (fmap10_comp _ _ _ _ $@ (_ $@L (fmap10_comp _ _ _ _))).
+    (** We use a notation defined above that shows the base type of the groupoid hom and formats the equation in a way that is easier to read. *)
+    (** Normalize brackets on LHS *)
+    refine (cat_assoc _ _ _ $@ _).
+    refine (_ $@L (cat_assoc _ _ _) $@ _).
+    do 4 refine ((cat_assoc _ _ _)^$ $@ _).
+    (** Normalize brackets on RHS *)
+    refine (_ $@ (((cat_assoc _ _ _) $@R _) $@R _)).
+    do 2 refine (_ $@ ((cat_assoc _ _ _) $@R _)).
+    do 2 refine (_ $@ cat_assoc _ _ _).
+    (** Cancel two braids next to eachother. *)
+    apply moveL_fmap01_fmap01_braidR.
+    apply moveL_fmap01_twistR.
+    refine (_ $@ (cat_assoc _ _ _)^$).
+    refine (_ $@ ((_ $@L _) $@ cat_idr _)^$).
+    2: refine ((fmap01_comp _ _ _ _)^$ $@ fmap02 _ _ _ $@ fmap01_id _ _ _).
+    2: apply braid_braid.
+    (** *)
+    apply moveL_twistR.
+    refine (_ $@ (cat_assoc _ _ _)^$).
+    refine (_ $@ (_ $@L _)).
+    2: apply braid_nat_r.
+    refine (_ $@ cat_assoc _ _ _).
+    apply moveL_fmap01_fmap01_braidR.
+    refine (_ $@ (cat_assoc _ _ _)^$).
+    refine (_ $@ (_ $@L _)).
+    2: apply braid_nat_r.
+    refine (_ $@ cat_assoc _ _ _).
+    apply moveL_fmap01_twistR.
+    refine (_ $@ _).
+    2: apply braid_nat_r.
+    (** Putting things back. *)
+    apply moveR_fmap01_twistR.
+    apply moveR_fmap01_fmap01_braidR.
+    apply moveR_twistR.
+    apply moveR_fmap01_twistR.
+    (** There are two braids on the RHS of the LHS that can be swapped. *)
+    refine (cat_assoc _ _ _ $@ _).
+    refine ((_ $@L _) $@ _).
+    1: refine ((fmap01_comp _ _ _ _)^$ $@ fmap02 _ _ _ $@ fmap01_comp _ _ _ _).
+    1: apply braid_nat_r.
+    refine ((cat_assoc _ _ _)^$ $@ _).
+    apply moveR_fmap01_braidR.
+    (** Naturality of twist on the RHS of the LHS. *)
+    refine (cat_assoc _ _ _ $@ _).
+    refine ((_ $@L _) $@ _).
+    1: apply twist_nat_m.
+    refine ((cat_assoc _ _ _)^$ $@ _).
+    (** Moving some things to the RHS so that we can braid and cancel on the LHS. *)
+    apply moveR_twistR.
+    refine (cat_assoc _ _ _ $@ _).
+    refine ((_ $@L _) $@ _).
+    1: apply braid_nat_l.
+    refine ((cat_assoc _ _ _)^$ $@ _).
+    apply moveR_braidR.
+    refine (cat_assoc _ _ _ $@ _).
+    refine ((_ $@L _) $@ cat_idr _ $@ _).
+    1: refine ((fmap01_comp _ _ _ _)^$ $@ fmap02 _ _ _ $@ fmap01_id _ _ _).
+    1: apply braid_braid.
+    apply moveL_braidR.
+    apply moveL_twistR.
+    apply moveL_fmap01_braidR.
+    (** We are almost at the desired 9-gon. Now we cancel the inner braid on the LHS. *)
+    do 4 refine (_ $@ (cat_assoc _ _ _)^$).
+    do 3 refine (cat_assoc _ _ _ $@ _).
+    refine (_ $@L _).
+    apply moveR_twistL.
+    do 4 refine (_ $@ cat_assoc _ _ _).
+    refine ((cat_assoc _ _ _)^$ $@ _).
+    (** Now we move terms around in order to get a homotopy in [a ⊗ (b ⊗ (d ⊗ c)) $-> d ⊗ (c ⊗ (a ⊗ b))]. *)
+    apply moveL_fmap01_twistR.
+    apply moveL_twistR.
+    do 2 refine (_ $@ (cat_assoc _ _ _)^$).
+    do 3 refine (cat_assoc _ _ _ $@ _).
+    apply moveL_twistL.
+    refine (_ $@ cat_assoc _ _ _).
+    do 4 refine ((cat_assoc _ _ _)^$ $@ _).
+    apply moveR_twistR.
+    apply moveR_fmap01_twistR.
+    do 3 refine (_ $@ (cat_assoc _ _ _)^$).
+    do 2 refine (cat_assoc _ _ _ $@ _).
+    apply moveL_fmap01_braidL.
+    do 2 refine (_ $@ cat_assoc _ _ _).
+    do 3 refine ((cat_assoc _ _ _)^$ $@ _).
+    (** And finally, this is the 9-gon we asked for. *)
+    apply twist_9_gon.
+  Defined.
+
+  Local Close Scope long_path_scope.
+
+  (** *** Hexagon *)
+
+  Local Instance hexagon_twist : HexagonIdentity cat_tensor.
+  Proof.
+    intros a b c; simpl.
+    refine (((_ $@L _) $@R _) $@ _ $@ (_ $@@ (_ $@R _))^$).
+    1,3,4: apply associator_twist'_unfold.
+    do 2 refine (((cat_assoc _ _ _)^$ $@R _) $@ _).
+    refine (cat_assoc _ _ _ $@ (_ $@L _) $@ _).
+    { refine ((fmap_comp _ _ _)^$ $@ fmap2 _ _ $@ fmap_id _ _).
+      apply braid_braid. }
+    refine (cat_idr _ $@ _).
+    refine (_ $@ cat_assoc _ _ _).
+    refine (_ $@ ((cat_assoc _ _ _)^$ $@R _)).
+    refine (_ $@ (((cat_idr _)^$ $@ (_ $@L _^$)) $@R _)).
+    2: apply braid_braid.
+    refine (((braid_nat_r _)^$ $@R _) $@ _).
+    refine (cat_assoc _ _ _ $@ (_ $@L _) $@ (cat_assoc _ _ _)^$).
+    refine (_ $@ cat_assoc _ _ _).
+    apply moveL_fmap01_braidR.
+    apply twist_hexagon.
+  Defined.
+
+  (** *** Conclusion *)
+
+  (** In conclusion, we have proven the following: *)
+
+  (** There is a monoidal structure on [A]. *)
+  Local Instance ismonoidal_twist
+    : IsMonoidal A cat_tensor cat_tensor_unit
+    := {}.
+
+  (** There is a symmetric monoidal category on [A]. *)
+  Local Instance issymmetricmonoidal_twist
+    : IsSymmetricMonoidal A cat_tensor cat_tensor_unit
+    := {}.
+
+  (** TODO: WIP *)
+
+  (** Here is a hexagon involving only twist *)
+  Definition twist_hex' a b c d
+    : fmap01 cat_tensor c (twist a b d)
+      $o twist a c (cat_tensor b d)
+      $o fmap01 cat_tensor a (twist b c d)
+    $== twist b c (cat_tensor a d)
+      $o fmap01 cat_tensor b (twist a c d)
+      $o twist a b (cat_tensor c d).
+  Proof.
+    pose proof (twist_hexagon c a d $@ cat_assoc _ _ _) as p.
+    apply moveR_twistL in p.
+    apply moveR_fmap01_braidL in p.
+    apply (fmap02 cat_tensor b) in p.
+    refine (_ $@ ((_ $@L p) $@R _)); clear p.
+    apply moveL_twistR.
+    apply moveL_twistL.
+    refine (_ $@ (fmap01_comp _ _ _ _)^$).
+    (** TODO simplify *)
+    apply moveR_twistL.
+    refine (_ $@ cat_assoc _ _ _).
+  Abort.
+
+End TwistConstruction.
diff --git a/theories/WildCat/Products.v b/theories/WildCat/Products.v
index 1e54cd998d8..c50ab4ca525 100644
--- a/theories/WildCat/Products.v
+++ b/theories/WildCat/Products.v
@@ -1,8 +1,9 @@
 Require Import Basics.Equivalences Basics.Overture Basics.Tactics.
-Require Import Types.Bool Types.Prod.
+Require Import Types.Bool Types.Prod Types.Forall.
 Require Import WildCat.Bifunctor WildCat.Core WildCat.Equiv WildCat.EquivGpd
                WildCat.Forall WildCat.NatTrans WildCat.Opposite
-               WildCat.Universe WildCat.Yoneda WildCat.ZeroGroupoid.
+               WildCat.Universe WildCat.Yoneda WildCat.ZeroGroupoid
+               WildCat.Monoidal.
 
 (** * Categories with products *)
 
@@ -389,40 +390,6 @@ Proof.
       exact ((cat_assoc _ _ _)^$ $@ r (inr j) $@ cat_assoc _ _ _).
 Defined.
 
-(** *** Symmetry of binary products *)
-
-Section Symmetry.
-
-  (** The requirement of having all binary products can be weakened further to having specific binary products, but it is not clear this is a useful generality. *)
-  Context {A : Type} `{HasEquivs A} `{!HasBinaryProducts A}.
-
-  Definition cat_binprod_swap (x y : A) : cat_binprod x y $-> cat_binprod y x
-    := cat_binprod_corec cat_pr2 cat_pr1.
-
-  Lemma cat_binprod_swap_cat_binprod_swap (x y : A)
-    : cat_binprod_swap x y $o cat_binprod_swap y x $== Id _.
-  Proof.
-    apply cat_binprod_eta_pr.
-    - refine ((cat_assoc _ _ _)^$ $@ _).
-      nrefine (cat_binprod_beta_pr1 _ _ $@R _ $@ _).
-      nrefine (cat_binprod_beta_pr2 _ _ $@ _).
-      exact (cat_idr _)^$.
-    - refine ((cat_assoc _ _ _)^$ $@ _).
-      nrefine (cat_binprod_beta_pr2 _ _ $@R _ $@ _).
-      nrefine (cat_binprod_beta_pr1 _ _ $@ _).
-      exact (cat_idr _)^$.
-  Defined.
-
-  Lemma cate_binprod_swap (x y : A)
-    : cat_binprod x y $<~> cat_binprod y x.
-  Proof.
-    snrapply cate_adjointify.
-    1,2: apply cat_binprod_swap.
-    all: apply cat_binprod_swap_cat_binprod_swap.
-  Defined.
-
-End Symmetry.
-
 (** *** Binary product functor *)
 
 (** We prove bifunctoriality of [cat_binprod : A -> A -> A] by factoring it as [cat_prod Bool o Bool_rec A]. First, we prove that [Bool_rec A : A -> A -> (Bool -> A)] is a bifunctor. *)
@@ -535,38 +502,113 @@ Proof.
   by apply cat_binprod_corec_eta.
 Defined.
 
-(** *** Products in Type *)
+Definition cat_pr1_fmap01_binprod {A : Type} `{HasBinaryProducts A}
+  (a : A) {x y : A} (g : x $-> y)
+  : cat_pr1 $o fmap01 (fun x y => cat_binprod x y) a g $== cat_pr1
+  := cat_binprod_beta_pr1 _ _ $@ cat_idl _.
 
-(** Since we use the Yoneda lemma in this file, we therefore depend on WildCat.Universe which means these instances have to live here. *)
-Global Instance hasbinaryproducts_type : HasBinaryProducts Type.
+Definition cat_pr1_fmap10_binprod {A : Type} `{HasBinaryProducts A}
+  {x y : A} (f : x $-> y) (a : A)
+  : cat_pr1 $o fmap10 (fun x y => cat_binprod x y) f a $== f $o cat_pr1
+  := cat_binprod_beta_pr1 _ _.
+
+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.
-  intros X Y.
-  snrapply Build_BinaryProduct.
-  - exact (X * Y).
-  - exact fst.
-  - exact snd.
-  - intros Z f g z. exact (f z, g z).
-  - reflexivity.
-  - reflexivity.
-  - intros Z f g p q x.
-    apply path_prod.
-    + exact (p x).
-    + exact (q x).
+  refine ((cat_assoc _ _ _)^$ $@ (_ $@R _) $@ cat_assoc _ _ _ $@ _).
+  1: apply cat_binprod_beta_pr1.
+  exact (cat_idl _ $@ cat_binprod_beta_pr1 _ _).
 Defined.
 
-(** Assuming [Funext], [Type] has all products. *)
-Global Instance hasallproducts_type `{Funext} : HasAllProducts Type.
+Definition cat_pr2_fmap01_binprod {A : Type} `{HasBinaryProducts A}
+  (a : A) {x y : A} (g : x $-> y)
+  : cat_pr2 $o fmap01 (fun x y => cat_binprod x y) a g $== g $o cat_pr2
+  := cat_binprod_beta_pr2 _ _.
+
+Definition cat_pr2_fmap10_binprod {A : Type} `{HasBinaryProducts A}
+  {x y : A} (f : x $-> y) (a : A)
+  : cat_pr2 $o fmap10 (fun x y => cat_binprod x y) f a $== cat_pr2
+  := cat_binprod_beta_pr2 _ _ $@ cat_idl _.
+
+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.
-  intros I x.
-  snrapply Build_Product.
-  - exact (forall (i : I), x i).
-  - intros i f. exact (f i).
-  - intros A f a i. exact (f i a).
-  - reflexivity.
-  - intros A f g p a.
-    exact (path_forall _ _ (fun i => p i a)).
+  refine ((cat_assoc _ _ _)^$ $@ (_ $@R _) $@ cat_assoc _ _ _ $@ (_ $@L _)).
+  1: apply cat_binprod_beta_pr2.
+  apply cat_pr2_fmap10_binprod.
 Defined.
 
+(** *** Symmetry of binary products *)
+
+Section Symmetry.
+
+  (** The requirement of having all binary products can be weakened further to having specific binary products, but it is not clear this is a useful generality. *)
+  Context {A : Type} `{HasEquivs A} `{!HasBinaryProducts A}.
+
+  Definition cat_binprod_swap (x y : A) : cat_binprod x y $-> cat_binprod y x
+    := cat_binprod_corec cat_pr2 cat_pr1.
+
+  Lemma cat_binprod_swap_cat_binprod_swap (x y : A)
+    : cat_binprod_swap x y $o cat_binprod_swap y x $== Id _.
+  Proof.
+    apply cat_binprod_eta_pr.
+    - refine ((cat_assoc _ _ _)^$ $@ _).
+      nrefine (cat_binprod_beta_pr1 _ _ $@R _ $@ _).
+      nrefine (cat_binprod_beta_pr2 _ _ $@ _).
+      exact (cat_idr _)^$.
+    - refine ((cat_assoc _ _ _)^$ $@ _).
+      nrefine (cat_binprod_beta_pr2 _ _ $@R _ $@ _).
+      nrefine (cat_binprod_beta_pr1 _ _ $@ _).
+      exact (cat_idr _)^$.
+  Defined.
+
+  Lemma cate_binprod_swap (x y : A)
+    : cat_binprod x y $<~> cat_binprod y x.
+  Proof.
+    snrapply cate_adjointify.
+    1,2: apply cat_binprod_swap.
+    all: apply 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.
+  Proof.
+    apply cat_binprod_eta_pr.
+    - refine ((cat_assoc _ _ _)^$ $@ _).
+      nrefine ((cat_binprod_beta_pr1 _ _ $@R _) $@ _).
+      nrefine (cat_pr2_fmap11_binprod _ _ $@ _).
+      refine (_ $@ cat_assoc _ _ _).
+      refine (_ $@ (_^$ $@R _)).
+      2: apply cat_pr1_fmap11_binprod.
+      refine ((_ $@L _^$) $@ (cat_assoc _ _ _)^$).
+      apply cat_binprod_beta_pr1.
+    - refine ((cat_assoc _ _ _)^$ $@ _).
+      nrefine ((cat_binprod_beta_pr2 _ _ $@R _) $@ _).
+      refine (cat_pr1_fmap11_binprod _ _ $@ _).
+      refine (_ $@ cat_assoc _ _ _).
+      refine (_ $@ (_^$ $@R _)).
+      2: apply cat_pr2_fmap11_binprod.
+      refine ((_ $@L _^$) $@ (cat_assoc _ _ _)^$).
+      apply cat_binprod_beta_pr2.
+  Defined.
+  
+  Local Instance symmetricbraiding_binprod
+    : SymmetricBraiding (fun x y => cat_binprod x y).
+  Proof.
+    snrapply Build_SymmetricBraiding.
+    - snrapply Build_Braiding.
+      + exact cat_binprod_swap.
+      + intros [a b] [c d] [f g]; cbn in f, g.
+        refine (cat_binprod_swap_nat f g $@ (_ $@R _)).
+        rapply fmap11_coh.
+    - exact cat_binprod_swap_cat_binprod_swap.
+  Defined.
+
+End Symmetry.
+
 (** *** Associativity of binary products *)
 
 Section Associativity.
@@ -578,7 +620,7 @@ Section Associativity.
   Proof.
     apply cat_binprod_corec.
     - exact (cat_pr1 $o cat_pr2).
-    - exact (fmap (fun y => cat_binprod x y) cat_pr2).
+    - exact (fmap01 (fun x y => cat_binprod x y) x cat_pr2).
   Defined.
 
   Lemma cat_binprod_twist_cat_binprod_twist (x y z : A)
@@ -618,13 +660,363 @@ Section Associativity.
     1,2: apply cat_binprod_twist_cat_binprod_twist.
   Defined.
 
-  Lemma cate_binprod_assoc (x y z : A)
-    : cat_binprod x (cat_binprod y z) $<~> cat_binprod (cat_binprod x y) z.
+  Definition cat_binprod_twist_nat {a a' b b' c c' : A}
+    (f : a $-> a') (g : b $-> b') (h : c $-> c')
+    : cat_binprod_twist a' b' c'
+        $o fmap11 (fun x y => cat_binprod x y) f (fmap11 (fun x y => cat_binprod x y) g h)
+      $== fmap11 (fun x y => cat_binprod x y) g (fmap11 (fun x y => cat_binprod x y) f h)
+        $o cat_binprod_twist a b c.
+  Proof.
+    apply cat_binprod_eta_pr.
+    - refine ((cat_assoc _ _ _)^$ $@ _).
+      nrefine ((cat_binprod_beta_pr1 _ _ $@R _) $@ _).
+      nrefine (cat_assoc _ _ _ $@ _).
+      nrefine ((_ $@L _) $@ _).
+      1: apply cat_pr2_fmap11_binprod.
+      refine ((cat_assoc _ _ _)^$ $@ _).
+      nrefine ((_ $@R _) $@ _).
+      1: apply cat_pr1_fmap11_binprod.
+      nrefine (_ $@ cat_assoc _ _ _).
+      refine (_ $@ (_^$ $@R _)).
+      2: apply cat_pr1_fmap11_binprod.
+      refine (cat_assoc _ _ _ $@ (_ $@L _^$) $@ (cat_assoc _ _ _)^$).
+      apply cat_binprod_beta_pr1.
+    - refine ((cat_assoc _ _ _)^$ $@ _).
+      nrefine ((cat_binprod_beta_pr2 _ _ $@R _) $@ _).
+      nrefine (_ $@ cat_assoc _ _ _).
+      refine (_ $@ (_^$ $@R _)).
+      2: apply cat_pr2_fmap11_binprod.
+      refine (_ $@ (_ $@L _^$) $@ (cat_assoc _ _ _)^$).
+      2: apply cat_binprod_beta_pr2.
+      refine (_ $@ (cat_assoc _ _ _)^$).
+      refine (_ $@ (_ $@L _)).
+      2: rapply fmap11_coh.
+      refine ((cat_assoc _ _ _)^$ $@ (_ $@R _) $@ (cat_assoc _ _ _)).
+      refine ((fmap01_comp _ _ _ _)^$ $@ fmap02 _ _ _ $@ fmap01_comp _ _ _ _).
+      apply cat_pr2_fmap11_binprod.
+  Defined.
+  
+  Local Existing Instance symmetricbraiding_binprod. 
+
+  Local Instance associator_binprod : Associator (fun x y => cat_binprod x y).
   Proof.
-    nrefine (cate_binprod_swap _ _ $oE _).
-    nrefine (cate_binprod_twist _ _ _ $oE _).
-    refine (emap (fun y => cat_binprod x y) _).
-    exact (cate_binprod_swap _ _).
+    srapply associator_twist.
+    - exact cat_binprod_twist.
+    - exact cat_binprod_twist_cat_binprod_twist.
+    - intros ? ? ? ? ? ?; exact cat_binprod_twist_nat.
   Defined.
 
+  Context (unit : A) `{!IsTerminal unit}.
+
+  Local Instance right_unitor_binprod
+    : RightUnitor (fun x y => cat_binprod x y) unit.
+  Proof.
+    snrapply Build_NatEquiv.
+    - intros a.
+      unfold flip.
+      snrapply cate_adjointify.
+      + exact cat_pr1.
+      + apply cat_binprod_corec.
+        * exact (Id _).
+        * exact (mor_terminal _ _).
+      + apply cat_binprod_beta_pr1.
+      + apply cat_binprod_eta_pr.
+        * refine ((cat_assoc _ _ _)^$ $@ (_ $@R _) $@ _).
+          1: apply cat_binprod_beta_pr1.
+          exact (cat_idl _ $@ (cat_idr _)^$).
+        * refine ((cat_assoc _ _ _)^$ $@ (_ $@R _) $@ _).
+          1: apply cat_binprod_beta_pr2.
+          refine (_^$ $@ _).
+          1,2: rapply mor_terminal_unique.
+    - intros a b f.
+      refine ((_ $@R _) $@ _ $@ (_ $@L _^$)).
+      1,3: apply cate_buildequiv_fun.
+      apply cat_binprod_beta_pr1.
+  Defined.
+
+  Local Existing Instance left_unitor_twist.
+
+  Local Instance triangle_binprod
+    : TriangleIdentity (fun x y => cat_binprod x y) unit.
+  Proof.
+    snrapply triangle_twist.
+    intros a b.
+    refine (fmap02 _ _ _ $@ _).
+    1: apply cate_buildequiv_fun.
+    refine (_ $@ ((_ $@L fmap02 _ _ _^$) $@R _)).
+    2: apply cate_buildequiv_fun.
+    apply cat_binprod_eta_pr.    
+    - refine (cat_pr1_fmap01_binprod _ _ $@ _).
+      nrefine (_ $@ cat_assoc _ _ _).
+      refine (_ $@ (((_^$ $@R _) $@ cat_assoc _ _ _) $@R _)).
+      2: apply cat_binprod_beta_pr1.
+      refine (_ $@ (_^$ $@R _)).
+      2: apply cat_pr2_fmap01_binprod.
+      refine (_ $@ (cat_assoc _ _ _)^$).
+      refine (_^$ $@ (_ $@L _^$)).
+      2: apply cat_binprod_beta_pr2.
+      apply cat_pr1_fmap01_binprod.
+    - nrefine (_ $@ _).
+      1: apply cat_pr2_fmap01_binprod.
+      nrefine (_ $@ cat_assoc _ _ _).
+      refine (_ $@ ((_^$ $@R _) $@ cat_assoc _ _ _ $@R _)).
+      2: apply cat_binprod_beta_pr2.
+      refine (_^$ $@ (_^$ $@R _)).
+      2: apply cat_pr1_fmap01_binprod.
+      apply cat_binprod_beta_pr1.
+  Defined.
+  
+  Local Instance pentagon_binprod
+    : PentagonIdentity (fun x y => cat_binprod x y).
+  Proof.
+    snrapply pentagon_twist.
+    intros a b c d.
+    repeat nrefine (cat_assoc _ _ _ $@ _).
+    repeat refine (_ $@ (cat_assoc _ _ _)^$).
+    apply cat_binprod_eta_pr.
+    - refine ((cat_assoc _ _ _)^$ $@ _ $@ cat_assoc _ _ _).
+      refine ((_ $@R _) $@ _ $@ (_^$ $@R _)).
+      1,3: apply cat_pr1_fmap01_binprod.
+      refine ((cat_assoc _ _ _)^$ $@ _ $@ cat_assoc _ _ _).
+      refine ((_ $@R _) $@ _ $@ (_^$ $@R _)).
+      1: apply cat_binprod_beta_pr1.
+      2: apply cat_pr1_fmap01_binprod.
+      refine ((cat_assoc _ _ _)^$ $@ _ $@ cat_assoc _ _ _).
+      refine (_ $@ _).
+      { do 2 refine (cat_assoc _ _ _ $@ _).
+        refine (_ $@L _).
+        refine ((cat_assoc _ _ _)^$ $@ _).
+        refine ((_ $@R _) $@ _).
+        1: apply cat_binprod_beta_pr2.
+        refine ((cat_assoc _ _ _)^$ $@ _).
+        refine ((_ $@R _) $@ _).
+        1: apply cat_binprod_beta_pr1.
+        refine (cat_assoc _ _ _ $@ (_ $@L _) $@ _).
+        1: apply cat_pr2_fmap01_binprod.
+        refine ((cat_assoc _ _ _)^$ $@ (_ $@R _)).
+        apply cat_binprod_beta_pr1. }
+      refine (_ $@ (_^$ $@R _)).
+      2: apply cat_binprod_beta_pr1.
+      refine (_ $@ (cat_assoc _ _ _)^$).
+      refine (_ $@ (_ $@L _^$)).
+      2: apply cat_pr2_fmap01_binprod.
+      refine (_ $@ cat_assoc _ _ _).
+      refine (_ $@ (_^$ $@R _)).
+      2: apply cat_binprod_beta_pr1.
+      symmetry; apply cat_assoc.
+    - refine ((cat_assoc _ _ _)^$ $@ _ $@ cat_assoc _ _ _).
+      refine ((_ $@R _) $@ _ $@ (_^$ $@R _)).
+      1,3: apply cat_pr2_fmap01_binprod.
+      refine (cat_assoc _ _ _ $@ _ $@ (cat_assoc _ _ _)^$).
+      refine ((_ $@L _) $@ _).
+      { refine ((cat_assoc _ _ _)^$ $@ (_ $@R _)).
+        apply cat_binprod_beta_pr2. }
+      refine (_ $@ (_ $@L _)).
+      2: { refine ((_^$ $@R _) $@ cat_assoc _ _ _).
+        apply cat_pr2_fmap01_binprod. }
+      apply cat_binprod_eta_pr.
+      + refine ((cat_assoc _ _ _)^$ $@ _ $@ cat_assoc _ _ _).
+        refine ((_ $@R _) $@ _ $@ (_^$ $@R _)).
+        1,3: apply cat_binprod_beta_pr1.
+        refine ((cat_assoc _ _ _)^$ $@ (_ $@R _) $@ _ $@ (cat_assoc _ _ _)^$).
+        1: apply cat_pr2_fmap01_binprod.
+        refine (cat_assoc _ _ _ $@ _).
+        refine ((_ $@L ((cat_assoc _ _ _)^$ $@ (_ $@R _))) $@ _).
+        1: apply cat_binprod_beta_pr2.
+        refine (_ $@ (_ $@L _)).
+        2: { do 2 refine ((_ $@R _) $@ cat_assoc _ _ _).
+          symmetry.
+          apply cat_binprod_beta_pr2. }
+        refine (_ $@ cat_assoc _ _ _).
+        refine (_ $@ (_ $@R _)).
+        2: { do 2 refine ((_ $@R _) $@ (cat_assoc _ _ _)).
+          symmetry.
+          apply cat_binprod_beta_pr1. }
+        do 2 refine (_ $@ (cat_assoc _ _ _)^$).
+        refine ((_ $@L _) $@ _).
+        { refine ((cat_assoc _ _ _)^$ $@ (_ $@R _)).
+          apply cat_binprod_beta_pr1. }
+        refine (_ $@ (_ $@L (_ $@L _))).
+        2: { refine ((_^$ $@R _) $@ cat_assoc _ _ _).
+          apply cat_binprod_beta_pr2. }
+        refine (_ $@ (_ $@L _)).
+        2: { refine ((_^$ $@R _) $@ cat_assoc _ _ _).
+          apply cat_binprod_beta_pr2. }
+        refine (_ $@ (_ $@L _)).
+        2: { refine ((_ $@L _^$) $@ (cat_assoc _ _ _)^$).
+          apply cat_binprod_beta_pr2. }
+        refine (_ $@ (_ $@L _)).
+        2: { refine ((_^$ $@R _) $@ cat_assoc _ _ _).
+          apply cat_binprod_beta_pr2. }
+        refine (_ $@ (_^$ $@R _) $@ cat_assoc _ _ _).
+        2: apply cat_binprod_beta_pr2.
+        refine ((_ $@L _) $@ _).
+        { refine (cat_assoc _ _ _ $@ (_ $@L _)).
+          apply cat_binprod_beta_pr2. }
+        refine ((_ $@L _) $@ _).
+        1: refine ((cat_assoc _ _ _)^$ $@ (_ $@R _)).
+        1: apply cat_binprod_beta_pr1.
+        symmetry; apply cat_assoc.
+      + refine ((cat_assoc _ _ _)^$ $@ _ $@ cat_assoc _ _ _).
+        refine ((_ $@R _) $@ _ $@ (_^$ $@R _)).
+        1,3: apply cat_binprod_beta_pr2.
+        refine ((cat_assoc _ _ _)^$ $@ ((_ $@ _) $@R _) $@ _).
+        1: apply cat_binprod_beta_pr1.
+        1: apply cat_idl.
+        refine ((cat_assoc _ _ _)^$ $@ (_ $@R _) $@ _).
+        1: apply cat_binprod_beta_pr1.
+        refine ((cat_assoc _ _ _)^$ $@ (_ $@R _) $@ _).
+        1: apply cat_binprod_beta_pr2.
+        refine (_ $@ (_ $@L _)).
+        2: { refine ((_^$ $@R _) $@ cat_assoc _ _ _).
+          refine (cat_assoc _ _ _ $@ (_ $@L _)).
+          apply cat_binprod_beta_pr2. }
+        refine (_ $@ cat_assoc _ _ _).
+        refine (_ $@ (_ $@R _)).
+        2: refine (cat_assoc _ _ _).
+        repeat refine (_ $@ (cat_assoc _ _ _)^$).
+        apply cat_binprod_eta_pr.
+        * refine ((cat_assoc _ _ _)^$ $@ _ $@ cat_assoc _ _ _).
+          refine ((_ $@R _) $@ _ $@ (_^$ $@R _)).
+          1,3: apply cat_pr1_fmap01_binprod.
+          nrefine (cat_pr1_fmap01_binprod _ _ $@ _ $@ cat_assoc _ _ _).
+          refine (_ $@ (_^$ $@R _)).
+          2: apply cat_pr1_fmap01_binprod.
+          refine (_^$ $@ (_^$ $@R _) $@ cat_assoc _ _ _).
+          2: apply cat_pr1_fmap01_binprod.
+          apply cat_pr1_fmap01_binprod.
+        * refine ((cat_assoc _ _ _)^$ $@ _ $@ cat_assoc _ _ _).
+          refine ((_ $@R _) $@ _ $@ (_^$ $@R _)).
+          1,3: apply cat_pr2_fmap01_binprod.
+          refine (cat_assoc _ _ _ $@ _ $@ (cat_assoc _ _ _)^$).
+          refine ((_ $@L _) $@ _).
+          1: apply cat_pr2_fmap01_binprod.
+          refine ((cat_assoc _ _ _)^$ $@ (_ $@R _) $@ _).
+          1: apply cat_binprod_beta_pr2.
+          refine (_ $@ (_ $@L _)).
+          2: { refine ((_^$ $@R _) $@ cat_assoc _ _ _).
+            apply cat_pr2_fmap01_binprod. }
+          refine (_ $@ cat_assoc _ _ _).
+          refine (_ $@ ((_^$ $@ _) $@R _)).
+          3: apply cat_assoc.
+          2: refine (_ $@R _).
+          2: apply cat_binprod_beta_pr2.
+          refine (_ $@ cat_assoc _ _ _).
+          refine (_ $@ ((_^$ $@ _^$) $@R _)).
+          3: apply cat_assoc.
+          2: refine (_ $@L _).
+          2: apply cat_pr2_fmap01_binprod.
+          refine (_ $@ (_ $@L ((_ $@L _^$) $@ (cat_assoc _ _ _)^$))
+            $@ (cat_assoc _ _ _)^$).
+          2: apply cat_pr2_fmap01_binprod.
+          refine (_ $@ (_ $@L (_ $@ _))).
+          3: apply cat_assoc.
+          2: refine (_^$ $@R _).
+          2: apply cat_binprod_beta_pr2.
+          refine ((_^$ $@R _) $@ cat_assoc _ _ _).
+          apply cat_pr1_fmap01_binprod.
+  Defined.
+
+  Local Instance hexagon_identity
+    : HexagonIdentity (fun x y => cat_binprod x y).
+  Proof.
+    snrapply hexagon_twist.
+    intros a b c.
+    refine (cat_assoc _ _ _ $@ _ $@ (cat_assoc _ _ _)^$).
+    snrapply cat_binprod_eta_pr.
+    - refine ((cat_assoc _ _ _)^$ $@ (_ $@R _)
+        $@ _ $@ (_^$ $@R _) $@ cat_assoc _ _ _).
+      1: apply cat_pr1_fmap01_binprod.
+      2: apply cat_binprod_beta_pr1.
+      refine ((cat_assoc _ _ _)^$ $@ (_ $@R _)
+        $@ _ $@ ((cat_assoc _ _ _ $@ (_ $@L _))^$ $@R _) $@ cat_assoc _ _ _).
+      1: apply cat_binprod_beta_pr1.
+      2: apply cat_pr2_fmap01_binprod.
+      nrefine (cat_assoc _ _ _ $@ (_ $@L _) $@ _). 
+      1: apply cat_pr2_fmap01_binprod.
+      refine (_ $@  (_ $@L (cat_assoc _ _ _)^$) $@ (cat_assoc _ _ _)^$).
+      refine (_ $@ (_ $@@ _)^$ $@ cat_assoc _ _ _).
+      2: apply cat_binprod_beta_pr2.
+      2: apply cat_binprod_beta_pr1.
+      refine ((cat_assoc _ _ _)^$ $@ (_ $@R _) $@ _^$).
+      1: apply cat_binprod_beta_pr1.
+      apply cat_pr2_fmap01_binprod.
+    - refine ((cat_assoc _ _ _)^$ $@ (_ $@R _)
+        $@ _ $@ (_^$ $@R _) $@ cat_assoc _ _ _).
+      1: apply cat_pr2_fmap01_binprod.
+      2: apply cat_binprod_beta_pr2.
+      nrefine (cat_assoc _ _ _ $@ (_ $@L _) $@ _).
+      { refine ((cat_assoc _ _ _)^$ $@ (_ $@R _)).
+        apply cat_binprod_beta_pr2. }
+      snrapply cat_binprod_eta_pr.
+      + refine ((cat_assoc _ _ _)^$ $@ (_ $@R _)
+          $@ _ $@ (_^$ $@R _) $@ cat_assoc _ _ _).
+        1: apply cat_binprod_beta_pr1.
+        2: apply cat_pr1_fmap01_binprod.
+        refine ((cat_assoc _ _ _)^$ $@ (_ $@R _)
+          $@ _ $@ (_^$ $@R _) $@ cat_assoc _ _ _).
+        1: apply cat_pr2_fmap01_binprod.
+        2: apply cat_pr1_fmap01_binprod.
+        refine (cat_assoc _ _ _ $@ (_ $@L _) $@ _ $@ _^$).
+        1: apply cat_pr2_fmap01_binprod.
+        2: apply cat_binprod_beta_pr1.
+        refine ((cat_assoc _ _ _)^$ $@ (_ $@R _)).
+        apply cat_binprod_beta_pr2.
+      + refine ((cat_assoc _ _ _)^$ $@ (_ $@R _)
+          $@ _ $@ (_^$ $@R _) $@ cat_assoc _ _ _).
+        1: apply cat_binprod_beta_pr2.
+        2: apply cat_pr2_fmap01_binprod.
+        refine ((cat_assoc _ _ _)^$ $@ (_ $@R _)
+          $@ _ $@ ((cat_assoc _ _ _ $@ (_ $@L _))^$ $@R _) $@ cat_assoc _ _ _).
+        1: apply cat_pr1_fmap01_binprod.
+        2: apply cat_pr2_fmap01_binprod.
+        nrefine (cat_pr1_fmap01_binprod _ _ $@ _).
+        refine (_ $@ (cat_assoc _ _ _)^$).
+        refine (_ $@ (_ $@L cat_assoc _ _ _)^$).
+        nrefine (_ $@ cat_assoc _ _ _).
+        refine ((_ $@@ _) $@ _)^$.
+        1,2: apply cat_binprod_beta_pr2.
+        apply cat_pr1_fmap01_binprod.
+  Defined.
+
+  Global Instance ismonoidal_binprod
+    : IsMonoidal A (fun x y => cat_binprod x y) unit
+    := {}.
+  
+  Global Instance issymmetricmonoidal_binprod
+    : IsSymmetricMonoidal A (fun x y => cat_binprod x y) unit
+    := {}.
+
 End Associativity.
+
+(** *** Products in Type *)
+
+(** Since we use the Yoneda lemma in this file, we therefore depend on WildCat.Universe which means these instances have to live here. *)
+Global Instance hasbinaryproducts_type : HasBinaryProducts Type.
+Proof.
+  intros X Y.
+  snrapply Build_BinaryProduct.
+  - exact (X * Y).
+  - exact fst.
+  - exact snd.
+  - intros Z f g z. exact (f z, g z).
+  - reflexivity.
+  - reflexivity.
+  - intros Z f g p q x.
+    apply path_prod.
+    + exact (p x).
+    + exact (q x).
+Defined.
+
+(** Assuming [Funext], [Type] has all products. *)
+Global Instance hasallproducts_type `{Funext} : HasAllProducts Type.
+Proof.
+  intros I x.
+  snrapply Build_Product.
+  - exact (forall (i : I), x i).
+  - intros i f. exact (f i).
+  - intros A f a i. exact (f i a).
+  - reflexivity.
+  - intros A f g p a.
+    exact (path_forall _ _ (fun i => p i a)).
+Defined.