Michael Shulman
dependent types in a 2-category

This is just bits and pieces for now; something more coherent will come later.

Overview

…

Of course, we should be able to treat an $n$-type as an $m$-type for any $m\ge n$. When $n=-1$ and $m=0$ this corresponds to replacing a proposition $\phi$ by the set $\{*\mid \phi \}$, while when $n=0$ and $m=1$ it corresponds to treating a set as a discrete category. It should also be true that the resulting $m$-type is appropriately truncated.

…

Type-raising

The following operations allow us to interpret an $n$-type as an $m$-type whenever $m\ge n$.

$$\frac{\Gamma ⊢A:n\mathrm{Type}}{\Gamma ⊢\mid A\mid :(n+1)\mathrm{Type}}(n=0,-1)$$\frac{\Gamma \vdash A:n Type} {\Gamma\vdash {|A|}:(n+1) Type} (n = 0,-1)

$$\frac{\Gamma ⊢A:n\mathrm{Type}}{\Gamma ,x:A⊢i_n(x):\mid A\mid }(n=0,-1)$$\frac{\Gamma \vdash A:n Type} {\Gamma, x:A \vdash i_n(x) : {|A|}} (n = 0,-1)

$$\frac{\Gamma ⊢A:n\mathrm{Type}}{\Gamma ,x:\mid A\mid ⊢j_n(x):A}(n=0,-1)$$\frac{\Gamma \vdash A:n Type} {\Gamma, x:{|A|} \vdash j_n(x) : A} (n = 0,-1)

$$\frac{\Gamma ⊢A:n\mathrm{Type}}{\Gamma ,x:A⊢x\equiv j_n(i_n(x)):A}(n=0,-1)$$\frac{\Gamma \vdash A:n Type} {\Gamma, x:A \vdash x\equiv j_n(i_n(x)) : A} (n = 0,-1)

$$\frac{\Gamma ⊢A:n\mathrm{Type}}{\Gamma ,x:\mid A\mid ⊢x\equiv i_n(j_n(x)):\mid A\mid }(n=0,-1)$$\frac{\Gamma \vdash A:n Type} {\Gamma, x:{|A|} \vdash x\equiv i_n(j_n(x)) : {|A|}} (n = 0,-1)

It follows that if $\phi :\mathrm{Prop}$, then $x:\mid \phi \mid ,y:\mid \phi \mid ⊢x\equiv y$, since $j_{-1}(x)\equiv j_{-1}(y)$ as both are terms of a $(-1)$-type $\phi$. Thus, $\mid \phi \mid$ is in fact a subsingleton as desired. What remains to assert is that if $A:\mathrm{Set}$ then $\mid A\mid :\mathrm{Cat}$ is a discrete category.

$$\frac{\Gamma ⊢A:\mathrm{Set}}{\Gamma ,x:\mid A\mid ,y:\mid A\mid ,f:{\mathrm{hom}}_{\mid A\mid }(x,y)⊢(x\equiv y)}$$\frac{\Gamma \vdash A:Set} {\Gamma, x:{|A|}, y:{|A|}, f:hom_{|A|}(x,y) \vdash (x \equiv y)}

$$\frac{\Gamma ⊢A:\mathrm{Set}}{\Gamma ,x:\mid A\mid ,f:{\mathrm{hom}}_{\mid A\mid }(x,x)⊢(f\equiv 1_x)}$$\frac{\Gamma \vdash A:Set} {\Gamma, x:{|A|}, f:hom_{|A|}(x,x) \vdash (f \equiv 1_x)}

Dependent sums

In theory, the ways to type the formation of dependent sums ${\Sigma }_{x:A}B(x)$ are parametrized by three sorts: the sort of $A$, the sort of $B$, and the sort of the result. In our case, we allow two general classes of dependent sums.

• In the first, $B$ must be a proposition, while $A$ can be anything, and in this case the result is a proposition. This construction gives existential quantifiers, so we will notate it as $(\exists x:A)B(x)$.
• In the second, $A$ must be a set, while $B$ can be anything, and the result has the same sort as $B$. This construction gives “indexed disjoint unions,” and we will use the ordinary dependent sum notation ${\Sigma }_{x:A}B(x)$ for it.

Note that in the overlap case when $A$ is a set and $B$ is a proposition, we get two different ways to form a dependent sum ${\Sigma }_{x:A}B(x)$ depending on what the result type is. If the result is a proposition, then it is the proposition $(\exists x:A)B(x)$, while if the result is a set, then it is the set $\{x:A\mid B(x)\}$. The difference from a computational point of view is that in the second case, it is possible to extract the witness $x:A$, while in the first it is not.

