x y g : (equiv_adjunction adj x y)^-1 g = adjunction_unit y $o fmap F g. Proof. epose (n1 := is1natural_natequiv (natequiv_inverse (natequiv_adjunction_l _)) _ _ _ _). clearbody n1; cbv in n1. refine (_ @ n1). by rewrite cat_idl_strong. 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.