fact: Definition cate_cat_prod_corec {z : A} : prod_0gpd (yon_0gpd x z) (yon_0gpd y z) $<~> (yon_0gpd (cat_prod x y) z) := cate_cat_prod_corec_inv^-1$.
imports: Basics EquivGpd Types.Prod WildCat.Core WildCat.ZeroGroupoid WildCat.Equiv WildCat.Yoneda WildCat.Universe WildCat.NatTrans WildCat.Opposite