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