We introduce variables with variances. In the standard categorical interpretation of a context such as , the type that depends on a variable is interpreted by an object of a slice category ; the intuition being that for each the type is the fiber over of the map . 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
of variable declarations, such that:
We will often omit the superscript s. We then define a 0-context to be a 1-context together with a finite list
of variable declarations, such that for each , the judgement
is derivable, and a (-1)-context to be a 0-context together with a finite list
of propositions, such that for each , the judgement
The intended interpretation of these contexts is as follows. A context indicates that everything to its right takes place in the opfibrational slice . Likewise, indicates that everything to its right takes place in , while indicates that everything to its right takes place in the ordinary slice 2-category . Recalling the theorems about iterated fibrations, a context such as indicates that we work in , while indicates working in the two-sided fibrational slice . 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 , where is a 0-type, means working in the slice 1-category of discrete objects over . Similarly, once we pass the second , we are now working in a poset of subterminals, and a declaration means we assume that is true (which amounts to working in the slice poset over ). For example, a context such as
means working in .
We say that a context is fibrational if no (in its 1-context section) is equal to . 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 to mean that is a fibrational context, and if is any context, we write for the context obtained from by dropping all variances (changing all to ).
The reason we write and instead of and is that a judgement written like looks as though we are defining a contravariant functor from to , 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.
We now have rules relating elements and arrows in sum types to those in the base, which essentially express the factorization properties of fibrations.
Note that is a term with free variable , so it is automatically functorial and acts on arrows as well as elements.
(Add a factorization axiom)
Of course, we have the analogous sums for opfibrations:
We trust the reader to write down the dual rules dealing with and opcartesian arrows.