fact: Definition yoneda_issect {A : Type} `{Is1Cat A} (a : A) (F : A^op -> Type) `{!Is0Functor F, !Is1Functor F} (x : F a) : un_yoneda a F (yoneda a F x) = x := opyoneda_issect (A:=A^op) a F x.
imports: Basics.Overture Basics.Tactics WildCat.Core WildCat.Equiv WildCat.Universe WildCat.Opposite WildCat.FunctorCat WildCat.NatTrans WildCat.Prod WildCat.ZeroGroupoid