open import Cat.Functor.Adjoint
open import Cat.Prelude

import Cat.Reasoning

module Cat.Functor.Adjoint.Compose

Composition of adjunctionsπŸ”—

Suppose we have four functors F⊣GF \dashv G and L⊣RL \dashv R, such that they β€œfit together,” i.e.Β the composites LFLF and GRGR both exist. What can we say about their composites? The hope is that they would again be adjoints, and this is indeed the case.

We prove this here by explicitly exhibiting the adjunction natural transformations and the triangle identities, which is definitely suboptimal for readability, but is the most efficient choice in terms of the resulting Agda program.

    {o β„“ oβ‚‚ β„“β‚‚ o₃ ℓ₃}
    {A : Precategory o β„“} {B : Precategory oβ‚‚ β„“β‚‚}
    {C : Precategory o₃ ℓ₃}
    {F : Functor A B} {G : Functor B A}
    {L : Functor B C} {R : Functor C B}
    (F⊣G : F ⊣ G)
    (L⊣R : L ⊣ R)
  where
LF⊣GR : (L F∘ F) ⊣ (G F∘ R)
LF⊣GR .unit .Ξ· x          = G.₁ (lr.unit.Ξ· _) A.∘ fg.unit.Ξ· _
LF⊣GR .counit .Ξ· x        = lr.counit.Ξ΅ _ C.∘ L.₁ (fg.counit.Ξ΅ _)

LF⊣GR .unit .is-natural x y f = path where abstract
  path : LF⊣GR .unit .Ξ· y A.∘ f ≑ GR.₁ (LF.₁ f) A.∘ LF⊣GR .unit .Ξ· x
  path =
    (G.₁ (lr.unit.Ξ· _) A.∘ fg.unit.Ξ· _) A.∘ f                β‰‘βŸ¨ A.pullr (fg.unit.is-natural _ _ _) βŸ©β‰‘
    G.₁ (lr.unit.Ξ· _) A.∘ G.₁ (F.₁ f) A.∘ fg.unit.Ξ· _        β‰‘βŸ¨ A.pulll (sym (G.F-∘ _ _)) βŸ©β‰‘
    G.₁ (lr.unit.Ξ· _ B.∘ F.₁ f) A.∘ fg.unit.Ξ· _              β‰‘βŸ¨ apβ‚‚ A._∘_ (ap G.₁ (lr.unit.is-natural _ _ _)) refl βŸ©β‰‘
    G.₁ (R.₁ (L.₁ (F.₁ f)) B.∘ lr.unit .Ξ· _) A.∘ fg.unit.Ξ· _ β‰‘βŸ¨ A.pushl (G.F-∘ _ _) βŸ©β‰‘
    GR.₁ (LF.₁ f) A.∘ G.₁ (lr.unit.Ξ· _) A.∘ (fg.unit.Ξ· _)    ∎

LF⊣GR .counit .is-natural x y f = path where abstract
  path : LF⊣GR .counit .Ξ· y C.∘ LF.₁ (GR.₁ f) ≑ f C.∘ LF⊣GR .counit .Ξ· x
  path =
    (lr.counit.Ξ΅ _ C.∘ L.₁ (fg.counit.Ξ΅ _)) C.∘ LF.₁ (GR.₁ f) β‰‘βŸ¨ C.pullr (sym (L.F-∘ _ _)) βŸ©β‰‘
    lr.counit.Ξ΅ _ C.∘ L.₁ (fg.counit.Ξ΅ _ B.∘ F.₁ (GR.₁ f))    β‰‘βŸ¨ ap (lr.counit.Ξ΅ _ C.∘_) (ap L.₁ (fg.counit.is-natural _ _ _)) βŸ©β‰‘
    lr.counit.Ξ΅ _ C.∘ L.₁ (R.F₁ f B.∘ fg.counit.Ξ΅ _)          β‰‘βŸ¨ ap (lr.counit.Ξ΅ _ C.∘_) (L.F-∘ _ _) βŸ©β‰‘
    lr.counit.Ξ΅ _ C.∘ L.₁ (R.F₁ f) C.∘ L.₁ (fg.counit.Ξ΅ _)    β‰‘βŸ¨ C.extendl (lr.counit.is-natural _ _ _) βŸ©β‰‘
    f C.∘ lr.counit.Ξ΅ _ C.∘ L.₁ (fg.counit.Ξ΅ _)               ∎

