proposition: Lemma cat_prod_swap_cat_prod_swap (x y : A) : cat_prod_swap x y $o cat_prod_swap y x $== Id _.
proof: Proof. unfold cat_prod_swap. apply cat_prod_pr_eta. - refine ((cat_assoc _ _ _)^$ $@ _). refine (cat_prod_beta_pr1 _ _ $@R _ $@ _). refine (cat_prod_beta_pr2 _ _ $@ _). exact (cat_idr _)^$. - refine ((cat_assoc _ _ _)^$ $@ _). refine (cat_prod_beta_pr2 _ _ $@R _ $@ _). refine (cat_prod_beta_pr1 _ _ $@ _). exact (cat_idr _)^$. Defined.
imports: Basics EquivGpd Types.Prod WildCat.Core WildCat.ZeroGroupoid WildCat.Equiv WildCat.Yoneda WildCat.Universe WildCat.NatTrans WildCat.Opposite