(C D J : Type) `{HasEquivs C, HasEquivs D, Is01Cat J} (F : Fun11 C D) (G : Fun11 D C) `{!HasMorExt C, !HasMorExt D, !HasMorExt (Fun01 J C), !HasMorExt (Fun01 J D)} : F ⊣ G -> fun11_fun01_postcomp (A:=J) F ⊣ fun11_fun01_postcomp (A:=J) G. Proof. intros adj. srapply Build_Adjunction_unit_counit. - snrapply Build_NatTrans. + intros K. exact (nattrans_prewhisker (adjunction_unit adj) K). + snrapply Build_Is1Natural. intros K K' θ j. apply GpdHom_path. refine (_ @ is1natural_natequiv (natequiv_inverse (natequiv_adjunction_r adj _)) _ _ _ _). refine ((is1natural_natequiv (natequiv_inverse (natequiv_adjunction_l adj _)) _ _ _ _)^ @ _). cbn; rapply ap. refine(cat_idl_strong _ @ _^). apply cat_idr_strong. - snrapply Build_NatTrans. + intros K. exact (nattrans_prewhisker (adjunction_counit adj) K). + snrapply Build_Is1Natural. intros K K' θ j. apply GpdHom_path. refine (_ @ is1natural_natequiv (natequiv_adjunction_r adj _) _ _ _ _). refine ((is1natural_natequiv (natequiv_adjunction_l adj _) _ _ _ _)^ @ _). cbn; rapply ap. refine(cat_idl_strong _ @ _^). apply cat_idr_strong. - exact (trans_prewhisker (adjunction_triangle1 adj)). - exact (trans_prewhisker (adjunction_triangle2 adj)). 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.