proposition: Lemma is1natural_γ_r x : Is1Natural (opyon (F x)) (fun x0 : D => opyon x (G x0)) (γ x).
proof: Proof. nrapply is1natural_opyoneda. exact _. Defined.
imports: Basics.Utf8 Basics.Overture Basics.Tactics Basics.Equivalences WildCat.Core WildCat.NatTrans WildCat.Equiv WildCat.Prod WildCat.Opposite WildCat.Yoneda WildCat.FunctorCat WildCat.Universe Types.Prod