{-# OPTIONS --lossy-unification #-}
open import Cat.Prelude

import Cat.Reasoning

module Cat.Functor.Adjoint.Compose


# Composition of adjunctionsπ

Suppose we have four functors $F \dashv G$ and $L \dashv R$, such that they βfit togetherβ, i.e.Β the composites $LF$ and $GR$ 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

private
module fg = _β£_ Fβ£G
module lr = _β£_ Lβ£R
module A = Cat.Reasoning A
module B = Cat.Reasoning B
module C = Cat.Reasoning C
module F = Functor F
module G = Functor G
module L = Functor L
module R = Functor R
open _β£_
open _=>_
module LF = Functor (L Fβ F)
module GR = Functor (G Fβ R)

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! (lr.unit.is-natural _ _ _) β©β‘
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! (fg.counit.is-natural _ _ _) β©β‘
lr.counit.Ξ΅ _ C.β β L.β (R.Fβ f B.β fg.counit.Ξ΅ _) β      β‘β¨ ap! (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! (LF.F-β _ _) β©β‘
(lr.counit.Ξ΅ _ C.β L.β (fg.counit.Ξ΅ _)) C.β LF.β (G.β (lr.unit.Ξ· _)) C.β LF.β (fg.unit.Ξ· _)      β‘β¨ cat! C β©β‘
lr.counit.Ξ΅ _ C.β (β L.β (fg.counit.Ξ΅ _) C.β LF.β (G.β (lr.unit.Ξ· _)) β C.β LF.β (fg.unit.Ξ· _))  β‘β¨ ap! (sym (L.F-β _ _) Β·Β· ap L.β (fg.counit.is-natural _ _ _) Β·Β· L.F-β _ _) β©β‘
lr.counit.Ξ΅ _ C.β (L.β (lr.unit.Ξ· _) C.β L.β (fg.counit.Ξ΅ _)) C.β LF.β (fg.unit.Ξ· _)             β‘β¨ cat! 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Β‘ (B.pulll (sym (R.F-β _ _))) β©β‘Λ
G.β (R.β (lr.counit.Ξ΅ _) B.β β R.β (L.β (fg.counit.Ξ΅ _)) B.β lr.unit.Ξ· _ β) A.β fg.unit .Ξ· _  β‘Λβ¨ apΒ‘ (lr.unit.is-natural _ _ _) β©β‘Λ
G.β (β R.β (lr.counit.Ξ΅ _) B.β lr.unit.Ξ· _ B.β fg.counit.Ξ΅ _ β) A.β fg.unit .Ξ· _              β‘β¨ ap! (B.cancell lr.zag) β©β‘
G.β (fg.counit.Ξ΅ _) A.β fg.unit .Ξ· _                                                          β‘β¨ fg.zag β©β‘
A.id                                                                                          β