fact: Definition opyon_faithful {A : Type} `{Is1Cat_Strong A} (a b : A) (f g : b $-> a) (p : forall (c : A) (h : a $-> c), h $o f = h $o g) : f = g := (cat_idl_strong f)^ @ p a (Id a) @ cat_idl_strong g.
imports: Basics.Overture Basics.Tactics WildCat.Core WildCat.Equiv WildCat.Universe WildCat.Opposite WildCat.FunctorCat WildCat.NatTrans WildCat.Prod WildCat.ZeroGroupoid