Michael Shulman functorially dependent types

Overview

We introduce variables with variances. In the standard categorical interpretation of a context such as $x:A, y:B(x)$, the type $B(x)$ that depends on a variable $x:A$ is interpreted by an object of a slice category $C/A$; the intuition being that for each $x: A$ the type $B(x)$ is the fiber over $x$ of the map $B\to A$. However, in 2-category the fibrational slices are often more important than ordinary slices, but incorporating fibrational slices necessitates some way of keeping track of which morphisms are fibrations and which are opfibrations.

Thus, we now define a 1-context to be a finite list

$$x_1:A_1^{\epsilon_1}, \dots, x_n:A_n^{\epsilon_n}$$

of variable declarations, such that:

1. For each $k$, the judgement
   $$x_1:A_1^{\epsilon_1}, \dots, x_{k-1}:A_{k-1}^{\epsilon_{k-1}} \vdash A_k:Cat$$

   is derivable.

2. Each $\epsilon_k$ is either $+$, $-$, or $0$.
3. If $\epsilon_k=0$, then $\epsilon_j=0$ for all $j\gt k$.

We will often omit the superscript $0$s. We then define a 0-context to be a 1-context $\Theta$ together with a finite list

$$y_1:B_1, \dots, y_n:B_n$$

of variable declarations, such that for each $k$, the judgement

$$\Theta | y_1:B_1,\dots, y_{k-1}:B_{k-1} \vdash B_k:Set$$

is derivable, and a (-1)-context to be a 0-context $\Theta|\Delta$ together with a finite list

$$\psi_1,\dots, \psi_n$$

of propositions, such that for each $k$, the judgement

$$\Theta | \Delta \vdash \psi_k :Prop$$

is derivable.

The intended interpretation of these contexts is as follows. A context $x:A^+$ indicates that everything to its right takes place in the opfibrational slice $Opf(A)$. Likewise, $x:A^-$ indicates that everything to its right takes place in $Fib(A)$, while $x:A^0$ indicates that everything to its right takes place in the ordinary slice 2-category $K/X$. Recalling the theorems about iterated fibrations, a context such as $x:A^+, y:B(x)^+$ indicates that we work in $Opf_{Opf(A)}(B\to A) = Opf(B)$, while $x:A^+, y:B^-$ indicates working in the two-sided fibrational slice $Fib(A,B)$. Note that the variance label goes on the base of the fibration.

Once we are past the first $|$, then we assume to be working only in the 1-category of discrete objects. After this point, the interpretation of 0-contexts is just as usual: a declaration $x:B$, where $B$ is a 0-type, means working in the slice 1-category of discrete objects over $B$. Similarly, once we pass the second $|$, we are now working in a poset of subterminals, and a declaration $\psi$ means we assume that $\psi$ is true (which amounts to working in the slice poset over $\psi$). For example, a context such as

$$x:A^+ | y:B$$

means working in $disc(Opf(A))/B$.

We say that a context is fibrational if no $\epsilon_k$ (in its 1-context section) is equal to $0$. Since fibrational slices inherit more good behavior than ordinary slices, some of the rules below will require only fibrational contexts. (However, some rules will also inexorably take us out of fibrational contexts.) We write $\Gamma^\pm$ to mean that $\Gamma$ is a fibrational context, and if $\Gamma$ is any context, we write $\Gamma^0$ for the context obtained from $\Gamma$ by dropping all variances (changing all $\epsilon_k$ to $0$).

The reason we write $A^+$ and $A^-$ instead of $A$ and $A^{op}$ is that a judgement written like $x:A^{op} \vdash b(x):B$ looks as though we are defining a contravariant functor from $A$ to $B$, whereas the fibrational variances only affect the types defined in a given context, not the terms.

Finally, a theory consists of some collection of axiomatic judgements of each type, with the restriction that axiomatic 1-type and 0-type declarations only occur in fibrational contexts. (This restriction will only be necessary when we come to construct a syntactic 2-category?.) There is a subtlety in that the contexts of the judgements in a theory must be well-formed, which involves an assertion about derivability in the theory itself, but the resolution of this presents no new difficulties over ordinary dependent type theory.

Old bits that haven’t been rethought yet

Sum types

$$\frac{\Gamma^\pm \vdash A:Type \qquad \Gamma^\pm, x:A^- \vdash B:Type}{\Gamma^\pm \vdash \Sigma_{x:A^-} B : Type} (\text{fibrational sum type})$$

We now have rules relating elements and arrows in sum types to those in the base, which essentially express the factorization properties of fibrations.

$$\frac{\Gamma^\pm \vdash A:Type \qquad \Gamma^\pm, x:A^- \vdash B:Type}{\Gamma^\pm, x:\Sigma_{x:A^-} B \vdash proj(x):A}$$

Note that $proj(x)$ is a term with free variable $x$, so it is automatically functorial and acts on arrows as well as elements.

$$\frac{\Gamma^\pm \vdash A:Type \qquad \Gamma^\pm, x:A^- \vdash B:Type}{\Gamma^\pm, x:A,y:A,f:hom_A(y,x), u:B \vdash f^*u : B[y/x]}$$

$$\frac{\Gamma^\pm \vdash A:Type \qquad \Gamma^\pm, x:A^- \vdash B:Type}{\Gamma^\pm, x:A,y:A,f:hom_A(y,x), u:B \vdash cart(u) : hom_{\Sigma_{x:A^-} B}(f^*u,u)}$$

(Add a factorization axiom)

Of course, we have the analogous sums for opfibrations:

$$\frac{\Gamma^\pm \vdash A:Type \qquad \Gamma^\pm, x:A^+ \vdash B:Type}{\Gamma^\pm \vdash \Sigma_{x:A^+} B : Type} (\text{opfibrational sum type})$$

We trust the reader to write down the dual rules dealing with $f_!u$ and opcartesian arrows.