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