diff --git a/test/WildCat/Opposite.v b/test/WildCat/Opposite.v
index a6dc6fa2395..f505a900772 100644
--- a/test/WildCat/Opposite.v
+++ b/test/WildCat/Opposite.v
@@ -2,9 +2,10 @@ From HoTT Require Import Basics WildCat.Core WildCat.Opposite.
 
 (* Opposites are (almost) definitionally involutive. *)
 
-Definition test1 A `{Is01Cat A} : A = (A^op)^op := 1.
-Definition test2 A `{x : Is01Cat A} : x = is01cat_op (A := A^op) := 1.
-Definition test3 A `{x : Is2Graph A} : x = is2graph_op (A := A^op) := 1.
+Definition test1 A : A = (A^op)^op :> Type := 1.
+Definition test2 A `{x : IsGraph A} : x = isgraph_op (A := A^op) := 1.
+Definition test3 A `{x : Is01Cat A} : x = is01cat_op (A := A^op) := 1.
+Definition test4 A `{x : Is2Graph A} : x = is2graph_op (A := A^op) := 1.
 
 (** Is1Cat is not definitionally involutive. *)
 Fail Definition test4 A `{x : Is1Cat A} : x = is1cat_op (A := A^op) := 1.
diff --git a/theories/Algebra/Groups/FreeProduct.v b/theories/Algebra/Groups/FreeProduct.v
index 76256713f25..3c4c1fe093b 100644
--- a/theories/Algebra/Groups/FreeProduct.v
+++ b/theories/Algebra/Groups/FreeProduct.v
@@ -716,7 +716,6 @@ Defined.
 (** The freeproduct is the coproduct in the category of groups. *)
 Global Instance hasbinarycoproducts : HasBinaryCoproducts Group.
 Proof.
-  snrapply Build_HasBinaryCoproducts.
   intros G H.
   snrapply Build_BinaryCoproduct.
   - exact (FreeProduct G H).
diff --git a/theories/Algebra/Groups/Group.v b/theories/Algebra/Groups/Group.v
index 972abc7ad6d..d417140ba25 100644
--- a/theories/Algebra/Groups/Group.v
+++ b/theories/Algebra/Groups/Group.v
@@ -716,7 +716,6 @@ Global Instance issurj_grp_prod_pr2 {G H : Group}
 
 Global Instance hasbinaryproducts_group : HasBinaryProducts Group.
 Proof.
-  snrapply Build_HasBinaryProducts.
   intros G H.
   snrapply Build_BinaryProduct.
   - exact (grp_prod G H).
diff --git a/theories/Homotopy/Wedge.v b/theories/Homotopy/Wedge.v
index 41080fd8828..73280acedb6 100644
--- a/theories/Homotopy/Wedge.v
+++ b/theories/Homotopy/Wedge.v
@@ -74,7 +74,6 @@ Defined.
 
 Global Instance hasbinarycoproducts : HasBinaryCoproducts pType.
 Proof.
-  snrapply Build_HasBinaryCoproducts.
   intros X Y.
   snrapply Build_BinaryCoproduct.
   - exact (X \/ Y).
diff --git a/theories/Pointed/Core.v b/theories/Pointed/Core.v
index 9055a6dc5ae..23664df8729 100644
--- a/theories/Pointed/Core.v
+++ b/theories/Pointed/Core.v
@@ -654,7 +654,6 @@ Defined.
 (** pType has binary products *)
 Global Instance hasbinaryproducts_ptype : HasBinaryProducts pType.
 Proof.
-  snrapply Build_HasBinaryProducts.
   intros X Y.
   snrapply Build_BinaryProduct.
   - exact (X * Y).
diff --git a/theories/WildCat/Coproducts.v b/theories/WildCat/Coproducts.v
index 89253b41629..6b34f35e336 100644
--- a/theories/WildCat/Coproducts.v
+++ b/theories/WildCat/Coproducts.v
@@ -3,11 +3,10 @@ Require Import WildCat.Core WildCat.ZeroGroupoid WildCat.Equiv WildCat.Yoneda Wi
 
 (** * Categories with coproducts *)
 
-Class BinaryCoproduct (A : Type) `{Is1Cat A} (x y : A) := Build_BinaryCoproduct' {
-  prod_co_coprod :: BinaryProduct (x : A^op) y
-}.
+Class BinaryCoproduct (A : Type) `{Is1Cat A} (x y : A) :=
+  prod_co_coprod :: BinaryProduct (x : A^op) (y : A^op)
+.
 
-Arguments Build_BinaryCoproduct' {_ _ _ _ _ x y} _.
 Arguments BinaryCoproduct {A _ _ _ _} x y.
 
 Definition cat_coprod {A : Type}  `{Is1Cat  A} (x y : A) `{!BinaryCoproduct x y} : A
@@ -32,15 +31,14 @@ Definition Build_BinaryCoproduct {A : Type} `{Is1Cat A} {x y : A}
   (cat_coprod_beta_inr : forall z (f : x $-> z) (g : y $-> z), cat_coprod_rec z f g $o cat_inr $== g)
   (cat_coprod_in_eta : forall z (f g : cat_coprod $-> z), f $o cat_inl $== g $o cat_inl -> f $o cat_inr $== g $o cat_inr -> f $== g)
   : BinaryCoproduct x y
