{I J : Type} {A : Type} `{HasBinaryProducts A} (x : I -> A) (y : J -> A) : Product I x -> Product J y -> Product (I + J) (sum_ind _ x y). Proof. intros p q. snrapply Build_Product. - exact (cat_binprod (cat_prod I x) (cat_prod J y)). - intros [i | j]. + exact (cat_pr _ $o cat_pr1). + exact (cat_pr _ $o cat_pr2). - intros z f. nrapply cat_binprod_corec. + nrapply cat_prod_corec. exact (f o inl). + nrapply cat_prod_corec. exact (f o inr). - intros z f [i | j]. + nrefine (cat_assoc _ _ _ $@ _). nrefine ((_ $@L cat_binprod_beta_pr1 _ _) $@ _). rapply cat_prod_beta. + nrefine (cat_assoc _ _ _ $@ _). nrefine ((_ $@L cat_binprod_beta_pr2 _ _) $@ _). rapply cat_prod_beta. - intros z f g r. rapply cat_binprod_eta_pr. + rapply cat_prod_pr_eta. intros i. exact ((cat_assoc _ _ _)^$ $@ r (inl i) $@ cat_assoc _ _ _). + rapply cat_prod_pr_eta. intros j. exact ((cat_assoc _ _ _)^$ $@ r (inr j) $@ cat_assoc _ _ _). Defined.
Require Import Basics.Equivalences Basics.Overture Basics.Tactics. Require Import Types.Bool Types.Prod Types.Forall. Require Import WildCat.Bifunctor WildCat.Core WildCat.Equiv WildCat.EquivGpd