Michael Shulman
internal logic of a 2-category

Introduction

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 CatCat), 0-types (sets, sort denoted SetSet), and (-1)-types (propositions, sort denoted PropProp). 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 nn-types on mm-types whenever nmn\le m. 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 SetSet. We do, however, require two type dependencies: dependency of propositions on types (i.e. predicate logic) and homhom-types which are dependent on objects. The latter will be the only types of sort SetSet 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 AA is an nn-category and x,yAx,y\in A then hom A(x,y)hom_A(x,y) is an (n1)(n-1)-category. For us, this means that if AA is an nn-type and x:A,y:Ax:A,y:A then we have a dependent (n1)(n-1)-type hom A(x,y)hom_A(x,y). For instance, if n=1n=1, then hom A(x,y)hom_A(x,y) is a 0-type: the type of arrows from xx to yy. And if n=0n=0, then hom A(x,y)hom_A(x,y) is a (-1)-type; in other words, a proposition, which we of course interpret as the assertion x=yx=y. (If n=(0,1)n=(0,1), it would instead be the assertion xyx\le y.) 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” iso A(x,y)iso_A(x,y) as subtypes of hom A(x,y)hom_A(x,y), which will behave like identity types. This will all come later, however.

Contexts and Judgments

Treating nn-types on an equal footing for all nn, we can say that our theories will consist only of two sorts of judgments:

  • ΓA:nType\Gamma \vdash A:n Type (type declarations)
  • Γa:A\Gamma \vdash a:A (term declaration)

In each case Γ\Gamma is a context, such as x:A,y:B,z:Cx:A,y:B,z:C, which declares the variables that occur in the rest of the judgement. Each type occurring in Γ\Gamma can depend on the variables occurring before it; thus we can have x:A,y:B(x)x:A, y:B(x) but not x:A(y),y:Bx:A(y), y:B. Formally, this means that the contexts are generated inductively according to the following rules:

  • The empty list is a context.
  • If Γ\Gamma is a context and ΓA:nType\Gamma \vdash A:n Type is derivable (where variables of Γ\Gamma can appear in AA), and xx is a fresh variable not appearing in Γ\Gamma, then Γ,x:A\Gamma, x:A 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 PropProp instead of (1)Type(-1)Type, SetSet instead of 0Type0 Type, and CatCat instead of 1Type1Type. 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 φ\varphi instead of x:φx:\varphi when φ\varphi 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 nn-type to depend on a variable of an mm-type for any nn and mm, even m=1m=-1.

Rules for deriving judgements

As is usual in type theories, we write

ABC\frac{A \qquad B}{C}

to mean that from the judgements AA and BB, we can deduce the judgement CC. We write JJ for the right-hand side of an arbitrary judgement of any sort. We write J[a/x]J[a/x] for the result of substituting the term aa for the variable xx in JJ, 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.

Structural rules

These are just the same as in ordinary type theory, and fairly boring.

ΓA:nTypeΓ,x:Ax:A(projection)\frac{\Gamma\vdash A:n Type}{\Gamma, x:A \vdash x:A} (projection)

Γa:AΓ,x:A,ΔJΓ,Δ[a/x]J[a/x](substitution)\frac{\Gamma\vdash a:A \qquad \Gamma, x:A, \Delta \vdash J} {\Gamma, \Delta[a/x] \vdash J[a/x]} (substitution)

Γ,x:A,y:A,ΔJΓ,x:A,Δ[x/y]J[x/y](contraction)\frac{\Gamma, x:A, y:A, \Delta \vdash J} {\Gamma,x:A, \Delta[x/y] \vdash J[x/y]} (contraction)

ΓA:nTypeΓJΓ,x:AJ(weakening)\frac{\Gamma \vdash A:n Type \qquad \Gamma\vdash J}{\Gamma, x:A \vdash J} (weakening)

Γ,x:A,y:B,ΔJΓ,y:B,x:A,ΔJ(exchange)\frac{\Gamma, x:A, y:B, \Delta \vdash J} {\Gamma, y:B, x:A, \Delta \vdash J} (exchange)

The exchange rule has, of course, the extra restriction that xx cannot occur freely in the type BB.

Propositional equality

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

