<! --- LETTERS --->
$$ \newcommand{\lR}{\mathbb{R}} $$
$$ \newcommand{\lZ}{\mathbb{Z}} $$
$$ \newcommand{\lN}{\mathbb{N}} $$
$$ \newcommand{\lI}{\mathbb{I}} $$
$$ \newcommand{\II}{\mathbb{I}} $$
$$ \newcommand{\bI}{\mathbf{I}} $$
$$ \newcommand{\bC}{\mathbf{C}} $$
$$ \newcommand{\bD}{\mathbf{D}} $$
$$ \newcommand{\bE}{\mathbf{E}} $$
$$ \newcommand{\bF}{\mathbf{F}} $$
$$ \newcommand{\iI}{\mathsf{I}} $$
$$ \newcommand{\iA}{\mathsf{A}} $$
$$ \newcommand{\iB}{\mathsf{B}} $$
$$ \newcommand{\iC}{\mathsf{C}} $$
$$ \newcommand{\iD}{\mathsf{D}} $$
$$ \newcommand{\iE}{\mathsf{E}} $$
$$ \newcommand{\iF}{\mathsf{F}} $$
$$ \newcommand{\iM}{\mathsf{M}} $$
<! --- SYMBOLS --->
$$ \newcommand{\eps}{\epsilon} $$
$$ \newcommand{\SetCat}{\mathrm{Set}} $$
$$ \newcommand{\Bool}{\mathrm{Bool}} $$
$$ \newcommand{\Pos}{\mathrm{Pos}} $$
$$ \newcommand{\lbl}{\mathsf{lbl}} $$
$$ \newcommand{\subdiv}{\mathsf{sd}} $$
$$ \newcommand{\Hom}{\mathrm{Hom}} $$
$$ \newcommand{\Fun}{\mathrm{Fun}} $$
$$ \newcommand{\Psh}{\mathrm{PSh}} $$
<! --- OPERATORS --->
$$ \newcommand{\dim}{\mathrm{dim}} $$
$$ \newcommand{\id}{\mathrm{id}} $$
$$ \newcommand{\src}{\partial^-} $$
$$ \newcommand{\tgt}{\partial^+} $$
$$ \newcommand{\und}[1]{\underline{#1}} $$
$$ \newcommand{\abs}[1]{\left|{#1}\right|} $$
$$ \newcommand{\op}{^{\mathrm{op}}} $$
$$ \newcommand{\inv}{^{-1}} $$
<! --- CATEGORIES, FUNCTORS AND CONSTRUCTIONS --->
$$ \newcommand{\ttr}[1]{\mathfrak{T}^{#1}} $$
$$ \newcommand{\lttr}[2]{\mathfrak{T}^{#1}{(#2)}} $$
$$ \newcommand{\truss}[1]{\mathsf{T}\!\mathsf{rs}_{#1}} $$
$$ \newcommand{\sctruss}[1]{\bar{\mathsf{T}}\!\mathsf{rs}_{#1}} $$
$$ \newcommand{\rotruss}[1]{\mathring{\mathsf{T}}\!\mathsf{rs}_{#1}} $$
$$\newcommand{\trussbun}[1]{\mathsf{TrsBun}_{#1}} $$
$$ \newcommand{\trusslbl}[1]{\mathsf{Lbl}\mathsf{T}\!\mathsf{rs}_{#1}} $$
$$ \newcommand{\blcat}[1]{\mathsf{B}\mathsf{lk}_{#1}} $$
$$ \newcommand{\blset}[1]{\mathsf{Blk}\mathsf{Set}_{#1}} $$
$$ \newcommand{\fcl}[2]{\chi^{#1}_{#2}} $$
$$ \newcommand{\Entr}{\mathsf{Entr}} $$
$$ \newcommand{\Exit}{\mathsf{Exit}} $$
<! --- ARROWS AND RELATIONS --->
$$ \newcommand{\fleq}{\preceq} $$
$$ \newcommand{\fles}{\prec} $$
$$ \newcommand{\xto}[1]{\xrightarrow{#1}} $$
$$ \newcommand{\xot}[1]{\xleftarrow{#1}} $$
$$ \newcommand{\ot}{\leftarrow} $$
$$ \newcommand{\toot}{\leftrightarrow} $$
$$ \newcommand{\imp}{\Rightarrow} $$
$$ \newcommand{\iff}{\Leftrightarrow} $$
$$ \newcommand{\iso}{\cong} $$
$$ \newcommand{\into}{\hookrightarrow} $$
$$ \newcommand{\proto}{\longrightarrow\mkern{-2.8ex}{\raisebox{.3ex}{$\tiny\vert$}}\mkern{2.5ex}} $$
<! --- DIAGRAM ARROWS --->
<! ---... should replace \rlap by \mathrlap, see KaTeX doc --->
$$ \newcommand{\ra}[1]{\xrightarrow{\ \ #1\ \ }\phantom{}\kern-1.5ex} $$
$$ \newcommand{\la}[1]{\xleftarrow{\ \ #1\ \ }\phantom{}\kern-1.5ex} $$
$$ \newcommand{\da}[1]{\downarrow\raisebox{.5ex}{\rlap{$\scriptstyle#1$}}} $$
$$ \newcommand{\dra}[1]{\raisebox{.2ex}{\llap{$\scriptstyle#1$}}\kern-.5ex\searrow}} $$
$$ \newcommand{\dla}[1]{\swarrow\kern-1ex\raisebox{.2ex}{\rlap{$\scriptstyle#1$}}} $$
$$ \newcommand{\ua}[1]{\uparrow\raisebox{.2ex}{\rlap{$\scriptstyle#1$}}} $$
$$ \newcommand{\ura}[1]{\raisebox{.2ex}{\llap{$\scriptstyle#1$}\kern-.5ex\nearrow}} $$
$$ \newcommand{\ula}[1]{\nwarrow\kern-1ex\raisebox{.2ex}{\rlap{$\scriptstyle#1$}}} $$
Abstract. Big things are different from small things. It’s a fundamental law of mathematical nature. But it’s not so often talked about. Here we at least say once that it’s a thing. (Feel free to extend!)
Context
There are certain things in mathematics that you learn to be true over time but which are not written down because they are not precise, and mathematicians usually like to only write down precise things. The distinction of big vs small things is one of them.
Small things
Small things are generated from nothingness by an inductive process that, inducitively, adds new components to exisiting components of that thing.
- Finite things are certainly small: you can just add each of the finitely many components separately.
- Inductive types are small things: e.g., the type of numbers is small.
- The set of all programs is still a small thing (among the small things though, it is relatively big :-D)
- Funnily enough, any mathematical theory is a small thing (proof terms are generated inductively); of course, it may contain terms that represent big things symbolically.
Big things
Big things are more spurious; they are things that derive from “proto-typical big things” (wow, vague!).
- Universes in type theory are big, and so are Grothendieck cardinals in ZFC
- Presheaf categories are big things (and so their derivatives: toposes, stable $\infty$-categories, etc.)
Moreover, when you take a big thing of big things, it’s naturally an even bigger thing.
Maths needs both
Just like a house needs a floor and a ceiling, mathematics needs big things and small things to function. We need the former to talk about all things, and we need the latter to talk about concrete things.
