proposition: Lemma cate_prod_swap (x y : A) : cat_prod x y $<~> cat_prod y x.
proof: Proof. snrapply cate_adjointify. 1,2: apply cat_prod_swap. all: apply cat_prod_swap_cat_prod_swap. Defined.
imports: Basics EquivGpd Types.Prod WildCat.Core WildCat.ZeroGroupoid WildCat.Equiv WildCat.Yoneda WildCat.Universe WildCat.NatTrans WildCat.Opposite