functorially dependent types

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:

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

- Each $\epsilon_k$ is either $+$, $-$, or $0$.
- 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.

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

Revised on March 1, 2010 20:46:13
by Mike Shulman
(128.135.230.139)