(y : D) : Is1Natural (yon y o F) (yon (G y)) (is0functor_F := is0functor_compose (A:=C^op) (B:=D^op) (C:=Type) _ _) (is0functor_G := is0functor_yon (G y)) (fun x : C^op => γ x y). Proof. nrapply (is1natural_natequiv (natequiv_inverse (Build_NatEquiv (yon (G y)) (yon y o F) (fun x => (γ x y)^-1$) _))). nrapply is1natural_yoneda. nrapply is1functor_compose. 1: nrapply is1functor_op; exact _. nrapply is1functor_opyon. nrapply hasmorext_op; exact _. Defined.
Require Import Basics.Utf8 Basics.Overture Basics.Tactics Basics.Equivalences. Require Import WildCat.Core. Require Import WildCat.NatTrans. Require Import WildCat.Equiv. Require Import WildCat.Prod. Require Import WildCat.Opposite. Require Import WildCat.Yoneda. Require Import WildCat.FunctorCat. Require Import WildCat.Universe. Require Import Types.Prod.