{A : Type} `{Is1Cat A} {x y : A} (cat_binprod : A) (cat_pr1 : cat_binprod $-> x) (cat_pr2 : cat_binprod $-> y) (cat_binprod_corec : forall z : A, z $-> x -> z $-> y -> z $-> cat_binprod) (cat_binprod_beta_pr1 : forall (z : A) (f : z $-> x) (g : z $-> y), cat_pr1 $o cat_binprod_corec z f g $== f) (cat_binprod_beta_pr2 : forall (z : A) (f : z $-> x) (g : z $-> y), cat_pr2 $o cat_binprod_corec z f g $== g) (cat_binprod_eta_pr : forall (z : A) (f g : z $-> cat_binprod), cat_pr1 $o f $== cat_pr1 $o g -> cat_pr2 $o f $== cat_pr2 $o g -> f $== g) : Product Bool (fun b => if b then x else y). Proof. snrapply (Build_Product _ cat_binprod). - intros [|]. + exact cat_pr1. + exact cat_pr2. - intros z f. nrapply cat_binprod_corec. + exact (f true). + exact (f false). - intros z f [|]. + nrapply cat_binprod_beta_pr1. + nrapply cat_binprod_beta_pr2. - 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