proposition: Lemma adjunction_compose (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: 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.
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