open import Cat.Diagram.Colimit.Base
open import Cat.Diagram.Limit.Finite
open import Cat.Diagram.Limit.Base
open import Cat.Instances.Functor
open import Cat.Diagram.Terminal
open import Cat.Diagram.Initial
open import Cat.Functor.Adjoint
open import Cat.Diagram.Duals
open import Cat.Functor.Base
open import Cat.Prelude

open import Data.Bool

module Cat.Functor.Adjoint.Continuous where


# Continuity of adjoints🔗

We prove that every functor $R : \ca{D} \to \ca{C}$ admitting a left adjoint $L \dashv R$ preserves every limit which exists in $\ca{D}$. We then instantiate this theorem to the “canonical” shapes of limit: terminal objects, products, pullbacks and equalisers.

  module _ {od ℓd} {J : Precategory od ℓd} {F : Functor J D} where


## Passing cones along🔗

The first thing we prove is that, given a cone over a diagram $F$ in $\ca{D}$, we can get a cone in $\ca{C}$ over $R \circ F$, by passing both the apex and the morphisms “over” using $R$. In reality, this is just the canonically-defined action of $R$ on cones over $F$:

    cone-right-adjoint : Cone F → Cone (R F∘ F)
cone-right-adjoint = F-map-cone R


Conversely, if we have a cone over $R \circ F$, we can turn that into a cone for $F$. In this direction, we use $L$ on the apex, but we must additionally use the adjunction counit to “adjust” the cone maps (that’s ψ).

    right-adjoint-cone : Cone (R F∘ F) → Cone F
right-adjoint-cone K .apex     = L.₀ (K .apex)
right-adjoint-cone K .ψ x      = adj.counit.ε _ D.∘ L.₁ (K .ψ x)
right-adjoint-cone K .commutes {x} {y} f =
F.₁ f D.∘ adj.counit.ε _ D.∘ L.₁ (K .ψ x)                    ≡⟨ D.extendl (sym (adj.counit.is-natural _ _ _)) ⟩≡
adj.counit.ε (F.₀ y) D.∘ L.₁ (R.₁ (F.₁ f)) D.∘ L.₁ (K .ψ x)  ≡˘⟨ ap (λ e → adj.counit.ε _ D.∘ e) (L.F-∘ _ _) ⟩≡˘
adj.counit.ε (F.₀ y) D.∘ L.₁ (R.₁ (F.₁ f) C.∘ K .ψ x)        ≡⟨ ap (λ e → adj.counit.ε _ D.∘ L.₁ e) (K .commutes f) ⟩≡
adj.counit.ε _ D.∘ L.₁ _                                     ∎


The key fact is that we can also pass homomorphisms along, both ways!

    cone-hom-right-adjoint
: {K : Cone (R F∘ F)} {K′ : Cone F}
→ Cone-hom F (right-adjoint-cone K) K′
→ Cone-hom (R F∘ F) K (cone-right-adjoint K′)
cone-hom-right-adjoint map .hom = R.₁ (map .hom) C.∘ adj.unit.η _
cone-hom-right-adjoint {K = K} {K′ = K′} map .commutes o =
R.₁ (K′ .ψ o) C.∘ R.₁ (map .hom) C.∘ adj.unit.η _                 ≡⟨ C.pulll (sym (R.F-∘ _ _)) ⟩≡
R.₁ (K′ .ψ o D.∘ map .hom) C.∘ adj.unit.η _                       ≡⟨ ap (λ e → R.₁ e C.∘ _) (map .commutes _) ⟩≡
R.₁ (adj.counit.ε _ D.∘ L.₁ (Cone.ψ K o)) C.∘ adj.unit.η _        ≡⟨ C.pushl (R.F-∘ _ _) ⟩≡
R.₁ (adj.counit.ε _) C.∘ R.₁ (L.₁ (Cone.ψ K o)) C.∘ adj.unit.η _  ≡˘⟨ C.pullr (adj.unit.is-natural _ _ _) ⟩≡˘
(R.F₁ (adj.counit.ε _) C.∘ adj.unit.η _) C.∘ Cone.ψ K o           ≡⟨ ap (λ e → e C.∘ Cone.ψ K _) adj.zag ⟩≡
C.id C.∘ Cone.ψ K o                                               ≡⟨ C.idl _ ⟩≡
Cone.ψ K o                                                        ∎

right-adjoint-cone-hom
: {K : Cone (R F∘ F)} {K′ : Cone F}
→ Cone-hom (R F∘ F) K (cone-right-adjoint K′)
→ Cone-hom F (right-adjoint-cone K) K′
right-adjoint-cone-hom map .hom = adj.counit.ε _ D.∘ L.₁ (map .hom)
right-adjoint-cone-hom {K = K} {K′ = K′} map .commutes o =
K′ .ψ o D.∘ adj.counit.ε _ D.∘ L.₁ (map .hom)               ≡⟨ D.extendl (sym (adj.counit.is-natural _ _ _)) ⟩≡
adj.counit.ε _ D.∘ (L.₁ (R.₁ (K′ .ψ o)) D.∘ L.₁ (map .hom)) ≡⟨ ap (λ e → _ D.∘ e) (sym (L.F-∘ _ _)) ⟩≡
adj.counit.ε _ D.∘ (L.₁ (R.₁ (K′ .ψ o) C.∘ map .hom))       ≡⟨ ap (λ e → _ D.∘ L.₁ e) (map .commutes _) ⟩≡
adj.counit.ε _ D.∘ L.₁ (K .ψ o)                             ∎


