This page, and subsequent ones, contains an overview of my current thinking about the “internal logic of a 2-category”, as part of the 2-categorical logic project. This logic is not by any means set in stone; it’s simply the most recent incarnation (or, more accurately, the most recent incarnation that I’ve managed to write up) of evolving ideas. Any suggestions for improvement are greatly appreciated.
As adumbrated at categorified logic, the logic we use will be a logic of dependent types. In general, we allow three different sorts of types, which we call 1-types (categories, sort denoted ), 0-types (sets, sort denoted ), and (-1)-types (propositions, sort denoted ). We could include (0,1)-types (posets) and (1,0)-types (groupoids) as well, but these rarely seem as important as the other three; thus we will just identify posets and groupoids with particular categories. (Note that by using the word “set” for the 0-types, we do not in general intend to imply any smallness condition on them.)
Eventually, we will allow dependent types, with dependencies of -types on -types whenever . This will eventually involve additional subtleties with dependent products and sums, which require the “variance” of the dependencies to be specified. For now, however, we will focus on first-order logic, with no “real” type dependencies. We will also make minimal use of the sort . We do, however, require two type dependencies: dependency of propositions on types (i.e. predicate logic) and -types which are dependent on objects. The latter will be the only types of sort we consider for now. However, we set up some of the basic notions in more generality, so as not to have to re-do them later.
Hom-types and equality types
A basic tenet of higher category theory is that if is an -category and then is an -category. For us, this means that if is an -type and then we have a dependent -type . For instance, if , then is a 0-type: the type of arrows from to . And if , then is a (-1)-type; in other words, a proposition, which we of course interpret as the assertion . (If , it would instead be the assertion .) So equality is a special case of the formation of hom-types.
In particular, note that equality, as a proposition, is only defined between elements of a 0-type. Thus, our language doesn’t even have the terminology to speak about equality between objects of a 1-type (category), only equality between elements of a 0-type (such as arrows in a category). This is also known as the “Speak No Evil” approach to category theory.
But if thought corrupts language, language can also corrupt thought. – George Orwell
Of course, these arrow-types are notably similar to the identity types in many versions of traditional Martin-Lof dependent type theory. In fact, it is well-known by now that equality types can be usefully interpreted in categories of groupoids or in homotopical categories. (Hoffman-Striecher, “The groupoid interpretation of type theory”; Awodey-Warren, “Homotopy theoretic models of identity types”.) Of course, the main difference is that arrow-types are (in general) directional. This makes it trickier to formulate “elimination rules” that generalize the rules for ordinary identity types, but we can still have a go?. We ought also to be able to construct “iso-types” as subtypes of , which will behave like identity types. This will all come later, however.
Contexts and Judgments
Treating -types on an equal footing for all , we can say that our theories will consist only of two sorts of judgments:
- (type declarations)
- (term declaration)
In each case is a context, such as , which declares the variables that occur in the rest of the judgement. Each type occurring in can depend on the variables occurring before it; thus we can have but not . Formally, this means that the contexts are generated inductively according to the following rules:
- The empty list is a context.
- If is a context and is derivable (where variables of can appear in ), and is a fresh variable not appearing in , then is a context.
Whenever we write a context it is assumed that there is no duplication of variables; this results in implicit hypotheses on the derivation rules.
To keep things looking familiar, we will usually write instead of , instead of , and instead of . Moreover, since any two inhabitants of a (-1)-type are indistinguishable (since our type theory is extensional and proof-irrelevant), we will generally write merely instead of when is a (-1)-type (a proposition). For the same reason, we never need to think about equality for inhabitants of propositions. Likewise, there can be no interesting dependence of a proposition on another proposition, so we omit propositions from the declarations of other propositions. We do, however, allow terms of an -type to depend on a variable of an -type for any and , even .
Rules for deriving judgements
As is usual in type theories, we write
to mean that from the judgements and , we can deduce the judgement . We write for the right-hand side of an arbitrary judgement of any sort. We write for the result of substituting the term for the variable in , and we do the same for contexts.
The following rules are the basic ones for first-order 2-categorical logic. We will add additional rules in later sections, to deal with size and type dependency. Of course, any particular theory will have its own additional basic types, terms, and axioms as well.
These are just the same as in ordinary type theory, and fairly boring.
The exchange rule has, of course, the extra restriction that cannot occur freely in the type .
As suggested above, propositional equality is only meaningful for terms of a 0-type. Recall that for now, the only 0-types we consider will be hom-sets (or constructed from hom-sets).
There are also the usual symmetry, transitivity, and substitution rules for equality. These can probably be formulated only using substitution, in the style of identity types.
In theory, there should be a “directional elimination rule” for arrow-types, akin to the elimination rule for identity types in ordinary intensional type theory. However, for its correct formulation this will certainly require functorially dependent types, and it’s not even entirely clear what it should say then. So we will just directly assert the following basic operations on arrows.
Functoriality and naturality
Functoriality is probably the most subtle of the rules for arrow types. The idea is that a term declaration of the form describes a morphism in the ambient 2-category from the object representing the context to the object representing the term . But morphisms in a 2-category act like functors in the internal logic, and functors act on arrows as well as objects.
The term does not indicate any actual substitution of for (which would be nonsensical since they have different types). Rather, it is a decoration which converts the term with free variable into a term with free variable . In particular, is free in while is no longer free.
Similarly, a term should represent a 2-cell between the morphisms represented by and , which should be a natural transformation in the internal logic.
The logical operations on propositions are morally special cases of operations on dependent types. But real dependent types will come later, so we introduce the logical operations explicitly now. We list all the possible logical operations here, but we will also be interested in fragments of logic containing only some of these operations.
We may also have infinitary conjunctions, with an evident extension of the rules.
We may also have infinitary disjunctions, with an evident extension of the rules. In a theory lacking implication, we also require explicitly the distributive axiom:
We have quantification over both 1-types and 0-types, beginning with existential quantification:
In the above elimination rule, cannot occur free in . In a theory lacking implication, we must also assert the Frobenius axiom:
First-order 2-categorical theories
A 2-categorical first-order theory, or a first-order 2-theory for short, consists of:
the choice of a particular fragment of the logical rules.
a set of basic (non-dependent) 1-types , i.e. axioms of the form .
a set of basic (non-dependent) 0-types, i.e. axioms of the form .
a set of basic dependent propositions, i.e. axioms of the form . Here will depend on the typed variables occurring in .
a set of basic terms-in-context, i.e. axioms of the form . We require that these axioms come with a well-founded ordering, such that is provable from axioms preceeding it and based on the chosen logical fragment. Note that we also allow to contain propositions.
strictly speaking, the previous list of axioms includes logical axioms, but we can state these separately anyway: a set of axioms of the form , where is provable. Note that of course, can include propositions as well as 1-types and 0-types.
Note that we do not allow axiomatic dependent 1-types or 0-types. The problem with these is that they generally need to be “functorially” dependent, and we don’t want to get into that now.
Fragments of logic
The most commonly relevant fragments of logic are:
cartesian logic: the only logical constructors are and binary . (Of course, we always have equality for terms of a 0-type as atomic formulas.)
regular logic: , binary , and (plus the Frobenius rule).
coherent logic: , binary , , binary , and (plus the distributivity and Frobenius rules).
geometric logic: , binary , , arbitrary , and (plus the (infinitary) distributivity and Frobenius rules).
(finitary: first-order logic: , binary , , binary , , , and .
Examples of 2-categorical theories
Firstly, any ordinary 1-categorical theory can be regarded as a 2-categorical theory with no basic 1-types, and whose basic 0-types, terms, and propositions are those of the given theory. The necessary fragment of logic will be the same. As a special case of this, any propositional theory can be regarded as a 2-categorical theory with no 1-types or 0-types.
The theory of a monoidal category
In this theory there is one basic 1-type, call it , and no basic 0-types or propositions. We have the following axiomatic terms:
Note the necessary use of the functoriality term-constructors in stating the two coherence axioms. Strictly speaking, we should have stated the multiplication as , so that then would be written as , and the action of functoriality such as would be written as .
The theory of a monad
Again there is one basic 1-type, call it , no basic 0-types or propositions, and the following axiomatic terms:
The theory of an adjunction
Here we have two basic 1-types and , no basic 0-types or propositions, and the following terms:
However, see also the page adjunctions in 2-logic for some other equivalent ways of describing adjunctions.
Interpretation in a 2-category
One subtle point of difference with the 1-categorical theory is that propositions are always interpreted by subobjects in , no matter what the context. Since not every subobject of an object of a slice 2-category is necessarily a subobject in , that means that working in in a nonempty context is not quite the same as working in in the empty context. Other than that, things are pretty straightforward.
Let be a 2-categorical theory be a 2-category with sufficient structure to interpret . That means that:
- if is cartesian, then has finite limits,
- if is regular, then is regular,
- if is coherent, then is coherent,
- if is geometric, then is infinitary-coherent, and
- if is finitary first-order, then is Heyting.
We now define the following things by mutual induction:
- for any context , an object of ,
- for any judgment , a morphism which is -truncated, and
- for every term , a section of the above morphism.
Here is the definition:
- Given and the interpretation , we interpret the extended context by .
- For each basic 1-type , we pick an object of , and for any we set .
- For each basic 0-type , we pick a discrete object of , and we likewise set .
- For each basic dependent proposition , we pick a subobject of , and we set .
- If contains the variable , then we interpret the term via the evident projection.
- Given terms and , for a 1-type, we therefore have two projections , and we let be the inserter of and .
- Given terms and where , we let be the equalizer of . This is sensible since is discrete.
- As a special case of the latter, given terms and and and for a 1-type, and therefore having two projections and two 2-cells , we let be the equifier of and .
- For each basic term , we pick a section of .
- We let , of course, and (intersection as subobjects of .
- If is coherent, we let be the initial object, and (union as subobjects of . Similarly for if is infinitary-coherent.
- If is regular, given with , we let be the image of along the projection .
- Finally, if is Heyting, given with , we let be the dual image of along the projection .
This interpretation is sound. In other words, the induction succeeds, and all the rules for term-formation (including all the logical rules) can be interpreted.
Of course, the definition of the interpretation depends on our choosing interpretations of the basic types and terms. For example:
- A model in of the theory of a monoidal category is precisely a pseudomonoid in .
- Of course, a model in of the theory of a monad, or an adjunction, is precisely a monad or adjunction in .
- If is a 1-categorical theory, then a model of (regarded as a 2-categorical theory) in is precisely a model of the original theory in the category of discrete objects in .
- Similarly, if is a propositional theory, then a model of in lives in the poset of subterminal objects.
The internal theory of a 2-category
Any 2-category comes with a “canonical” theory associated to it, which has a canonical model in . In this theory:
- the basic 1-types are all the objects of , with interpretation the identity.
- the basic 0-types are all the discrete objects of , with interpretation the identity.
- the basic dependent propositions in a context , are all the subobjects of in .
- the basic terms of a type in context are all the sections in of the morphism .
Of course, this definition is again inductive, so one has to prove that the induction succeeds. Usually when we refer to the internal logic of a 2-category it is this logic we are talking about. Of course, whatever logical structure has (regular, coherent, etc.) can be reflected in its internal logic.