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)x:A, y:B(x), the type B(x)B(x) that depends on a variable x:Ax:A is interpreted by an object of a slice category C/AC/A; the intuition being that for each x:Ax: A the type B(x)B(x) is the fiber over xx of the map BAB\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 ϵ 1,,x n:A n ϵ n x_1:A_1^{\epsilon_1}, \dots, x_n:A_n^{\epsilon_n}

of variable declarations, such that:

  1. For each kk, the judgement
    x 1:A 1 ϵ 1,,x k1:A k1 ϵ k1A k:Catx_1:A_1^{\epsilon_1}, \dots, x_{k-1}:A_{k-1}^{\epsilon_{k-1}} \vdash A_k:Cat

    is derivable.

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

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

y 1:B 1,,y n:B n y_1:B_1, \dots, y_n:B_n

of variable declarations, such that for each kk, the judgement

Θ|y 1:B 1,,y k1:B k1B k:Set\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

ψ 1,,ψ n \psi_1,\dots, \psi_n

of propositions, such that for each kk, the judgement

Θ|Δψ k:Prop\Theta | \Delta \vdash \psi_k :Prop

is derivable.

The intended interpretation of these contexts is as follows. A context x:A +x:A^+ indicates that everything to its right takes place in the opfibrational slice Opf(A)Opf(A). Likewise, x:A x:A^- indicates that everything to its right takes place in Fib(A)Fib(A), while x:A 0x:A^0 indicates that everything to its right takes place in the ordinary slice 2-category K/XK/X. Recalling the theorems about iterated fibrations, a context such as x:A +,y:B(x) +x:A^+, y:B(x)^+ indicates that we work in Opf Opf(A)(BA)=Opf(B)Opf_{Opf(A)}(B\to A) = Opf(B), while x:A +,y:B x:A^+, y:B^- indicates working in the two-sided fibrational slice Fib(A,B)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:Bx:B, where BB is a 0-type, means working in the slice 1-category of discrete objects over BB. 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:Bx:A^+ | y:B

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

We say that a context is fibrational if no ϵ k\epsilon_k (in its 1-context section) is equal to 00. 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 Γ 0\Gamma^0 for the context obtained from Γ\Gamma by dropping all variances (changing all ϵ k\epsilon_k to 00).

The reason we write A +A^+ and A A^- instead of AA and A opA^{op} is that a judgement written like x:A opb(x):Bx:A^{op} \vdash b(x):B looks as though we are defining a contravariant functor from AA to BB, 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

Γ ±A:TypeΓ ±,x:A B:TypeΓ ±Σ x:A B:Type(fibrational sum type)\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.

Γ ±A:TypeΓ ±,x:A B:TypeΓ ±,x:Σ x:A Bproj(x):A\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)proj(x) is a term with free variable xx, so it is automatically functorial and acts on arrows as well as elements.

Γ ±A:TypeΓ ±,x:A B:TypeΓ ±,x:A,y:A,f:hom A(y,x),u:Bf *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 f^*u : B[y/x]}

Γ ±A:TypeΓ ±,x:A B:TypeΓ ±,x:A,y:A,f:hom A(y,x),u:Bcart(u):hom Σ x:A B(f *u,u)\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:

Γ ±A:TypeΓ ±,x:A +B:TypeΓ ±Σ x:A +B:Type(opfibrational sum type)\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 !uf_!u and opcartesian arrows.

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