proposition: Lemma cate_prod_assoc (x y z : A) : cat_prod x (cat_prod y z) $<~> cat_prod (cat_prod x y) z.
proof: Proof. refine (cate_prod_swap _ _ $oE _). refine (cate_prod_twist _ _ _ $oE _). refine (emap (fun y => cat_prod x y) _). exact (cate_prod_swap _ _). Defined.
imports: Basics EquivGpd Types.Prod WildCat.Core WildCat.ZeroGroupoid WildCat.Equiv WildCat.Yoneda WildCat.Universe WildCat.NatTrans WildCat.Opposite