proposition: Lemma cate_coprod_assoc {A : Type} `{HasEquivs A} {e : HasBinaryCoproducts A} (x y z : A) : cat_coprod x (cat_coprod y z) $<~> cat_coprod (cat_coprod x y) z.
proof: Proof. exact (@cate_prod_assoc A^op _ _ _ _ _ e x y z)^-1$. Defined.
imports: Basics EquivGpd Types.Prod Types.Sum WildCat.Core WildCat.ZeroGroupoid WildCat.Equiv WildCat.Yoneda WildCat.Universe WildCat.NatTrans WildCat.Opposite WildCat.Products