proposition: Lemma cat_prod_beta_pr1 {z : A} (f : z $-> x) (g : z $-> y) : cat_pr1 $o cat_prod_corec f g $== f.
proof: Proof. exact (fst (cate_isretr cate_cat_prod_corec_inv (f, g))). Defined.
imports: Basics EquivGpd Types.Prod WildCat.Core WildCat.ZeroGroupoid WildCat.Equiv WildCat.Yoneda WildCat.Universe WildCat.NatTrans WildCat.Opposite