Michael Shulman
2-internal logic

Caveat

This logic is not by any means set in stone. What’s here is simply the most recent incarnation (or, more accurately, the most recent incarnation that I’ve managed to write up) of my evolving ideas about “the internal language of a 2-category.” Any suggestions for improvement, especially from people more familiar than I with ordinary logic and type theory, would be greatly appreciated.

Speak no evil

As adumbrated at categorified logic, the logic we use will be a logic of dependent types. We will have three different sorts of types, which we call 1-types (categories), 0-types (sets), and (-1)-types (propositions). 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.

In 1-categorical logic, it is often possible to avoid dependent types, but in 2-categorical logic they seem to play a more important role. For one thing, there seems no way to construct exponentials in a 2-category from “higher-order structure” the way that exponentials can be constructed from power objects in a 1-topos; thus we need to incorporate them into the type theory. Additionally, the use of dependent types allows us to restrict the language in categorically sensible ways.

A basic tenet of higher category theory is that if $A$ is an $n$-category and $x,y\in A$ then ${\mathrm{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 ${\mathrm{hom}}_A(x,y)$. For instance, if $n=1$, then ${\mathrm{hom}}_A(x,y)$ is a 0-type: the type of arrows from $x$ to $y$. And if $n=0$, then ${\mathrm{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=(\mathrm{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 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 equality 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. Later on we will construct “iso-types” ${\mathrm{iso}}_A(x,y)$ as subtypes of ${\mathrm{hom}}_A(x,y)$, which have some of the same properties as equality types.

We will allow ourselves to treat an $n$-type as an $m$-type for any $m\ge n$. When $n=-1$ this corresponds to replacing a proposition $\phi$ by the set $\{x:A\mid \phi \}$. When $n=0$ it corresponds to treating a set as a discrete category. Of course, when we do this we include as an axiom that the resulting $m$-type is truncated in an appropriate way: $\{x:A\mid \phi \}$ is a subobject of $A$, and a discrete category is in fact discrete.

Judgements, contexts, and theories

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

• $\Gamma ⊢A:n\mathrm{Type}$ (type declarations)
• $\Gamma ⊢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$. We insist that the variables in $\Gamma$ occur in descending hierarchical order; thus we have first a list of 1-type variables, then a list of 0-type variables, and then a list of (-1)-type variables. If necessary we may separate the different parts of the context by vertical bars, so that $\Gamma =\Theta \mid \Delta \mid \Phi$.

To keep things looking familiar, we will write $\mathrm{Prop}$ instead of $(-1)\mathrm{Type}$. And since any two inhabitants of a (-1)-type are indistinguishable, we will generally write merely $\phi$ instead of $x:\phi$ when $\phi$ is a (-1)-type (a proposition). For the same reason, there can be no interesting dependence of a (-1)-type on another (-1)-type, so we omit (-1)-types from the declarations of other (-1)-types. Thus, written out in more detail, we actually have six different sorts of judgements:

$\Theta ⊢A:1\mathrm{Type}$	1-type declaration
$\Theta ⊢a:A$	1-term declaration
$\Theta \mid \Delta ⊢B:0\mathrm{Type}$	0-type declaration
$\Theta \mid \Delta ⊢b:B$	0-term declaration
$\Theta \mid \Delta ⊢\phi :\mathrm{Prop}$	(-1)-type declaration, aka proposition declaration
$\Theta \mid \Delta \mid \Phi ⊢\phi$	(-1)-term declaration, aka logical sequent

Note that in a logical sequent, $\Phi$ is a list of propositions; thus a logical sequent ends with something of the form ${\psi }_1,\dots ,{\psi }_n⊢\phi$ which of course has the usual meaning that ${\psi }_1,\dots ,{\psi }_n$ together imply $\phi$.

A final difference between our language and most common dependently typed languages is that we introduce variables with variances. In the standard categorical interpretation of a context such as $x:A,y:B(x)$, the type $B(x)$ that depends on a variable $x:A$ is interpreted by an object of a slice category $C/A$; the intuition being that for each $x:A$ the type $B(x)$ is the fiber over $x$ of the map $B\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 formally define a 1-context to be a finite list

$$x_1:A_1^{{ϵ}_1},\dots ,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 $k$, the judgement

   $$x_1:A_1^{{ϵ}_1},\dots ,x_{k-1}:A_{k-1}^{{ϵ}_{k-1}}⊢A_k:1\mathrm{Type}$$x_1:A_1^{\epsilon_1}, \dots, x_{k-1}:A_{k-1}^{\epsilon_{k-1}} \vdash A_k:1Type

   is derivable.

2. Each ${ϵ}_k$ is either $+$, $-$, or $0$.

3. If ${ϵ}_k=0$, then ${ϵ}_j=0$ for all $j>k$.

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

$$y_1:B_1,\dots ,y_n:B_n$$y_1:B_1, \dots, y_n:B_n

of variable declarations, such that for each $k$, the judgement

$$\Theta \mid y_1:B_1,\dots ,y_{k-1}:B_{k-1}⊢B_k:0\mathrm{Type}$$\Theta | y_1:B_1,\dots, y_{k-1}:B_{k-1} \vdash B_k:0Type

is derivable, and a (-1)-context to be a 0-context $\Theta \mid \Delta$ together with a finite list

$${\psi }_1,\dots ,{\psi }_n$$\psi_1,\dots, \psi_n

of propositions, such that for each $k$, the judgement

$$\Theta \mid \Delta ⊢{\psi }_k:\mathrm{Prop}$$\Theta | \Delta \vdash \psi_k :Prop

is derivable.

Note that any sort of context can be empty. The rules for forming judgements will ensure that free variables can only occur to the right of where in the context they are declared. Whenever we write a context it is assumed that there is no duplication of variables; this results in implicit hypotheses on the derivation rules.

The intended interpretation of these contexts is as follows. A context $x:A^{+}$ indicates that everything to its right takes place in the opfibrational slice $\mathrm{Opf}(A)$. Likewise, $x:A^{-}$ indicates that everything to its right takes place in $\mathrm{Fib}(A)$, while $x:A^0$ indicates that everything to its right takes place in the ordinary slice 2-category $K/X$. Recalling the theorems about iterated fibrations, a context such as $x:A^{+},y:B(x{)}^{+}$ indicates that we work in ${\mathrm{Opf}}_{\mathrm{Opf}(A)}(B\to A)=\mathrm{Opf}(B)$, while $x:A^{+},y:B^{-}$ indicates working in the two-sided fibrational slice $\mathrm{Fib}(A,B)$. Note that the variance label goes on the base of the fibration.

Once we are past the first $\mid$, 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:B$, where $B$ is a 0-type, means working in the slice 1-category of discrete objects over $B$. Similarly, once we pass the second $\mid$, 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^{+}\mid y:B$$x:A^+ | y:B

means working in $\mathrm{disc}(\mathrm{Opf}(A))/B$.

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

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

Rules for making judgements

As is usual in type theories, we write

$$\frac{AB}{C}$$\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.

We will write $x:A^{+?}$ or $x:A^{-?}$ in a context appearing in the conclusion of a rule to mean that if the context to the left of this variable is fibrational, then we may have $x:A^{+}$ or $x:A^{-}$, respectively, but otherwise we have merely $x:A$.

(The rules that follow have not been updated to treat 1-types and 0-types separately.)

Structural rules

$$\frac{\Gamma ⊢A:\mathrm{Type}}{\Gamma ,x:A^{ϵ}⊢x:A}(\mathrm{projection})$$\frac{\Gamma\vdash A:Type}{\Gamma, x:A^\epsilon \vdash x:A} (projection)

$$\frac{\Gamma ⊢a:A\Gamma ,x:A,\Delta ⊢J}{\Gamma ,\Delta [a/x]⊢J[a/x]}(\mathrm{substitution})$$\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 ⊢J}{\Gamma ,x:A^{ϵ},\Delta [x/y]⊢J[x/y]}(\mathrm{contraction})$$\frac{\Gamma, x:A^\epsilon, y:A^\epsilon, \Delta \vdash J}{\Gamma,x:A^\epsilon, \Delta[x/y] \vdash J[x/y]} (contraction)

In the contraction rule, note that the two $ϵ$s in $x:A^{ϵ},y:A^{ϵ}$ must be the same.

$$\frac{\Gamma ⊢A:\mathrm{Type}\Gamma ⊢J}{\Gamma ,x:A^{ϵ}⊢J}(\mathrm{weakening})$$\frac{\Gamma \vdash A:Type \qquad \Gamma\vdash J}{\Gamma, x:A^\epsilon \vdash J} (weakening)

$$\frac{\Gamma ,x:A^{{ϵ}_1},y:B^{{ϵ}_2},\Delta ⊢J}{\Gamma ,y:B^{{ϵ}_2},x:A^{{ϵ}_1},\Delta ⊢J}(\mathrm{exchange})$$\frac{\Gamma, x:A^{\epsilon_1}, y:B^{\epsilon_2}, \Delta \vdash J}{\Gamma, y:B^{\epsilon_2}, x:A^{\epsilon_1}, \Delta \vdash J} (exchange)

The exchange rule has the extra restriction that $x$ cannot occur freely in the type $B$. Finally we have:

$$\frac{\Gamma ,\Delta ⊢J}{\Gamma ,{\Delta }^0⊢J}(\mathrm{neglect})$$\frac{\Gamma,\Delta\vdash J}{\Gamma, \Delta^0\vdash J} (neglect)

Arrow types

$$\frac{\Gamma ⊢A:\mathrm{Type}}{\Gamma ,x:A^{-?},y:A^{+?}⊢{\mathrm{hom}}_A(x,y):\mathrm{Type}}(\mathrm{arrow}\mathrm{type})$$\frac{\Gamma \vdash A:Type}{\Gamma, x:A^{-?}, y:A^{+?} \vdash hom_A(x,y):Type} (arrow type)

$$\frac{\Gamma ⊢A:\mathrm{Type}}{\Gamma ,x:A⊢1_x:{\mathrm{hom}}_A(x,x)}(\mathrm{identities})$$\frac{\Gamma \vdash A:Type}{\Gamma, x:A\vdash 1_x:hom_A(x,x)} (identities)

Note that $x$ cannot be fibrational in the context ${\mathrm{hom}}_A(x,x)$.

$$\frac{\Gamma ⊢A:\mathrm{Type}}{\Gamma ,x:A^{-?},z:A^{+?},y:A,f:{\mathrm{hom}}_A(x,y),g:{\mathrm{hom}}_A(y,z)⊢g\circ f:{\mathrm{hom}}_A(x,z)}(\mathrm{composition})$$\frac{\Gamma \vdash A:Type}{\Gamma, x:A^{-?}, z:A^{+?}, y:A, f:hom_A(x,y), g:hom_A(y,z)\vdash g\circ f :hom_A(x,z)} (composition)

Likewise, note that $y$ cannot be fibrational if we want to compose along it, although $x$ and $z$ can be.

$$\frac{\Gamma ⊢B:\mathrm{Type}\Gamma ,x:A⊢b:B}{\Gamma ,y:A^{-?},z:A^{+?},f:{\mathrm{hom}}_A(y,z)⊢b(f/x):{\mathrm{hom}}_B(b[y/x],b[z/x])}(\mathrm{functoriality})$$\frac{\Gamma \vdash B:Type \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)

Functoriality is probably the most subtle of the rules for arrow types. The idea is that a term declaration of the form $\Gamma ⊢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.

By the way, 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$ with free variable $x:A$ into a term $b(f/x)$ with free variable $f:{\mathrm{hom}}_A(y,z)$. In particular $f$ is free in $b(f/x)$ while $x$ is no longer free.

Equality

$$\frac{\Gamma ⊢A:\mathrm{Type}}{\Gamma ,x:A^{-?},y:A^{+?},f:{\mathrm{hom}}_A(x,y),g:{\mathrm{hom}}_A(x,y)⊢(f=g):\mathrm{Prop}}$$\frac{\Gamma \vdash A:Type}{\Gamma, x:A^{-?}, y:A^{+?}, f:hom_A(x,y), g:hom_A(x,y) \vdash (f=g):Prop}

There are the usual reflexivity, symmetry, transitivity, and substitution rules for equality. We also have associativity and unitality rules for composition:

$$\frac{\Gamma ⊢A:\mathrm{Type}}{\Gamma ,x:A^{-?},w:A^{+?},y:A,z:A,f:{\mathrm{hom}}_A(x,y),g:{\mathrm{hom}}_A(y,z),h:{\mathrm{hom}}_A(z,w)\mid \top ⊢(h\circ (g\circ f)=(h\circ g)\circ f)}$$\frac{\Gamma \vdash A:Type}{\Gamma, x:A^{-?}, w:A^{+?}, y:A, z:A, f: hom_A(x,y), g:hom_A(y,z), h:hom_A(z,w) | \top \vdash (h \circ (g\circ f) = (h\circ g)\circ f)}

$$\frac{\Gamma ⊢A:\mathrm{Type}}{\Gamma ,y:A^{+?},x:A,f:{\mathrm{hom}}_A(x,y)\mid \top ⊢((f\circ 1_x)=f)}(\text{right unit})$$\frac{\Gamma \vdash A:Type}{\Gamma, y:A^{+?}, x:A, f:hom_A(x,y) | \top \vdash ((f\circ 1_x) = f)}(\text{right unit})

$$\frac{\Gamma ⊢A:\mathrm{Type}}{\Gamma ,x:A^{-?},y:A,f:{\mathrm{hom}}_A(x,y)\mid \top ⊢((1_y\circ f)=f)}(\text{left unit})$$\frac{\Gamma \vdash A:Type}{\Gamma, x:A^{-?}, y:A, f:hom_A(x,y) | \top \vdash ((1_y\circ f) = f)}(\text{left unit})

And functoriality and naturality rules for arrow-types:

$$\frac{\Gamma ⊢B:\mathrm{Type}\Gamma ,x:A⊢b:B}{\Gamma ,y:A\mid \top ⊢(b(1_y/x)=1_{b[y/x]})}$$\frac{\Gamma \vdash B:Type \qquad \Gamma, x:A \vdash b:B}{\Gamma, y:A |\top\vdash (b(1_y/x) = 1_{b[y/x]})}

$$\frac{\Gamma ⊢B:\mathrm{Type}\Gamma ,x:A⊢b:B}{\Gamma ,y:A^{-?},w:A^{+?},z:A,f:{\mathrm{hom}}_A(y,z),g:{\mathrm{hom}}_A(z,w)\mid \top ⊢b(g/x)\circ b(f/x)=b(g\circ f/x)}$$\frac{\Gamma \vdash B:Type \qquad \Gamma, x:A \vdash b:B}{\Gamma, y:A^{-?}, w:A^{+?}, z:A, f:hom_A(y,z), g:hom_A(z,w) | \top\vdash b(g/x) \circ b(f/x) = b(g\circ f/x)}

$$\frac{\Gamma ,x:A⊢j:B(b_1,b_2)}{\Gamma ,y:A^{-?},z:A^{+?},f:{\mathrm{hom}}_A(y,z)\mid \top ⊢(j[z/x]\circ b_1(f/x)=b_2(g/x)\circ j[y/x])}(\mathrm{naturality})$$\frac{\Gamma, x:A \vdash j:B(b_1,b_2)}{\Gamma, y:A^{-?}, z:A^{+?}, f:hom_A(y,z) |\top\vdash (j[z/x] \circ b_1(f/x) = b_2(g/x) \circ j[y/x])}(naturality)

The idea of the naturality rule is that a term $\Gamma ,x:A⊢j:B(b_1,b_2)$ represents a 2-cell between the morphisms represented by $b_1$ and $b_2$, which should be a natural transformation in the internal logic.

We also assert that arrow-types are discrete, by saying that they are posetal and their order relation $\le$ is symmetric.

$$\frac{\Gamma ⊢A:\mathrm{Type}}{\Gamma ,x:A^{-?},y:A^{+?},f:{\mathrm{hom}}_A(x,y),g:{\mathrm{hom}}_A(x,y),h:{\mathrm{hom}}_{{\mathrm{hom}}_A(x,y)}(f,g),k:{\mathrm{hom}}_{{\mathrm{hom}}_A(x,y)}(f,g)\mid \top ⊢h=k}$$\frac{\Gamma \vdash A:Type}{\Gamma, x:A^{-?}, y:A^{+?}, f:hom_A(x,y), g:hom_A(x,y), h:hom_{hom_A(x,y)}(f,g), k:hom_{hom_A(x,y)}(f,g) | \top \vdash h=k}

$$\frac{\Gamma ⊢A:\mathrm{Type}}{\Gamma ,x:A^{-?},y:A^{+?},f:{\mathrm{hom}}_A(x,y),g:{\mathrm{hom}}_A(x,y),h:{\mathrm{hom}}_{{\mathrm{hom}}_A(x,y)}(f,g)⊢\mathrm{inv}(h):{\mathrm{hom}}_{{\mathrm{hom}}_A(x,y)}(g,f)}$$\frac{\Gamma \vdash A:Type}{\Gamma, x:A^{-?}, y:A^{+?}, f:hom_A(x,y), g:hom_A(x,y), h:hom_{hom_A(x,y)}(f,g) \vdash inv(h) :hom_{hom_A(x,y)}(g,f)}

Unit type

The rules for the unit type $1$ are fairly straightforward; they simply express that it is a 2-categorical terminal object.

$$\frac{}{⊢1:\mathrm{Type}}(\text{unit type})$$\frac{}{\vdash 1:Type} (\text{unit type})

$$\frac{}{⊢\star :1}(\text{unit term})$$\frac{}{\vdash \star:1} (\text{unit term})

$$\frac{}{x:1^{-},y:1^{+}⊢{\star }_{xy}:{\mathrm{hom}}_1(x,y)}(\text{unit arrow term})$$\frac{}{x:1^-,y:1^+ \vdash \star_{x y} : hom_1(x,y)} (\text{unit arrow term})

$$\frac{}{x:1^{-},y:1^{+},f:{\mathrm{hom}}_1(x,y),g:{\mathrm{hom}}_1(x,y)\mid \top ⊢(f=g)}(\text{the unit is discrete})$$\frac{}{x:1^-, y:1^+, f:hom_1(x,y), g:hom_1(x,y) | \top \vdash (f=g)} (\text{the unit is discrete})

Sum types

$$\frac{{\Gamma }^{\pm }⊢A:\mathrm{Type}{\Gamma }^{\pm },x:A^{-}⊢B:\mathrm{Type}}{{\Gamma }^{\pm }⊢{\Sigma }_{x:A^{-}}B:\mathrm{Type}}(\text{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.

$$\frac{{\Gamma }^{\pm }⊢A:\mathrm{Type}{\Gamma }^{\pm },x:A^{-}⊢B:\mathrm{Type}}{{\Gamma }^{\pm },x:{\Sigma }_{x:A^{-}}B⊢\mathrm{proj}(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 $\mathrm{proj}(x)$ is a term with free variable $x$, so it is automatically functorial and acts on arrows as well as elements.

$$\frac{{\Gamma }^{\pm }⊢A:\mathrm{Type}{\Gamma }^{\pm },x:A^{-}⊢B:\mathrm{Type}}{{\Gamma }^{\pm },x:A,y:A,f:{\mathrm{hom}}_A(y,x),u:B⊢f^{*}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]}

$$\frac{{\Gamma }^{\pm }⊢A:\mathrm{Type}{\Gamma }^{\pm },x:A^{-}⊢B:\mathrm{Type}}{{\Gamma }^{\pm },x:A,y:A,f:{\mathrm{hom}}_A(y,x),u:B⊢\mathrm{cart}(u):{\mathrm{hom}}_{{\Sigma }_{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:

$$\frac{{\Gamma }^{\pm }⊢A:\mathrm{Type}{\Gamma }^{\pm },x:A^{+}⊢B:\mathrm{Type}}{{\Gamma }^{\pm }⊢{\Sigma }_{x:A^{+}}B:\mathrm{Type}}(\text{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_{!}u$ and opcartesian arrows.

Subobject types

$$\frac{\Gamma ,x:A⊢\phi :\mathrm{Prop}}{{\Gamma }^0⊢\{x:A\mid \phi \}:\mathrm{Type}}$$\frac{\Gamma, x:A \vdash \varphi:Prop}{\Gamma^0 \vdash \{x:A | \varphi\}:Type}

Note that all fibrational context is lost when we pass to subobject types. Of course, this is because a subobject of a fibration need not be a fibration. The next set of rules say that $\phi$ is true of $x$ if and only if $x$ factors through $\{x:A\mid \phi \}$.

$$\frac{\Gamma ,x:A⊢\phi :\mathrm{Prop}\Gamma ⊢a:A\Gamma \mid \top ⊢\phi [a/x]}{{\Gamma }^0⊢i_{\phi }(a):\{x:A\mid \phi \}}$$\frac{\Gamma, x:A \vdash \varphi:Prop \qquad \Gamma \vdash a:A \qquad \Gamma | \top\vdash \varphi[a/x]}{\Gamma^0 \vdash i_\varphi(a): \{x:A | \varphi\}}

$$\frac{\Gamma ,x:A⊢\phi :\mathrm{Prop}}{{\Gamma }^0,y:\{x:A\mid \phi \}⊢o_{\phi }(y):A}$$\frac{\Gamma, x:A \vdash \varphi:Prop}{\Gamma^0, y: \{x:A | \varphi\} \vdash o_\varphi(y):A}

$$\frac{\Gamma ,x:A\mid \theta \wedge \phi ⊢\psi }{{\Gamma }^0,y:\{x:A\mid \phi \}\mid \theta [o(y)/x]⊢\psi [o(y)/x]}$$\frac{\Gamma, x:A | \theta \wedge \varphi \vdash \psi}{\Gamma^0, y: \{x:A | \varphi\}| \theta[o(y)/x] \vdash \psi[o(y)/x]}

$$\frac{{\Gamma }^0,y:\{x:A\mid \phi \}\mid \theta [o(y)/x]⊢\psi [o(y)/x]}{{\Gamma }^0,x:A\mid \theta \wedge \phi ⊢\psi }$$\frac{\Gamma^0, y: \{x:A | \varphi\}| \theta[o(y)/x] \vdash \psi[o(y)/x]}{\Gamma^0, x:A | \theta \wedge \varphi \vdash \psi}

We also have also rules expressing that $\{x:A\mid \phi \}$ is a full subobject of $A$.

$$\frac{\Gamma ,x:A⊢\phi :\mathrm{Prop}\Gamma ⊢a_1:A\Gamma ⊢a_2:A\Gamma \mid \top ⊢\phi [a_1/x]\Gamma \mid \top ⊢\phi [a_2/x]}{{\Gamma }^0,f:{\mathrm{hom}}_A(a_1,a_2)⊢i_{\phi }(f):{\mathrm{hom}}_{\{x:A\mid \phi \}}(i_{\phi }(a_1),i_{\phi }(a_2))}$$\frac{\Gamma, x:A \vdash \varphi:Prop \qquad \Gamma \vdash a_1:A \qquad \Gamma \vdash a_2:A \qquad \Gamma | \top\vdash \varphi[a_1/x]\qquad \Gamma | \top\vdash \varphi[a_2/x]} {\Gamma^0, f:hom_A(a_1,a_2) \vdash i_\varphi(f): hom_{\{x:A | \varphi\}}(i_\varphi(a_1),i_\varphi(a_2))}

$$\frac{\Gamma ,x:A⊢\phi :\mathrm{Prop}\Gamma ⊢a:A\Gamma \mid \top ⊢\phi [a/x]}{{\Gamma }^0⊢{\mathrm{iso}}_1:{\mathrm{hom}}_A(a,o_{\phi }(i_{\phi }(a))){\Gamma }^0⊢{\mathrm{iso}}_2:{\mathrm{hom}}_A(o_{\phi }(i_{\phi }(a)),a){\Gamma }^0\mid \top ⊢({\mathrm{iso}}_1\circ {\mathrm{iso}}_2=1_{o_{\phi }(i_{\phi }(a))}){\Gamma }^0\mid \top ⊢({\mathrm{iso}}_2\circ {\mathrm{iso}}_1=1_a)}$$\frac{\Gamma, x:A \vdash \varphi:Prop \qquad \Gamma \vdash a:A \qquad \Gamma | \top\vdash \varphi[a/x]}{\Gamma^0 \vdash iso_1:hom_A(a,o_\varphi(i_\varphi(a))) \qquad \Gamma^0 \vdash iso_2:hom_A(o_\varphi(i_\varphi(a)),a) \qquad \Gamma^0 | \top \vdash (iso_1 \circ iso_2 = 1_{o_\varphi(i_\varphi(a))})\qquad \Gamma^0 | \top \vdash (iso_2 \circ iso_1 = 1_a)}

$$\frac{\Gamma ,x:A⊢\phi :\mathrm{Prop}\Gamma ⊢a_1:A\Gamma ⊢a_2:A\Gamma \mid \top ⊢\phi [a_1/x]\Gamma \mid \top ⊢\phi [a_2/x]}{{\Gamma }^0,f:{\mathrm{hom}}_A(a_1,a_2)\mid \top ⊢o_{\phi }(i_{\phi }(f))\circ {\mathrm{iso}}_1={\mathrm{iso}}_1\circ f}$$\frac{\Gamma, x:A \vdash \varphi:Prop \qquad \Gamma \vdash a_1:A \qquad \Gamma \vdash a_2:A \qquad \Gamma | \top\vdash \varphi[a_1/x] \qquad \Gamma | \top\vdash \varphi[a_2/x]} {\Gamma^0, f:hom_A(a_1,a_2) | \top \vdash o_\varphi(i_\varphi(f)) \circ iso_1 = iso_1 \circ f}

$$\frac{\Gamma ,x:A⊢\phi :\mathrm{Prop}}{{\Gamma }^0,y:\{x:A\mid \phi \}⊢{\mathrm{iso}}_1:{\mathrm{hom}}_A(y,i_{\phi }(o_{\phi }(y))){\Gamma }^0,y:\{x:A\mid \phi \}⊢{\mathrm{iso}}_2:{\mathrm{hom}}_A(i_{\phi }(o_{\phi }(y)),y){\Gamma }^0,y:\{x:A\mid \phi \}\mid \top ⊢({\mathrm{iso}}_1\circ {\mathrm{iso}}_2=1_{i_{\phi }(o_{\phi }(y))}){\Gamma }^0,y:\{x:A\mid \phi \}\mid \top ⊢({\mathrm{iso}}_2\circ {\mathrm{iso}}_1=1_y)}$$\frac{\Gamma, x:A \vdash \varphi:Prop}{\Gamma^0, y: \{x:A | \varphi\} \vdash iso_1:hom_A(y,i_\varphi(o_\varphi(y))) \qquad \Gamma^0, y: \{x:A | \varphi\} \vdash iso_2:hom_A(i_\varphi(o_\varphi(y)),y) \qquad \Gamma^0, y: \{x:A | \varphi\} | \top \vdash (iso_1 \circ iso_2 = 1_{i_\varphi(o_\varphi(y))})\qquad \Gamma^0, y: \{x:A | \varphi\} | \top \vdash (iso_2 \circ iso_1 = 1_y)}

$$\frac{\Gamma ,x:A⊢\phi :\mathrm{Prop}}{{\Gamma }^0,y:\{x:A\mid \phi \},z:\{x:A\mid \phi \}f:{\mathrm{hom}}_{\{x:A\mid \phi \}}(y,z)\mid \top ⊢i_{\phi }(o_{\phi }(f))\circ {\mathrm{iso}}_1={\mathrm{iso}}_1\circ f}$$\frac{\Gamma, x:A \vdash \varphi:Prop}{\Gamma^0, y: \{x:A | \varphi\}, z: \{x:A | \varphi\} f:hom_{\{x:A | \varphi\}}(y,z) | \top \vdash i_\varphi(o_\varphi(f)) \circ iso_1 = iso_1 \circ f}

The naturality properties of ${\mathrm{iso}}_1$ and ${\mathrm{iso}}_2$ would come for free from the naturality rule, above, except that $i_{\phi }(y)$ is not an ordinary term (it is only defined if $y$ is a term $a$ such that $⊢\phi [a/x]$) so that that rule doesn’t apply.

Propositions

We have the usual introduction and elimination rules for the logical connectives. For example, for $\wedge$ we have

$$\frac{\Gamma ⊢\phi :\mathrm{Prop}\Gamma ⊢\psi :\mathrm{Prop}}{\Gamma ⊢(\phi \wedge \psi ):\mathrm{Prop}}$$\frac{\Gamma \vdash \varphi:Prop \qquad \Gamma \vdash \psi:Prop}{\Gamma \vdash (\varphi\wedge\psi):Prop}

$$\frac{\Gamma \mid \theta ⊢\phi \Gamma \mid \theta ⊢\psi }{\Gamma \mid \theta ⊢(\phi \wedge \psi )}$$\frac{\Gamma | \theta \vdash \varphi \qquad \Gamma | \theta \vdash \psi}{\Gamma | \theta \vdash (\varphi\wedge\psi)}

$$\frac{\Gamma \mid \theta ⊢(\phi \wedge \psi )}{\Gamma \mid \theta ⊢\phi }$$\frac{\Gamma | \theta \vdash (\varphi\wedge\psi)}{\Gamma | \theta \vdash \varphi}

$$\frac{\Gamma \mid \theta ⊢(\phi \wedge \psi )}{\Gamma \mid \theta ⊢\psi }$$\frac{\Gamma | \theta \vdash (\varphi\wedge\psi)}{\Gamma | \theta \vdash \psi}

The analogous rules for $\top ,\perp ,\wedge ,\vee ,\Rightarrow ,\neg$ are all standard. The following rules for quantifiers are also standard, bearing in mind that as usual, in a dependently typed logic, we can only introduce quantifiers over the last variable in the context.

$$\frac{\Gamma ,x:A⊢\phi :\mathrm{Prop}}{\Gamma ⊢(\forall x:A)\phi :\mathrm{Prop}}$$\frac{\Gamma, x:A \vdash \varphi:Prop}{\Gamma \vdash (\forall x:A)\varphi: Prop}

$$\frac{\Gamma ,x:A\mid \theta ⊢\phi }{\Gamma \mid \theta ⊢(\forall x:A)\phi }$$\frac{\Gamma, x:A | \theta \vdash \varphi}{\Gamma | \theta \vdash (\forall x:A)\varphi}

($x$ must not occur free in $\theta$ in the above rule)

$$\frac{\Gamma ⊢a:A\Gamma \mid \theta ⊢(\forall x:A)\phi }{\Gamma \mid \theta ⊢\phi [a/x]}$$\frac{\Gamma\vdash a:A \qquad \Gamma | \theta \vdash (\forall x:A) \varphi}{\Gamma | \theta \vdash \varphi[a/x]}

$$\frac{\Gamma ,x:A⊢\phi :\mathrm{Prop}}{\Gamma ⊢(\exists x:A)\phi :\mathrm{Prop}}$$\frac{\Gamma, x:A \vdash \varphi:Prop}{\Gamma \vdash (\exists x:A)\varphi: Prop}

$$\frac{\Gamma ⊢a:A\Gamma \mid \theta ⊢\phi [a/x]}{\Gamma \mid \theta ⊢(\exists x:A)\phi }$$\frac{\Gamma \vdash a:A \qquad \Gamma | \theta \vdash \varphi[a/x]}{\Gamma |\theta \vdash (\exists x:A) \varphi}

$$\frac{\Gamma \mid \theta ⊢(\exists x:A)\phi \Gamma ,x:A\mid \xi \wedge \phi ⊢\psi }{\Gamma \mid \theta \wedge \xi ⊢\psi }$$\frac{\Gamma | \theta \vdash (\exists x:A)\varphi \qquad \Gamma, x:A | \xi \wedge \varphi \vdash \psi}{\Gamma | \theta \wedge \xi \vdash \psi}

($x$ must not appear free in $\xi$ or $\psi$ in the above rule.)

Iteration types

Coproduct types

Quotient types

Interpretation in a 2-category