x y f : equiv_adjunction adj x y f = fmap G f $o adjunction_counit x. Proof. refine (_ @ is1natural_equiv_adjunction_r adj _ _ _ _ _). by cbv; rewrite (cat_idr_strong f). Qed.
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.