fact: Definition un_yoneda_0gpd {A : Type} `{Is1Cat A} (a : A) (F : A^op -> ZeroGpd) {ff : Is0Functor F} : (yon_0gpd a $=> F) -> F a := un_opyoneda_0gpd (A:=A^op) a F.
imports: Basics.Overture Basics.Tactics WildCat.Core WildCat.Equiv WildCat.Universe WildCat.Opposite WildCat.FunctorCat WildCat.NatTrans WildCat.Prod WildCat.ZeroGroupoid