LF⊣GR .zig =
  (lr.counit.Ξ΅ _ C.∘ L.₁ (fg.counit.Ξ΅ _)) C.∘ LF.₁ (G.₁ (lr.unit.Ξ· _) A.∘ fg.unit.Ξ· _)           β‰‘βŸ¨ apβ‚‚ C._∘_ refl (LF.F-∘ _ _) βŸ©β‰‘
  (lr.counit.Ξ΅ _ C.∘ L.₁ (fg.counit.Ξ΅ _)) C.∘ LF.₁ (G.₁ (lr.unit.Ξ· _)) C.∘ LF.₁ (fg.unit.Ξ· _)    β‰‘βŸ¨ solve C βŸ©β‰‘
  lr.counit.Ξ΅ _ C.∘ ((L.₁ (fg.counit.Ξ΅ _) C.∘ LF.₁ (G.₁ (lr.unit.Ξ· _))) C.∘ LF.₁ (fg.unit.Ξ· _))  β‰‘βŸ¨ apβ‚‚ C._∘_ refl (apβ‚‚ C._∘_ (sym (L.F-∘ _ _) Β·Β· ap L.₁ (fg.counit.is-natural _ _ _) Β·Β· L.F-∘ _ _) refl) βŸ©β‰‘
  lr.counit.Ξ΅ _ C.∘ (L.₁ (lr.unit.Ξ· _) C.∘ L.₁ (fg.counit.Ξ΅ _)) C.∘ LF.₁ (fg.unit.Ξ· _)           β‰‘βŸ¨ solve C βŸ©β‰‘
  (lr.counit.Ξ΅ _ C.∘ L.₁ (lr.unit.Ξ· _)) C.∘ (L.₁ (fg.counit.Ξ΅ _) C.∘ LF.₁ (fg.unit.Ξ· _))         β‰‘βŸ¨ apβ‚‚ C._∘_ lr.zig (sym (L.F-∘ _ _) βˆ™ ap L.₁ fg.zig βˆ™ L.F-id) βŸ©β‰‘
  C.id C.∘ C.id                                                                                  β‰‘βŸ¨ C.eliml refl βŸ©β‰‘
  C.id                                                                                           ∎

LF⊣GR .zag =
  GR.₁ (lr.counit.Ξ΅ _ C.∘ L.₁ (fg.counit.Ξ΅ _)) A.∘ G.₁ (lr.unit.Ξ· _) A.∘ fg.unit .Ξ· _       β‰‘βŸ¨ A.pulll (sym (G.F-∘ _ _)) βŸ©β‰‘
  G.₁ (R.₁ (lr.counit.Ξ΅ _ C.∘ L.₁ (fg.counit.Ξ΅ _)) B.∘ lr.unit.Ξ· _) A.∘ fg.unit .Ξ· _        β‰‘βŸ¨ apβ‚‚ A._∘_ (ap G.₁ (sym (B.pulll (sym (R.F-∘ _ _))))) refl βŸ©β‰‘
  G.₁ (R.₁ (lr.counit.Ξ΅ _) B.∘ R.₁ (L.₁ (fg.counit.Ξ΅ _)) B.∘ lr.unit.Ξ· _) A.∘ fg.unit .Ξ· _  β‰‘βŸ¨ apβ‚‚ A._∘_ (ap G.₁ (apβ‚‚ B._∘_ refl (sym (lr.unit.is-natural _ _ _)))) refl βŸ©β‰‘
  G.₁ (R.₁ (lr.counit.Ξ΅ _) B.∘ lr.unit.Ξ· _ B.∘ fg.counit.Ξ΅ _) A.∘ fg.unit .Ξ· _              β‰‘βŸ¨ apβ‚‚ A._∘_ (ap G.₁ (B.cancell lr.zag)) refl βŸ©β‰‘
  G.₁ (fg.counit.Ξ΅ _) A.∘ fg.unit .Ξ· _                                                      β‰‘βŸ¨ fg.zag βŸ©β‰‘
  A.id                                                                                      ∎