(A B C : Type) (F : A -> B) (G : B -> A) (F' : B -> C) (G' : C -> B) `{Is1Cat A, HasEquivs B, Is1Cat C} `{!Is0Functor F, !Is0Functor G, !Is0Functor F', !Is0Functor G'} : F ⊣ G -> F' ⊣ G' -> F' o F ⊣ G o G'. Proof. intros adj1 adj2. snrapply Build_Adjunction_natequiv_nat_right. { intros y. nrefine (natequiv_compose (natequiv_adjunction_l adj1 _) _). exact (natequiv_prewhisker (A:=A^op) (B:=B^op) (natequiv_adjunction_l adj2 y) F). } intros x. rapply is1natural_comp. + rapply (is1natural_prewhisker G' (natequiv_adjunction_r adj1 x)). + rapply is1natural_equiv_adjunction_r. 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.