(I : Type) {A : Type} `{Is1Cat A} {x : I -> A} (cat_prod : A) (cat_pr : forall i : I, cat_prod $-> x i) (cat_prod_corec : forall z : A, (forall i : I, z $-> x i) -> (z $-> cat_prod)) (cat_prod_beta_pr : forall (z : A) (f : forall i, z $-> x i) (i : I), cat_pr i $o cat_prod_corec z f $== f i) (cat_prod_eta_pr : forall (z : A) (f g : z $-> cat_prod), (forall i : I, cat_pr i $o f $== cat_pr i $o g) -> f $== g) : Product I x. Proof. snrapply (' I A _ _ _ _ _ cat_prod cat_pr). intros z. nrapply isequiv_0gpd_issurjinj. nrapply Build_IsSurjInj. - intros f. exists (cat_prod_corec z f). intros i. nrapply cat_prod_beta_pr. - intros f g p. by nrapply cat_prod_eta_pr. 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