NatTrans idmap (G o F). Proof. snrapply Build_NatTrans. { hnf. intros x. exact (equiv_adjunction adj x (F x) (Id _)). } snrapply Build_Is1Natural. intros x x' f. apply GpdHom_path. refine (_^ @ _ @ _). 1: exact (is1natural_equiv_adjunction_l adj _ _ _ f (Id _)). 2: exact (is1natural_equiv_adjunction_r adj _ _ _ (fmap F f) (Id _)). simpl. apply equiv_ap'. apply path_hom. apply Square.vrefl. 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.