§ 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 fprojectOut :: Limit f -> f aprojectOut (MkLimit fa)  = fadata Colimit (f:: * -> *) where  MkCoLimit :: f a -> Colimit fprojectIn :: f a -> Colimit fprojectIn = MkCoLimit