fact: Definition cat_prod_diag {A : Type} `{Is1Cat A} (x : A) `{!BinaryProduct x x} : x $-> cat_prod x x := cat_prod_corec (Id _) (Id _).
imports: Basics EquivGpd Types.Prod WildCat.Core WildCat.ZeroGroupoid WildCat.Equiv WildCat.Yoneda WildCat.Universe WildCat.NatTrans WildCat.Opposite