Hence, if we have a limit for $F$, the two lemmas above (in the “towards right adjoint” direction) already get us 66% of the way to having a limit for $R \circ F$. The missing bit is a very short calculation:

    right-adjoint-limit : Limit F → Limit (R F∘ F)
right-adjoint-limit lim .top = cone-right-adjoint (lim .top)
right-adjoint-limit lim .has⊤ cone = contr ! !-unique where
pre! = lim .has⊤ _ .centre
! = cone-hom-right-adjoint pre!

!-unique : ∀ x → ! ≡ x
!-unique x = Cone-hom-path _ (
R.₁ (pre! .hom) C.∘ adj.unit.η _                             ≡⟨ ap (λ e → R.₁ e C.∘ _) (ap hom (lim .has⊤ _ .paths (right-adjoint-cone-hom x))) ⟩≡
R.₁ (adj.counit.ε _ D.∘ L.₁ (x .hom)) C.∘ adj.unit.η _       ≡˘⟨ C.pulll (sym (R.F-∘ _ _)) ⟩≡˘
R.₁ (adj.counit.ε _) C.∘ R.₁ (L.₁ (x .hom)) C.∘ adj.unit.η _ ≡˘⟨ ap (R.₁ _ C.∘_) (adj.unit.is-natural _ _ _) ⟩≡˘
R.₁ (adj.counit.ε _) C.∘ adj.unit.η _ C.∘ x .hom             ≡⟨ C.cancell adj.zag ⟩≡
x .hom                                                       ∎)


We then have the promised theorem: right adjoints preserve limits.

  right-adjoint-is-continuous
: ∀ {os ℓs} → is-continuous {oshape = os} {hshape = ℓs} R
right-adjoint-is-continuous L x = Terminal.has⊤ (right-adjoint-limit (record { top = L ; has⊤ = x }))


## Concrete limits🔗

For establishing the preservation of “concrete limits”, in addition to the preexisting conversion functions (Lim→Prod, Limit→Pullback, Limit→Equaliser, etc.), we must establish results analogous to canonical-functors: Functors out of shape categories are entirely determined by the “introduction forms” cospan→cospan-diagram and par-arrows→par-diagram.

  open import Cat.Instances.Shape.Parallel
open import Cat.Instances.Shape.Cospan
open import Cat.Diagram.Limit.Equaliser
open import Cat.Diagram.Limit.Pullback
open import Cat.Diagram.Limit.Product
open import Cat.Diagram.Equaliser
open import Cat.Diagram.Pullback
open import Cat.Diagram.Product

right-adjoint→product
: ∀ {A B} → Product D A B → Product C (R.₀ A) (R.₀ B)
right-adjoint→product {A = A} {B} prod =
Lim→Prod C (fixup (right-adjoint-limit (Prod→Lim D prod)))
where
fixup : Limit (R F∘ 2-object-diagram D {iss = Bool-is-set} A B)
→ Limit (2-object-diagram C {iss = Bool-is-set} (R.₀ A) (R.₀ B))
fixup = subst Limit (canonical-functors _ _)

right-adjoint→pullback
: ∀ {A B c} {f : D.Hom A c} {g : D.Hom B c}
→ Pullback D f g → Pullback C (R.₁ f) (R.₁ g)
right-adjoint→pullback {f = f} {g} pb =
Limit→Pullback C {x = lzero} {y = lzero}
(right-adjoint-limit (Pullback→Limit D pb))

right-adjoint→equaliser
: ∀ {A B} {f g : D.Hom A B}
→ Equaliser D f g → Equaliser C (R.₁ f) (R.₁ g)
right-adjoint→equaliser {f = f} {g} eq =
Limit→Equaliser C (right-adjoint-limit
(Equaliser→Limit D {F = par-arrows→par-diagram f g} eq))

right-adjoint→terminal
: ∀ {X} → is-terminal D X → is-terminal C (R.₀ X)
right-adjoint→terminal term x = contr fin uniq where
fin = L-adjunct L⊣R (term (L.₀ x) .centre)
uniq : ∀ x → fin ≡ x
uniq x = ap fst \$ is-contr→is-prop (R-adjunct-is-equiv L⊣R .is-eqv _)
(_ , equiv→section (R-adjunct-is-equiv L⊣R) _)
(x , is-contr→is-prop (term _) _ _)

right-adjoint→lex : is-lex R
right-adjoint→lex .is-lex.pres-⊤ = right-adjoint→terminal
right-adjoint→lex .is-lex.pres-pullback {f = f} {g = g} pb =
right-adjoint→pullback (record { p₁ = _ ; p₂ = _ ; has-is-pb = pb }) .Pullback.has-is-pb