{A : Type} `{HasBinaryProducts A} : HasProducts Bool A. Proof. intros x. snrapply Build_Product. - exact (cat_binprod (x true) (x false)). - intros [|]. + exact cat_pr1. + exact cat_pr2. - intros z f. exact (cat_binprod_corec (f true) (f false)). - intros z f [|]. + exact (cat_binprod_beta_pr1 (f true) (f false)). + exact (cat_binprod_beta_pr2 (f true) (f false)). - intros z f g p. nrapply cat_binprod_eta_pr. + exact (p true). + exact (p false). 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