Sigma types demonstrations

by

This post lists some example usages of the dependent sum type (denoted $\Sigma$, and I prefer the name ‘sigma type’ over ‘dependent sum type’) to help intuiting its applications.

I’ll use the $t.1$ and $t.2$ for sigma elimination (projections) and $\langle a, b\rangle$ for sigma introduction.

The first two sections use some category theory but not the last one. So, if you’re new to category theory, you may wanna skip the first two.

Subobject classifiers

In a categorical model of dependent type theories, such as a contextual category, there’s always a category whose objects are contexts and morphisms are substitutions (aka “context morphisms”). It is well-known (like, written in the “idea” section of this nlab entry) that subobject classifiers in such categories correspond to the universe of propositions in type theories.

Recall that a subobject classifier is a monomorphism (hereafter as ‘mono’) $\text{true}\in\mathcal C(*, \Omega)$ from the terminal object $*\in\mathcal C$ such that for all mono $f\in\mathcal C(U, X)$ there’s a unique morphism $\chi_U\in(X,\Omega)$ characterized by the following pullback square:

\[\begin{CD} U @>>> * \\ @VfVV @VV\text{true}V \\ X @>>\chi_U> \Omega \end{CD}\]

The universe of propositions $\text{Prop}$ is a type such that for each type $X$ and a proof that $X$ is a proposition, there is a term $El(X):\text{Prop}$.

The sigma type $\Sigma_{P:\text{Prop}}P$ (we’re implicitly converting an instance of $\text{Prop}$ to a type. You can think of it as applying the elimination rule of $\text{Prop}$) could be used to represent the terminal object. Diagrammatically:

\[\begin{CD} \Gamma,P:\text{Prop} @>>> \Sigma_{P:\text{Prop}}P \\ @V\pi_PVV @VV.1V \\ \Gamma @>>> \text{Prop} \end{CD}\]

It is terminal because propositions are contractible.

(I appreciate Brendan Zabarauskas for his review from Twitter)

Initiality of $\Pi_{P:\text{Prop}}P$

A contextual category is normally equipped with a terminal object – the empty context, but the initial object is not very straightforward to intuit. I’ll show you a construction.

Once we have the universe of propositions (so, some kind of “universe”), we can construct the empty type as a pi type $\bot=\Pi_{P:\text{Prop}}P$ (observation: we’ve just used $\Sigma_{P:\text{Prop}}P$ as a terminal object, and replacing sigma with pi gives us the initial object!!). But weather this object is the initial object in a contextual category (or any other similar construction) is not obvious. The construction of the unique morphisms could also be done with a sigma type.

Suppose you have a type $A$, we construct the type $\Sigma_\bot A$, and we can prove it to be a proposition (easy), so $El(\Sigma_\bot A):\text{Prop}$. For every type $A$, we can construct such instance of $\text{Prop}$, and we can obtain a morphism $\bot\text{-elim}\in\mathcal C(\bot, A)$ (expands to $\mathcal C(\Pi_{P:\text{Prop}}P, A)$) by:

  1. Apply (evaluation map is unique) the term $El(\Sigma_\bot A)$ to the parameter of type $\Pi_{P:\text{Prop}}P$, get an instance of $\Sigma_\bot A$.
  2. Perform the second projection (unique morphism), get an instance of $A$.

Parametricity in TTC

In the “type theory with colors” paper, they parameterize types with an optional color denoted $i$, and we can erase the colors. For instance, we can mark the type parameter $A$ of the $\text{List}$ type with a color, and $\text{List}$ becomes a type parameterized by a color. If we erase this color, $\text{List}$ loses its parameter $A$ and becomes the Peano natural number type $\mathbb N$. Notationally $\lfloor \text{List}~a\rfloor_i=\mathbb N$, and we have the same notation for terms (apart from types). You should be able to imagine that list concat erases to Peano addition.

  1. Binding syntax $x:_{\not i} A$ means “$x$ is an instance of a type that erases to $A$.
  2. Binding $x:_i A$ means that this binding and all relevant usages are all colored as $i$.
  3. Judgment $A:_i s$ (not a binding, but a judgment) denotes the encoding of types as “predicates” (so, type $A$ becomes some kind of predicate, and $s$ is a “kind” in the Haskell sense, which might be $\mathcal U$ or with some indices).

For the last notation I think it worth a demonstration. The example given in [Bernardy and Marlin, 2013] is $\text{List} (A:_i \mathcal U) :_i (x :_{\not i} \mathbb N) \to \mathcal U$, and we put $\mathbb N$ there because $\text{List}$ erases to it. We write $m:_i\text{List}~a$ to mean that $\lfloor m \rfloor_i:\text{List}~a~(\lfloor m \rfloor_i)$ (note that here we’re treating $\text{List}~a$ as a predicate that takes a term that erases to a natural number. That’s how we make sense of the application of $\lfloor m \rfloor_i$. In the paper, the notation is weird, and I picked the application syntax I’m comfortable with here).

Then, we also define sigma types with colors $(x:A)\times_i B$, which is similar to $\Sigma_{x:A}B$ but instead of the usual introduction rule $\cfrac{a:A\quad b:B[a/x]}{\langle a,b\rangle:\Sigma_{x:A}B}$, we ask $a$ to be a term that erases to be of type $A$, and $b:_i B[a/x]$ colored (so it has a predicate interpretation), yielding the introduction rule $\cfrac{a:_{\not i}A\quad b:_i B[a/x]}{\langle a,b\rangle_i:(x:A)\times_i B}$ (I slightly modified the notation in the paper again).

Now, consider a function $f:(A:\mathcal U)\to A\to A$, a type $B:\mathcal U$, and a term $b:B$. I’d like to remind you a fact about identity type that $\langle b,\text{refl}_b\rangle:\Sigma_{x:B} (x=b)$ and its colored version $\langle b,\text{refl}_b\rangle_i:(x:B)\times_i (x=b)$.

We can easily derive the judgment $f~\Big((x:B)\times_i (x=b)\Big)~\langle b,\text{refl}_b\rangle_i:(x:B)\times_i (x=b)$.

Look at it. It’s parametricity, and the proof is ✨internalized✨.


Tweet this Top

License

This work (Sigma types demonstrations) is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.

License