proposition: Lemma adjunction_natequiv_left {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: 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.
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