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

Contexts and Judgments

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

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

In each case $\Gamma$ is a context, such as $x: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)$ but not $x: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 $\Gamma \vdash A:n Type$ is derivable (where variables of $\Gamma$ can appear in $A$), and $x$ is a fresh variable not appearing in $\Gamma$, then $\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 $Prop$ instead of $(-1)Type$, $Set$ instead of $0 Type$, and $Cat$ instead of $1Type$. 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:\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 $n$-type to depend on a variable of an $m$-type for any $n$ and $m$, even $m=-1$.

Rules for deriving judgements

As is usual in type theories, we write

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

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

$$\frac{\Gamma\vdash A:n Type}{\Gamma, x:A \vdash x:A} (projection)$$

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

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

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

$$\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 $x$ cannot occur freely in the type $B$.

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

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

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

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

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

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

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

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

$$\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 $\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 $B$. But morphisms in a 2-category act like functors in the internal logic, and functors act on arrows as well as objects.

$$\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)$ does not indicate any actual substitution of $f$ for $x$ (which would be nonsensical since they have different types). Rather, it is a decoration which converts the term $b:B$ with free variable $x:A$ into a term $b(f/x): hom_B(b[y/x],b[z/x])$ with free variable $f:hom_A(y,z)$. In particular, $f$ is free in $b(f/x)$ while $x$ is no longer free.

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

$$\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 $\Gamma, x:A \vdash j:hom_B(b_1,b_2)$ should represent a 2-cell between the morphisms represented by $b_1$ and $b_2$, which should be a natural transformation in the internal logic.

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

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

$$\frac{}{\vdash \top}$$

Conjunction:

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

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

$$\frac{\Gamma \vdash \bot \qquad \Gamma \vdash \varphi:Prop}{\Gamma \vdash \varphi}$$

Disjunction:

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

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

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

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

$$\frac{\Gamma, x:A, \varphi(x) \vdash \psi}{\Gamma, (\exists x:A)\varphi(x) \vdash \psi}$$

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

$$\frac{\Gamma \vdash (\varphi \wedge (\exists x:A)\psi(x))}{\Gamma \vdash (\exists x:A)(\varphi\wedge \psi(x))}$$

Universal quantification:

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

