Transformation (nattrans_comp (nattrans_prewhisker adjunction_unit F) (nattrans_postwhisker F adjunction_counit)) (nattrans_id _). Proof. intros c. change (?x $-> _) with (x $-> Id (F c)). rewrite <- (eissect (equiv_adjunction adj _ _) (Id (F c))). cbv;rewrite <- (triangle_helper2 _ (F c) (adjunction_counit _)). exact (Id _). 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.