{C D : Type} (F : C -> D) (G G' : D -> C) `{HasEquivs C, Is1Cat D, !HasMorExt C, !Is0Functor F, !Is0Functor G, !Is0Functor G'} : NatEquiv G G' -> F ⊣ G -> F ⊣ G'. Proof. intros e adj. snrapply Build_Adjunction_natequiv_nat_left. { intros x. refine (natequiv_compose _ (natequiv_adjunction_r adj _)). rapply (natequiv_postwhisker _ e). } intros y. rapply is1natural_comp. 2: exact _. rapply is1natural_yoneda. 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.