open import Cat.Instances.Shape.Terminal
open import Cat.Diagram.Colimit.Base
open import Cat.Diagram.Limit.Finite
open import Cat.Diagram.Limit.Base
open import Cat.Diagram.Terminal
open import Cat.Functor.Kan.Base
open import Cat.Prelude

import Cat.Functor.Reasoning as Func

module Cat.Functor.Adjoint.Continuous where

module _
{o o' β β'} {C : Precategory o β} {D : Precategory o' β'}
{L : Functor C D} {R : Functor D C}
(Lβ£R : L β£ R)
where
private
module L = Func L
module R = Func R
module C = Precategory C
module D = Precategory D
open _=>_


We prove that every functor admitting a left adjoint preserves every limit which exists in We then instantiate this theorem to the βcanonicalβ shapes of limit: terminal objects, products, pullback and equalisers.

This follows directly from the fact that adjoints preserve Kan extensions.

  right-adjoint-is-continuous
: β {os βs} β is-continuous os βs R

: β {os βs} β is-cocontinuous os βs L

module _ {od βd} {J : Precategory od βd} where
right-adjoint-limit : β {F : Functor J D} β Limit F β Limit (R Fβ F)

left-adjoint-colimit : β {F : Functor J C} β Colimit F β Colimit (L Fβ F)


## Concrete limitsπ

We now show that adjoint functors preserve βconcrete limitsβ. We could show this using general abstract nonsense, but we can avoid transports if we do it by hand.

  open import Cat.Diagram.Equaliser
open import Cat.Diagram.Pullback
open import Cat.Diagram.Product

  right-adjointβis-product
: β {x a b} {p1 : D.Hom x a} {p2 : D.Hom x b}
β is-product D p1 p2
β is-product C (R.β p1) (R.β p2)
right-adjointβis-product {x = x} {a} {b} {p1} {p2} d-prod = c-prod where
open is-product

c-prod : is-product C (R.β p1) (R.β p2)
c-prod .unique {other = other} p q =

: β {p x y z}
β {p1 : D.Hom p x} {f : D.Hom x z} {p2 : D.Hom p y} {g : D.Hom y z}
β is-pullback D p1 f p2 g
β is-pullback C (R.β p1) (R.β f) (R.β p2) (R.β g)
right-adjointβis-pullback {p1 = p1} {f} {p2} {g} d-pb = c-pb where
open is-pullback

c-pb : is-pullback C (R.β p1) (R.β f) (R.β p2) (R.β g)
c-pb .square = R.weave (d-pb .square)
c-pb .universal sq =
c-pb .pββuniversal =
R.pulll (d-pb .pββuniversal) β L-R-adjunct Lβ£R _
c-pb .pββuniversal =
R.pulll (d-pb .pββuniversal) β L-R-adjunct Lβ£R _
c-pb .unique {_} {pβ'} {pβ'} {sq} {other} p q =

: β {e a b} {f g : D.Hom a b} {equ : D.Hom e a}
β is-equaliser D f g equ
β is-equaliser C (R.β f) (R.β g) (R.β equ)
right-adjointβis-equaliser {f = f} {g} {equ} d-equal = c-equal where
open is-equaliser

c-equal : is-equaliser C (R.β f) (R.β g) (R.β equ)
c-equal .equal = R.weave (d-equal .equal)
c-equal .universal sq =
c-equal .factors =
R.pulll (d-equal .factors) β L-R-adjunct Lβ£R _
c-equal .unique p =

: β {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βcounit (R-adjunct-is-equiv Lβ£R) _)
(x , is-contrβis-prop (term _) _ _)