fact: Definition cat_prod_corec_inv {A : Type} `{Is1Cat A} (xy x y z : A) (pr1 : xy $-> x) (pr2 : xy $-> y) : yon_0gpd xy z $-> prod_0gpd (yon_0gpd x z) (yon_0gpd y z).
imports: Basics EquivGpd Types.Prod WildCat.Core WildCat.ZeroGroupoid WildCat.Equiv WildCat.Yoneda WildCat.Universe WildCat.NatTrans WildCat.Opposite