ΓA:SetΓ,x:A,y:A(x=y):Prop(equality)\frac{\Gamma \vdash A:Set} {\Gamma, x:A, y:A \vdash (x=y):Prop} (equality)

ΓA:SetΓ,x:A(x=x)(reflexivity)\frac{\Gamma \vdash A:Set}{\Gamma, x:A \vdash (x=x)} (reflexivity)

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.

Arrow types

ΓA:CatΓ,x:A,y:Ahom A(x,y):Set(arrowtype)\frac{\Gamma \vdash A:Cat} {\Gamma, x:A, y:A \vdash hom_A(x,y):Set} (arrow type)

ΓA:CatΓ,x:A1 x:hom A(x,x)(identities)\frac{\Gamma \vdash A:Cat} {\Gamma, x:A\vdash 1_x:hom_A(x,x)} (identities)

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.

ΓA:CatΓ,x:A,y:A,z:A,f:hom A(x,y),g:hom A(y,z)gf:hom A(x,z)(composition)\frac{\Gamma \vdash A:Cat} {\Gamma, x:A, y:A, z:A, f:hom_A(x,y), g:hom_A(y,z)\vdash g\circ f: hom_A(x,z)} (composition)

ΓA:CatΓ,x:A,y:A,z:A,w:A,f:hom A(x,y),g:hom A(y,z),h:hom A(z,w)(h(gf)=(hg)f)(associativity)\frac{\Gamma \vdash A:Cat} {\Gamma, x:A, y:A, z:A, w:A, f: hom_A(x,y), g:hom_A(y,z), h:hom_A(z,w) \vdash (h \circ (g\circ f) = (h\circ g)\circ f)} (associativity)

ΓA:CatΓ,x:A,y:A,f:hom A(x,y)((f1 x)=f)(rightunit)\frac{\Gamma \vdash A:Cat} {\Gamma, x:A, y:A, f:hom_A(x,y) \vdash ((f\circ 1_x) = f)}(right unit)

ΓA:TypeΓ,x:A,y:A,f:hom A(x,y)|((1 yf)=f)(leftunit)\frac{\Gamma \vdash A:Type} {\Gamma, x:A, y:A, f:hom_A(x,y) | \top \vdash ((1_y\circ f) = f)}(left unit)

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 Γb:B\Gamma \vdash b:B describes a morphism in the ambient 2-category from the object representing the context Γ\Gamma to the object representing the term BB. But morphisms in a 2-category act like functors in the internal logic, and functors act on arrows as well as objects.

B:CatΓ,x:Ab:BΓ,y:A,z:A,f:hom A(y,z)b(f/x):hom B(b[y/x],b[z/x])(functoriality)\frac{\vdash B:Cat \qquad \Gamma, x:A \vdash b:B} {\Gamma, y:A, z:A, f:hom_A(y,z) \vdash b(f/x): hom_B(b[y/x],b[z/x])} (functoriality)

The term b(f/x)b(f/x) does not indicate any actual substitution of ff for xx (which would be nonsensical since they have different types). Rather, it is a decoration which converts the term b:Bb:B with free variable x:Ax:A into a term b(f/x):hom B(b[y/x],b[z/x])b(f/x): hom_B(b[y/x],b[z/x]) with free variable f:hom A(y,z)f:hom_A(y,z). In particular, ff is free in b(f/x)b(f/x) while xx is no longer free.

Γ,x:AB:CatΓ,x:Ab:BΓ,x:A(b(1 y/x)=1 b[y/x])(functorialityonidentities)\frac{\Gamma,x:A \vdash B:Cat \qquad \Gamma, x:A \vdash b:B} {\Gamma, x:A \vdash (b(1_y/x) = 1_{b[y/x]})} (functoriality on identities)

Γ,x:AB:CatΓ,x:Ab:BΓ,y:A,z:A,w:A,f:hom A(y,z),g:hom A(z,w)b(g/x)b(f/x)=b(gf/x)(functorialityoncomposition)\frac{\Gamma, x:A \vdash B:Cat \qquad \Gamma, x:A \vdash b:B} {\Gamma, y:A, z:A, w:A, f:hom_A(y,z), g:hom_A(z,w) \vdash b(g/x) \circ b(f/x) = b(g\circ f/x)} (functoriality on composition)

