§ Intuition for limits in category theory

§ A characterization of limits

The theorem that characterizes limits is this:

A category has Finite Limits iff it has all finite products and equalizers.
limits have maps out of them.

§ Ravi Vakil's intuition for limits: Take sub things.

• An element of a limit gives one of each of its ingredients. For example, $K[[X]] = \lim_n \text{degree}~n~\text{polynomials}$, since we can get a degree n polynomial for all n, from any power series by truncation.
• limits have maps out of them.
• RAPL : right adjoints preserve limits.
• Limits commute with limits.
• These are mentioned in "Algebraic geometry in the time of Covid: Pseudolecture 2"
• Also, recalling that kernels are limits allows one to remember that we have maps that go out of a limit.

§ Limits are things you get maps out of.

• product has projections going out of it.
• gcd is less than the things that build it: gdb(a, b) -> a, b since gcd(a, b) < a and gcd(a, b) < b.
• single point set can be mapped out of.
• type Limit f = forall a. f a

§ Limits in Haskell

{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
data Limit (f :: * -> *) where
  MkLimit :: (forall a. f a) -> Limit f

projectOut :: Limit f -> f a
projectOut (MkLimit fa)  = fa

data Colimit (f:: * -> *) where
  MkCoLimit :: f a -> Colimit f

projectIn :: f a -> Colimit f
projectIn = MkCoLimit