fact: Definition cat_prod_swap (x y : A) : cat_prod x y $-> cat_prod y x := cat_prod_corec cat_pr2 cat_pr1.
imports: Basics EquivGpd Types.Prod WildCat.Core WildCat.ZeroGroupoid WildCat.Equiv WildCat.Yoneda WildCat.Universe WildCat.NatTrans WildCat.Opposite