proposition: Lemma adjunction_natequiv_right {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: 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.
imports: Basics.Utf8 Basics.Overture Basics.Tactics Basics.Equivalences WildCat.Core WildCat.NatTrans WildCat.Equiv WildCat.Prod WildCat.Opposite WildCat.Yoneda WildCat.FunctorCat WildCat.Universe Types.Prod