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:

- 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$.
- 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.

- Binding syntax $x:_{\not i} A$ means “$x$ is an instance of a type that erases to $A$.
- Binding $x:_i A$ means that this binding and all relevant usages are all colored as $i$.
- 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).

- Erasure deletes colored things, and in case of the colored sigma type, it’s $b$, so erasure of colored sigma is the first projection.
- Interpreting a colored sigma judgment $t:(x:A)\times_i B$ as predicate is $t:_i B[\lfloor t\rfloor_i/x]$.

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)$.

- What if we erase the color $i$ from this application? Well, by erasing the arguments! We take the first projection of the sigma type and the pair term, yielding $f~B~b$.
- What if we interpret this shit as a predicate? Well, since we know its erasure $f~B~b$, the predicate interpretation is $(x=b)[f~B~b/x]$, aka $f~B~b=b$.

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