Similarly, a term Γ,x:Aj:hom B(b 1,b 2)\Gamma, x:A \vdash j:hom_B(b_1,b_2) should represent a 2-cell between the morphisms represented by b 1b_1 and b 2b_2, which should be a natural transformation in the internal logic.

Γ,x:AB:CatΓ,x:Aj:hom B(b 1,b 2)Γ,y:A,z:A,f:hom A(y,z)(j[z/x]b 1(f/x)=b 2(g/x)j[y/x])(naturality)\frac{\Gamma, x:A \vdash B:Cat \qquad \Gamma, x:A \vdash j:hom_B(b_1,b_2)} {\Gamma, y:A, z:A, f:hom_A(y,z) \vdash (j[z/x] \circ b_1(f/x) = b_2(g/x) \circ j[y/x])}(naturality)

Logical operations

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.

Truth:

:Prop\frac{}{\vdash \top:Prop}

\frac{}{\vdash \top}

Conjunction:

Γφ:PropΓψ:PropΓ(φψ):Prop\frac{\Gamma \vdash \varphi:Prop \qquad \Gamma \vdash \psi:Prop}{\Gamma \vdash (\varphi\wedge\psi) :Prop}

ΓφΓψΓ(φψ)\frac{\Gamma \vdash \varphi \qquad \Gamma \vdash \psi}{\Gamma \vdash (\varphi\wedge\psi)}

Γ(φψ)ΓφΓψ\frac{\Gamma \vdash (\varphi\wedge\psi)}{\Gamma \vdash \varphi \qquad \Gamma \vdash \psi}

We may also have infinitary conjunctions, with an evident extension of the rules.

Falsity:

:Prop\frac{}{\vdash \bot:Prop}

ΓΓφ:PropΓφ\frac{\Gamma \vdash \bot \qquad \Gamma \vdash \varphi:Prop}{\Gamma \vdash \varphi}

Disjunction:

Γφ:PropΓψ:PropΓ(φψ):Prop\frac{\Gamma \vdash \varphi:Prop \qquad \Gamma \vdash \psi:Prop}{\Gamma \vdash (\varphi\vee\psi) :Prop}

ΓφΓ(φψ)\frac{\Gamma \vdash \varphi}{\Gamma\vdash (\varphi\vee\psi)}

ΓψΓ(φψ)\frac{\Gamma \vdash \psi}{\Gamma\vdash (\varphi\vee\psi)}

Γ,φχΓ,ψχΓ,(φψ)χ\frac{\Gamma, \varphi \vdash \chi \qquad \Gamma,\psi \vdash \chi}{\Gamma, (\varphi\vee\psi) \vdash \chi}

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:

Γ(φ(ψχ))Γ(φψ)(φχ)\frac{\Gamma \vdash (\varphi\wedge (\psi\vee\chi))}{\Gamma \vdash (\varphi\wedge \psi)\vee(\varphi\wedge \chi)}

Implication:

Γφ:PropΓψ:PropΓφψ:Prop\frac{\Gamma \vdash \varphi:Prop \qquad \Gamma \vdash \psi :Prop}{\Gamma \vdash \varphi\Rightarrow\psi :Prop}

Γ,φψΓφψ\frac{\Gamma, \varphi \vdash \psi}{\Gamma \vdash \varphi\Rightarrow\psi}

ΓφψΓ,φψ\frac{\Gamma \vdash \varphi\Rightarrow\psi}{\Gamma, \varphi \vdash \psi}

We have quantification over both 1-types and 0-types, beginning with existential quantification:

ΓA:nTypeΓ,x:Aφ(x):PropΓ(x:A)φ(x):Prop\frac{\Gamma \vdash A:n Type\qquad \Gamma, x:A \vdash \varphi(x):Prop}{\Gamma \vdash (\exists x:A) \varphi(x) :Prop}

Γt:AΓφ(t)Γ(x:A)φ(x)\frac{\Gamma \vdash t:A \qquad \Gamma \vdash \varphi(t)}{\Gamma \vdash (\exists x:A) \varphi(x)}

Γ,x:A,φ(x)ψΓ,(x:A)φ(x)ψ\frac{\Gamma, x:A, \varphi(x) \vdash \psi}{\Gamma, (\exists x:A)\varphi(x) \vdash \psi}

In the above elimination rule, xx cannot occur free in ψ\psi. In a theory lacking implication, we must also assert the Frobenius axiom:

