NatTrans (F o G) idmap. Proof. snrapply Build_NatTrans. { hnf. intros y. exact ((equiv_adjunction adj (G y) y)^-1 (Id _)). } snrapply Build_Is1Natural. intros y y' f. apply GpdHom_path. refine (_^ @ _ @ _). 1: exact (is1natural_natequiv (natequiv_inverse (natequiv_adjunction_l _)) (G y') _ (fmap G f) _). 2: exact (is1natural_natequiv (natequiv_inverse (natequiv_adjunction_r _)) _ _ _ (Id _)). simpl. apply equiv_ap_inv'. 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.