{f f' : x $-> z} {g g' : y $-> z} : f $== f' -> g $== g' -> cat_bincoprod_rec f g $== cat_bincoprod_rec f' g' := @cat_binprod_corec_eta A^op _ _ _ _ x y _ _ f f' g g'. End Lemmata. Global Instance is0functor_cat_bincoprod_l {A : Type} `{hbc : HasBinaryCoproducts A} y : Is0Functor (A:=A) (fun x => cat_bincoprod x y). Proof. rapply is0functor_op'. exact (is0functor_cat_binprod_l (A:=A^op) (H0:=hbc) y). Defined.
Require Import Basics.Overture Basics.Tactics Basics.Decidable. Require Import Types.Bool. Require Import WildCat.Core WildCat.Equiv WildCat.Forall WildCat.NatTrans