make coproduct definition more definitional

Signed-off-by: Ali Caglayan <[email protected]>

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).

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).

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).

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).

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' {
+Class BinaryCoproduct (A : Type) `{Is1Cat A} (x y : A) :=
   prod_co_coprod :: BinaryProduct (x : A^op) y
-}.
+.
 
-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.
 
@@ -120,9 +118,9 @@ End Lemmata.
 
 (** *** Cateogires 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
+.
 
 (** *** Coproduct functor *)
 
@@ -133,7 +131,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).

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 *)
 
@@ -307,7 +307,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).