{A : Type} `{Is1Cat A} `{!HasBinaryCoproducts A} {a b c : A} (f : a $-> c) (g : b $-> c) : cat_bincoprod_rec f g $o cat_bincoprod_swap b a $== cat_bincoprod_rec g f := @cat_binprod_swap_corec A^op _ _ _ _ hasbinaryproducts_op_hasbinarycoproducts _ _ _ _ _. Global Instance ismonoidal_cat_bincoprod {A : Type} `{HasEquivs A} `{!HasBinaryCoproducts A} (zero : A) `{!IsInitial zero} : IsMonoidal A (fun x y => cat_bincoprod x y) zero | 10. Proof. nrapply ismonoidal_op'. nrapply (ismonoidal_cat_binprod (A:=A^op) zero). by nrapply isterminal_op_isinitial. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Decidable. Require Import Types.Bool. Require Import WildCat.Core WildCat.Equiv WildCat.Forall WildCat.NatTrans