$$\frac{\Gamma, x:A \vdash \varphi(x)}{\Gamma \vdash (\forall x:A) \varphi(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,\dots$, i.e. axioms of the form $\vdash A:1 Type$.

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

• a set of basic dependent propositions, i.e. axioms of the form $\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 $\Gamma \vdash t:A$. We require that these axioms come with a well-founded ordering, such that $\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 $\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 $V$, and no basic 0-types or propositions. We have the following axiomatic terms:

• $\vdash i:V$
• $x:V,y:V\vdash (x\otimes y):V$
• $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 \vdash \lambda_x : hom_V(i\otimes x,x)$
• $x:V \vdash \rho_x : hom_V(x\otimes i,x)$
• $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 \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:V\vdash mult:V$, so that then $a\otimes b$ would be written as $mult[a/x,b/y]$, and the action of functoriality such as $x\otimes \alpha_{y,z,w}$ would be written as $mult(\alpha_{y,z,w}/y)$.

The theory of a monad

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

• $x:A \vdash t(x):A$
• $x:A \vdash \eta_x : hom_A(x,t(x))$
• $x:A \vdash \mu_x : hom_A(t(t(x)),t(x))$
• $x:A \vdash \mu_x \circ t(\eta_x/x) = 1_{t(x)}$
• $x:A \vdash \mu_x \circ \eta_{t(x)} = 1_{t(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 $A$ and $B$, no basic 0-types or propositions, and the following terms:

• $x:A \vdash f(x):B$
• $y:B \vdash g(y):A$
• $x:A \vdash \eta_x:hom_A(x,g(f(x)))$
• $y:B \vdash \varepsilon_y:hom_B(f(g(y)),y)$
• $x:A \vdash \varepsilon_{f(x)} \circ f(\eta_x) = 1_{f(x)}$
• $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 $K$, no matter what the context. Since not every subobject of an object of a slice 2-category $K/A$ is necessarily a subobject in $K$, that means that working in $K$ in a nonempty context $\Gamma$ is not quite the same as working in $K/[\Gamma]$ in the empty context. Other than that, things are pretty straightforward.

Let $T$ be a 2-categorical theory $K$ be a 2-category with sufficient structure to interpret $T$. That means that:

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

We now define the following things by mutual induction:

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

Here is the definition:

• Given $[\Gamma]$ and the interpretation $[A]_\Gamma\to [\Gamma]$, we interpret the extended context $\Gamma, x:A$ by $[\Gamma,x:A] = [A]_\Gamma$.
• For each basic 1-type $A$, we pick an object $[A]$ of $K$, and for any $\Gamma$ we set $[A]_\Gamma = [\Gamma] \times [A]$.
• For each basic 0-type $B$, we pick a discrete object $[B]$ of $K$, and we likewise set $[B]_\Gamma = [\Gamma] \times [B]$.
• For each basic dependent proposition $\Gamma \vdash \varphi:Prop$, we pick a subobject of $[\Gamma]$, and we set $[\varphi]_\Gamma = [\varphi]$.
• If $\Gamma$ contains the variable $x:A$, then we interpret the term $\Gamma \vdash x:A$ via the evident projection.
• Given terms $\Gamma\vdash x:A$ and $\Gamma\vdash y:A$, for $A$ a 1-type, we therefore have two projections $[x],[y]\colon [\Gamma] \to [A]$, and we let $[hom_A(x,y)]_\Gamma$ be the inserter of $[x]$ and $[y]$.
• Given terms $\Gamma\vdash x:B$ and $\Gamma\vdash y:B$ where $\Gamma\vdash B: Set$, we let $[x=y]_\Gamma$ be the equalizer of $[x],[y]:[\Gamma] \to [B]_\Gamma$. This is sensible since $[B]_\Gamma$ is discrete.
• As a special case of the latter, given terms $\Gamma\vdash x:A$ and $\Gamma\vdash y:A$ and $\Gamma\vdash f:hom_A(x,y)$ and $\Gamma\vdash g:hom_A(x,y)$ for $A$ a 1-type, and therefore having two projections $[x],[y]:[\Gamma] \to [A]$ and two 2-cells $[f],[g]\colon [x]\to [y]$, we let $[f=g]_\Gamma$ be the equifier of $[f]$ and $[g]$.
• For each basic term $\Gamma \vdash t:A$, we pick a section of $[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 $K$ 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 $K$ is infinitary-coherent.
• If $K$ is regular, given $\Gamma, x:A \vdash \varphi(x)$ with $[\varphi]_{\Gamma, x:A} \hookrightarrow [\Gamma, x:A] \to [\Gamma]$, we let $[(\exists x:A)\varphi(x)]_\Gamma \hookrightarrow [\Gamma]$ be the image of $[\varphi]_{\Gamma, x:A}$ along the projection $[\Gamma, x:A] \to [\Gamma]$.
• Finally, if $K$ is Heyting, given $\Gamma, x:A \vdash \varphi(x)$ with $[\varphi]_{\Gamma, x:A} \hookrightarrow [\Gamma, x:A] \to [\Gamma]$, we let $[(\forall x:A)\varphi(x)]_\Gamma \hookrightarrow [\Gamma]$ be the dual image of $[\varphi]_{\Gamma, x:A}$ along the projection $[\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 $K$ of the theory of a monoidal category is precisely a pseudomonoid in $K$.
• Of course, a model in $K$ of the theory of a monad, or an adjunction, is precisely a monad or adjunction in $K$.
• If $T$ is a 1-categorical theory, then a model of $T$ (regarded as a 2-categorical theory) in $K$ is precisely a model of the original theory $T$ in the category of discrete objects in $K$.
• Similarly, if $T$ is a propositional theory, then a model of $T$ in $K$ lives in the poset of subterminal objects.

The internal theory of a 2-category

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

• the basic 1-types are all the objects of $K$, with interpretation the identity.
• the basic 0-types are all the discrete objects of $K$, with interpretation the identity.
• the basic dependent propositions in a context $\Gamma$, are all the subobjects of $[\Gamma]$ in $K$.
• the basic terms of a type $A$ in context $\Gamma$ are all the sections in $K$ of the morphism $[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 $K$ has (regular, coherent, etc.) can be reflected in its internal logic.