Γ(φ(x:A)ψ(x))Γ(x:A)(φψ(x))\frac{\Gamma \vdash (\varphi \wedge (\exists x:A)\psi(x))}{\Gamma \vdash (\exists x:A)(\varphi\wedge \psi(x))}

Universal quantification:

ΓA:nTypeΓ,x:Aφ(x):PropΓ(x:A)φ(x):Prop\frac{\Gamma \vdash A:n Type\qquad \Gamma, x:A \vdash \varphi(x):Prop}{\Gamma \vdash (\forall x:A) \varphi(x) :Prop}

Γ,x:Aφ(x)Γ(x:A)φ(x)\frac{\Gamma, x:A \vdash \varphi(x)}{\Gamma \vdash (\forall x:A) \varphi(x)}

Γ(x:A)φ(x)Γ,x:Aφ(x)\frac{\Gamma \vdash (\forall x:A)\varphi(x)}{\Gamma, x:A \vdash \varphi(x)}

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 A,B,A,B,\dots, i.e. axioms of the form A:1Type\vdash A:1 Type.

  • a set of basic (non-dependent) 0-types, i.e. axioms of the form A:0Type\vdash A:0 Type.

  • a set of basic dependent propositions, i.e. axioms of the form Γφ:Prop\Gamma \vdash \varphi:Prop. Here φ\varphi will depend on the typed variables occurring in Γ\Gamma.

  • a set of basic terms-in-context, i.e. axioms of the form Γt:A\Gamma \vdash t:A. We require that these axioms come with a well-founded ordering, such that ΓA:nType\Gamma \vdash A:n Type is provable from axioms preceeding it and based on the chosen logical fragment. Note that we also allow Γ\Gamma 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 Γφ\Gamma \vdash \varphi, where Γφ:Prop\Gamma \vdash \varphi:Prop is provable. Note that of course, Γ\Gamma 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 \top and binary \wedge. (Of course, we always have equality for terms of a 0-type as atomic formulas.)

  • regular logic: \top, binary \wedge, and \exists (plus the Frobenius rule).

  • coherent logic: \top, binary \wedge, \bot, binary \vee, and \exists (plus the distributivity and Frobenius rules).

  • geometric logic: \top, binary \wedge, \bot, arbitrary \bigvee, and \exists (plus the (infinitary) distributivity and Frobenius rules).

  • (finitary: first-order logic: \top, binary \wedge, \bot, binary \vee, \Rightarrow, \exists, and \forall.

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 VV, and no basic 0-types or propositions. We have the following axiomatic terms:

  • i:V\vdash i:V
  • x:V,y:V(xy):Vx:V,y:V\vdash (x\otimes y):V
  • x:V,y:V,z:Vα x,y,z:hom V((xy)z,x(yz))x:V,y:V,z:V \vdash \alpha_{x,y,z}:hom_V((x\otimes y)\otimes z, x\otimes (y\otimes z))
  • x:Vλ x:hom V(ix,x)x:V \vdash \lambda_x : hom_V(i\otimes x,x)
  • x:Vρ x:hom V(xi,x)x:V \vdash \rho_x : hom_V(x\otimes i,x)
  • x:V,y:V,z:V,w:Vα x,y,zwα xy,z,w=(xα y,z,w)α x,yz,w(α x,y,zw)x:V,y:V,z:V,w:V \vdash \alpha_{x,y,z\otimes w} \circ \alpha_{x\otimes y, z,w} = (x\otimes \alpha_{y,z,w})\circ \alpha_{x,y\otimes z,w} \circ (\alpha_{x,y,z}\otimes w)
  • x:V,y:V(ρ xy)=(xλ y)α x,i,yx:V,y:V \vdash (\rho_x\otimes y) = (x\otimes \lambda_y) \circ \alpha_{x,i,y}

Note the necessary use of the functoriality term-constructors in stating the two coherence axioms. Strictly speaking, we should have stated the multiplication as x:V,y:Vmult:Vx:V,y:V\vdash mult:V, so that then aba\otimes b would be written as mult[a/x,b/y]mult[a/x,b/y], and the action of functoriality such as xα y,z,wx\otimes \alpha_{y,z,w} would be written as mult(α y,z,w/y)mult(\alpha_{y,z,w}/y).

The theory of a monad

Again there is one basic 1-type, call it AA, no basic 0-types or propositions, and the following axiomatic terms:

  • x:At(x):Ax:A \vdash t(x):A
  • x:Aη x:hom A(x,t(x))x:A \vdash \eta_x : hom_A(x,t(x))
  • x:Aμ x:hom A(t(t(x)),t(x))x:A \vdash \mu_x : hom_A(t(t(x)),t(x))
  • x:Aμ xt(η x/x)=1 t(x)x:A \vdash \mu_x \circ t(\eta_x/x) = 1_{t(x)}
  • x:Aμ xη t(x)=1 t(x)x:A \vdash \mu_x \circ \eta_{t(x)} = 1_{t(x)}
  • x:Aμ xμ t(x)=μ xt(μ x/x)x:A \vdash \mu_x \circ \mu_{t(x)} = \mu_x \circ t(\mu_x/x)

The theory of an adjunction

Here we have two basic 1-types AA and BB, no basic 0-types or propositions, and the following terms:

  • x:Af(x):Bx:A \vdash f(x):B
  • y:Bg(y):Ay:B \vdash g(y):A
  • x:Aη x:hom A(x,g(f(x)))x:A \vdash \eta_x:hom_A(x,g(f(x)))
  • y:Bε y:hom B(f(g(y)),y)y:B \vdash \varepsilon_y:hom_B(f(g(y)),y)
  • x:Aε f(x)f(η x)=1 f(x)x:A \vdash \varepsilon_{f(x)} \circ f(\eta_x) = 1_{f(x)}
  • y:Bg(ε y)η g(y)=1 g(y)y:B \vdash g(\varepsilon_{y}) \circ \eta_{g(y)} = 1_{g(y)}

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 KK, no matter what the context. Since not every subobject of an object of a slice 2-category K/AK/A is necessarily a subobject in KK, that means that working in KK in a nonempty context Γ\Gamma is not quite the same as working in K/[Γ]K/[\Gamma] in the empty context. Other than that, things are pretty straightforward.

Let TT be a 2-categorical theory KK be a 2-category with sufficient structure to interpret TT. That means that:

  • if TT is cartesian, then KK has finite limits,
  • if TT is regular, then KK is regular,
  • if TT is coherent, then KK is coherent,
  • if TT is geometric, then KK is infinitary-coherent, and
  • if TT is finitary first-order, then KK is Heyting.

We now define the following things by mutual induction:

  • for any context Γ\Gamma, an object [Γ][\Gamma] of KK,
  • for any judgment ΓA:nType\Gamma\vdash A:n Type, a morphism [A] Γ[Γ][A]_\Gamma\to [\Gamma] which is nn-truncated, and
  • for every term Γt:A\Gamma \vdash t:A, a section of the above morphism.

Here is the definition:

  • Given [Γ][\Gamma] and the interpretation [A] Γ[Γ][A]_\Gamma\to [\Gamma], we interpret the extended context Γ,x:A\Gamma, x:A by [Γ,x:A]=[A] Γ[\Gamma,x:A] = [A]_\Gamma.
  • For each basic 1-type AA, we pick an object [A][A] of KK, and for any Γ\Gamma we set [A] Γ=[Γ]×[A][A]_\Gamma = [\Gamma] \times [A].
  • For each basic 0-type BB, we pick a discrete object [B][B] of KK, and we likewise set [B] Γ=[Γ]×[B][B]_\Gamma = [\Gamma] \times [B].
  • For each basic dependent proposition Γφ:Prop\Gamma \vdash \varphi:Prop, we pick a subobject of [Γ][\Gamma], and we set [φ] Γ=[φ][\varphi]_\Gamma = [\varphi].
  • If Γ\Gamma contains the variable x:Ax:A, then we interpret the term Γx:A\Gamma \vdash x:A via the evident projection.
  • Given terms Γx:A\Gamma\vdash x:A and Γy:A\Gamma\vdash y:A, for AA a 1-type, we therefore have two projections [x],[y]:[Γ][A][x],[y]\colon [\Gamma] \to [A], and we let [hom A(x,y)] Γ[hom_A(x,y)]_\Gamma be the inserter of [x][x] and [y][y].
  • Given terms Γx:B\Gamma\vdash x:B and Γy:B\Gamma\vdash y:B where ΓB:Set\Gamma\vdash B: Set, we let [x=y] Γ[x=y]_\Gamma be the equalizer of [x],[y]:[Γ][B] Γ[x],[y]:[\Gamma] \to [B]_\Gamma. This is sensible since [B] Γ[B]_\Gamma is discrete.
  • As a special case of the latter, given terms Γx:A\Gamma\vdash x:A and Γy:A\Gamma\vdash y:A and Γf:hom A(x,y)\Gamma\vdash f:hom_A(x,y) and Γg:hom A(x,y)\Gamma\vdash g:hom_A(x,y) for AA a 1-type, and therefore having two projections [x],[y]:[Γ][A][x],[y]:[\Gamma] \to [A] and two 2-cells [f],[g]:[x][y][f],[g]\colon [x]\to [y], we let [f=g] Γ[f=g]_\Gamma be the equifier of [f][f] and [g][g].
  • For each basic term Γt:A\Gamma \vdash t:A, we pick a section of [A] Γ[Γ][A]_\Gamma \to [\Gamma].
  • We let [] Γ=[Γ][Γ][\top]_\Gamma = [\Gamma] \to [\Gamma], of course, and [φψ] Γ=[φ] Γ[ψ] Γ[\varphi\wedge \psi]_\Gamma = [\varphi]_\Gamma \cap [\psi]_\Gamma (intersection as subobjects of [Γ][\Gamma].
  • If KK is coherent, we let [] Γ[\bot]_\Gamma be the initial object, and [φψ] Γ=[φ] Γ[ψ] Γ[\varphi\vee \psi]_\Gamma = [\varphi]_\Gamma \cup [\psi]_\Gamma (union as subobjects of [Γ][\Gamma]. Similarly for \bigvee if KK is infinitary-coherent.
  • If KK is regular, given Γ,x:Aφ(x)\Gamma, x:A \vdash \varphi(x) with [φ] Γ,x:A[Γ,x:A][Γ][\varphi]_{\Gamma, x:A} \hookrightarrow [\Gamma, x:A] \to [\Gamma], we let [(x:A)φ(x)] Γ[Γ][(\exists x:A)\varphi(x)]_\Gamma \hookrightarrow [\Gamma] be the image of [φ] Γ,x:A[\varphi]_{\Gamma, x:A} along the projection [Γ,x:A][Γ][\Gamma, x:A] \to [\Gamma].
  • Finally, if KK is Heyting, given Γ,x:Aφ(x)\Gamma, x:A \vdash \varphi(x) with [φ] Γ,x:A[Γ,x:A][Γ][\varphi]_{\Gamma, x:A} \hookrightarrow [\Gamma, x:A] \to [\Gamma], we let [(x:A)φ(x)] Γ[Γ][(\forall x:A)\varphi(x)]_\Gamma \hookrightarrow [\Gamma] be the dual image of [φ] Γ,x:A[\varphi]_{\Gamma, x:A} along the projection [Γ,x:A][Γ][\Gamma, x:A] \to [\Gamma].
Theorem

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 KK of the theory of a monoidal category is precisely a pseudomonoid in KK.
  • Of course, a model in KK of the theory of a monad, or an adjunction, is precisely a monad or adjunction in KK.
  • If TT is a 1-categorical theory, then a model of TT (regarded as a 2-categorical theory) in KK is precisely a model of the original theory TT in the category of discrete objects in KK.
  • Similarly, if TT is a propositional theory, then a model of TT in KK lives in the poset of subterminal objects.

The internal theory of a 2-category

Any 2-category KK comes with a “canonical” theory associated to it, which has a canonical model in KK. In this theory:

  • the basic 1-types are all the objects of KK, with interpretation the identity.
  • the basic 0-types are all the discrete objects of KK, with interpretation the identity.
  • the basic dependent propositions in a context Γ\Gamma, are all the subobjects of [Γ][\Gamma] in KK.
  • the basic terms of a type AA in context Γ\Gamma are all the sections in KK of the morphism [A] Γ[Γ][A]_\Gamma \to [\Gamma].

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 KK has (regular, coherent, etc.) can be reflected in its internal logic.

Revised on May 31, 2011 16:22:43 by Mike Shulman (71.136.238.9)