There should also be dependent sums of the second sort where $A$ is a category, with the result being a category. However, in this case, unless the dependence of $B$ on $A$ is given functorially, then it is not possible to determine the morphisms in the dependent sum. We will study the general case of functorially dependent types elsewhere, but here we do need one particular case.

Strong dependent sums

$$\frac{\Gamma ⊢A:\mathrm{Set}\Gamma ,x:A⊢B(x):n\mathrm{Type}}{\Gamma ⊢{\Sigma }_{x:A}B(x):n\mathrm{Type}}$$\frac{\Gamma \vdash A:Set \qquad \Gamma, x:A \vdash B(x):n Type}{ \Gamma \vdash \Sigma_{x:A}B(x) :n Type}

$$\frac{\Gamma ⊢A:\mathrm{Set}\Gamma ,x:A⊢B(x):n\mathrm{Type}}{\Gamma ,x:A,y:B(x)⊢⟨x,y⟩:{\Sigma }_{x:A}B(x)}$$\frac{\Gamma \vdash A:Set \qquad \Gamma, x:A \vdash B(x):n Type}{\Gamma, x:A, y:B(x) \vdash \langle x,y\rangle : \Sigma_{x:A} B(x)}

$$\frac{\Gamma ⊢A:\mathrm{Set}\Gamma ,x:A⊢B(x):n\mathrm{Type}}{\Gamma ,z:{\Sigma }_{x:A}B(x)⊢{\pi }_1(z):A}$$\frac{\Gamma \vdash A:Set \qquad \Gamma, x:A \vdash B(x):n Type} {\Gamma, z: \Sigma_{x:A}B(x) \vdash \pi_1(z) :A}

$$\frac{\Gamma ⊢A:\mathrm{Set}\Gamma ,x:A⊢B(x):n\mathrm{Type}}{\Gamma ,z:{\Sigma }_{x:A}B(x)⊢{\pi }_2(z):B({\pi }_1(x))}$$\frac{\Gamma \vdash A:Set \qquad \Gamma, x:A \vdash B(x):n Type} {\Gamma, z: \Sigma_{x:A}B(x) \vdash \pi_2(z) :B(\pi_1(x))}

$$\frac{\Gamma ⊢A:\mathrm{Set}\Gamma ,x:A⊢B(x):n\mathrm{Type}}{\Gamma ,x:A,y:B(x)⊢{\pi }_1(⟨x,y⟩)\equiv x:A}$$\frac{\Gamma \vdash A:Set \qquad \Gamma, x:A \vdash B(x):n Type}{\Gamma, x:A, y:B(x) \vdash \pi_1(\langle x,y\rangle) \equiv x : A}

$$\frac{\Gamma ⊢A:\mathrm{Set}\Gamma ,x:A⊢B(x):n\mathrm{Type}}{\Gamma ,x:A,y:B(x)⊢{\pi }_2(⟨x,y⟩)\equiv y:A(x)}$$\frac{\Gamma \vdash A:Set \qquad \Gamma, x:A \vdash B(x):n Type}{\Gamma, x:A, y:B(x) \vdash \pi_2(\langle x,y\rangle) \equiv y : A(x)}

$$\frac{\Gamma ⊢A:\mathrm{Set}\Gamma ,x:A⊢B(x):n\mathrm{Type}}{\Gamma ,z:{\Sigma }_{x:A}B(x)⊢z\equiv ⟨{\pi }_1(z),{\pi }_2(z)⟩:{\Sigma }_{x:A}B(x)}$$\frac{\Gamma \vdash A:Set \qquad \Gamma, x:A \vdash B(x):n Type} {\Gamma, z: \Sigma_{x:A}B(x) \vdash z \equiv \langle \pi_1(z), \pi_2(z)\rangle :\Sigma_{x:A}B(x)}

Note that when $n=0$ and $B(x)$ is independent of $x$, then ${\Sigma }_{x:A}B(x)$ is canonically isomomorphic to $A\times B$. In ordinary type theory, one doesn’t need to define both binary products and dependent sums, since the former can be constructed from the latter in this way. However, since we aren’t allowing dependent sums over categories, we need binary products for categories given separately.

When $n=1$ we also have rules for morphisms.