-  := Build_BinaryCoproduct'
-    (Build_BinaryProduct
+  := Build_BinaryProduct
       (cat_coprod : A^op)
       cat_inl
       cat_inr
       cat_coprod_rec
       cat_coprod_beta_inl
       cat_coprod_beta_inr
-      cat_coprod_in_eta).
+      cat_coprod_in_eta.
 
 Section Lemmata.
 
@@ -118,11 +116,27 @@ Section Lemmata.
 
 End Lemmata.
 
-(** *** Cateogires with binary coproducts *)
+(** *** Categories with binary coproducts *)
 
-Class HasBinaryCoproducts (A : Type) `{Is1Cat A} := {
-  binary_coproducts :: forall x y : A, BinaryCoproduct x y;
-}.
+Class HasBinaryCoproducts (A : Type) `{Is1Cat A} :=
+  binary_coproducts :: forall x y, BinaryCoproduct x y
+.
+
+(** ** Symmetry of coproducts *)
+
+Definition cate_coprod_swap {A : Type} `{HasEquivs A} {e : HasBinaryCoproducts A} (x y : A)
+  : cat_coprod x y $<~> cat_coprod y x.
+Proof.
+  exact (@cate_prod_swap A^op _ _ _ _ _ e _ _).
+Defined.
+
+(** ** Associativity of coproducts *)
+
+Lemma cate_coprod_assoc {A : Type} `{HasEquivs A} {e : HasBinaryCoproducts A} (x y z : A)
+  : cat_coprod x (cat_coprod y z) $<~> cat_coprod (cat_coprod x y) z.
+Proof.
+  exact (@cate_prod_assoc A^op _ _ _ _ _ e x y z)^-1$.
+Defined.
 
 (** *** Coproduct functor *)
 
@@ -133,7 +147,6 @@ Class HasBinaryCoproducts (A : Type) `{Is1Cat A} := {
 (** [Type] has all binary coproducts *)
 Global Instance hasbinarycoproducts_type : HasBinaryCoproducts Type.
 Proof.
-  snrapply Build_HasBinaryCoproducts.
   intros X Y.
   snrapply Build_BinaryCoproduct.
   - exact (X + Y).
diff --git a/theories/WildCat/Products.v b/theories/WildCat/Products.v
index bfeb665eb20..283584cd58b 100644
--- a/theories/WildCat/Products.v
+++ b/theories/WildCat/Products.v
@@ -157,9 +157,9 @@ End Lemmata.
 (** *** Categories with binary products *)
 
 (** A category with binary products is a category with a binary product for each pair of objects. *)
-Class HasBinaryProducts (A : Type) `{Is1Cat A} := {
-  binary_products :: forall x y : A, BinaryProduct x y;
-}.
+Class HasBinaryProducts (A : Type) `{Is1Cat A} :=
+  binary_products :: forall x y : A, BinaryProduct x y
+.
 
 (** *** Symmetry of products *)
 
@@ -200,7 +200,6 @@ End Symmetry.
 
 (** Binary products are functorial in each argument. *)
 
-(* TODO: jdchristensen: Another approach to handling functoriality on the right is to first prove that products are symmetric. Then functoriality on the right follows from functoriality on the left... *)
 Global Instance is0functor_cat_prod_l {A : Type}
   `{HasBinaryProducts A} y
   : Is0Functor (fun x => cat_prod x y).
@@ -307,7 +306,6 @@ Defined.
 (** Since we use the Yoneda lemma in this file, we therefore depend on WildCat.Universe which means this instance has to therefore live here. *)
 Global Instance hasbinaryproducts_type : HasBinaryProducts Type.
 Proof.
-  snrapply Build_HasBinaryProducts.
   intros X Y.
   snrapply Build_BinaryProduct.
   - exact (X * Y).