proposition: Lemma adjunction_postcomp (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: Proof. intros adj. srapply Build_Adjunction_unit_counit. - snrapply Build_NatTrans. + intros K. exact (nattrans_prewhisker (adjunction_unit adj) K). + 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). + 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.
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