$$\frac{\Gamma ⊢A:\mathrm{Set}\Gamma ,x:A⊢B(x):\mathrm{Cat}}{\Gamma ,x:A,y_1:B(x),y_2:B(x),f:{\mathrm{hom}}_{B(x)}(y_1,y_2)⊢⟨x,f⟩:{\mathrm{hom}}_{{\Sigma }_{x:A}B(x)}(⟨x,y_1⟩,⟨x,y_2⟩)}$$\frac{\Gamma \vdash A:Set \qquad \Gamma, x:A \vdash B(x):Cat} {\Gamma, x:A, y_1:B(x), y_2:B(x), f:hom_{B(x)}(y_1,y_2) \vdash \langle x,f\rangle : hom_{\Sigma_{x:A} B(x)}(\langle x,y_1\rangle, \langle x,y_2\rangle)}

$$\frac{\Gamma ⊢A:\mathrm{Set}\Gamma ,x:A⊢B(x):\mathrm{Cat}}{\Gamma ,z_1:{\Sigma }_{x:A}B(x),z_2:{\Sigma }_{x:A}B(x),f:{\mathrm{hom}}_{{\Sigma }_{x:A}B(x)}(z_1,z_2)⊢{\pi }_1(z_1)\equiv {\pi }_2(z_2):A}$$\frac{\Gamma \vdash A:Set \qquad \Gamma, x:A \vdash B(x):Cat} {\Gamma, z_1: \Sigma_{x:A}B(x), z_2 : \Sigma_{x:A}B(x), f:hom_{\Sigma_{x:A}B(x)}(z_1,z_2) \vdash \pi_1(z_1)\equiv \pi_2(z_2): A}

$$\frac{\Gamma ⊢A:\mathrm{Set}\Gamma ,x:A⊢B(x):\mathrm{Cat}}{\Gamma ,z_1:{\Sigma }_{x:A}B(x),z_2:{\Sigma }_{x:A}B(x),f:{\mathrm{hom}}_{{\Sigma }_{x:A}B(x)}(z_1,z_2)⊢{\pi }_2(f):{\mathrm{hom}}_{B({\pi }_1(x))}({\pi }_2(z_1),{\pi }_2(z_2))}$$\frac{\Gamma \vdash A:Set \qquad \Gamma, x:A \vdash B(x):Cat} {\Gamma, z_1: \Sigma_{x:A}B(x), z_2 : \Sigma_{x:A}B(x), f:hom_{\Sigma_{x:A}B(x)}(z_1,z_2) \vdash \pi_2(f): hom_{B(\pi_1(x))}(\pi_2(z_1),\pi_2(z_2))}

$$\frac{\Gamma ⊢A:\mathrm{Set}\Gamma ,x:A⊢B(x):\mathrm{Cat}}{\Gamma ,x:A,y_1:B(x),y_2:B(x),f:{\mathrm{hom}}_{B(x)}(y_1,y_2)⊢f\equiv {\pi }_2(⟨x,f⟩):{\mathrm{hom}}_{B(x)}(y_1,y_2)}$$\frac{\Gamma \vdash A:Set \qquad \Gamma, x:A \vdash B(x):Cat} {\Gamma, x:A, y_1:B(x), y_2:B(x), f:hom_{B(x)}(y_1,y_2) \vdash f \equiv \pi_2(\langle x,f\rangle) : hom_{B(x)}(y_1,y_2)}

$$\frac{\Gamma ⊢A:\mathrm{Set}\Gamma ,x:A⊢B(x):\mathrm{Cat}}{\Gamma ,z_1:{\Sigma }_{x:A}B(x),z_2:{\Sigma }_{x:A}B(x),f:{\mathrm{hom}}_{{\Sigma }_{x:A}B(x)}(z_1,z_2)⊢f\equiv ⟨{\pi }_1(z),{\pi }_2(f)⟩:{\mathrm{hom}}_{{\Sigma }_{x:A}B(x)}(z_1,z_2)}$$\frac{\Gamma \vdash A:Set \qquad \Gamma, x:A \vdash B(x):Cat} {\Gamma, z_1: \Sigma_{x:A}B(x), z_2 : \Sigma_{x:A}B(x), f:hom_{\Sigma_{x:A}B(x)}(z_1,z_2) \vdash f\equiv \langle \pi_1(z), \pi_2(f)\rangle: hom_{\Sigma_{x:A}B(x)}(z_1,z_2)}

Dependent products

As with dependent sums, in general the operation ${\Pi }_{x:A}B(x)$ is parametrized by the sorts of $A$, of $B(x)$, and of the result. Since exponentials in a 2-category require fibrations and variance, for now we restrict to the case when $B(x)$ and ${\Pi }_{x:A}B(x)$ are both propositions. When $A$ is a set or a category, this gives universal quantification, which we write as $(\forall x:A)B(x)$, while when $A$ is also a proposition it gives implication, which we write as $A\Rightarrow B$.