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