{A : Type} `{Is01Cat A} (a : A) (F : A -> Type) {ff : Is0Functor F} : (opyon a $=> F) -> F a := fun alpha => alpha a (Id a). Global Instance is1natural_opyoneda {A : Type} `{Is1Cat A} (a : A) (F : A -> Type) `{!Is0Functor F, !Is1Functor F} (x : F a) : Is1Natural (opyon a) F (opyoneda a F x). Proof. snrapply Build_Is1Natural. unfold opyon, opyoneda; intros b c f g; cbn in *. exact (fmap_comp F g f x). Defined.
Require Import Basics.Overture Basics.Tactics. Require Import WildCat.Core. Require Import WildCat.Equiv. Require Import WildCat.Universe. Require Import WildCat.Opposite. Require Import WildCat.FunctorCat. Require Import WildCat.NatTrans. Require Import WildCat.Prod. Require Import WildCat.Bifunctor. Require Import WildCat.ZeroGroupoid.