{A : Type} `{Is1Cat A} (a : A) (F : A -> ZeroGpd) {ff : Is0Functor F} : (opyon_0gpd a $=> F) -> F a := fun alpha => alpha a (Id a). Global Instance is1natural_opyoneda_0gpd {A : Type} `{Is1Cat A} (a : A) (F : A -> ZeroGpd) `{!Is0Functor F, !Is1Functor F} (x : F a) : Is1Natural (opyon_0gpd a) F (opyoneda_0gpd a F x). Proof. snrapply Build_Is1Natural. unfold opyon_0gpd, opyoneda_0gpd; 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.