# Interpreting intensional identity types and Tarskian universe in the syntactic/classifying category of a dependent type theory

Let $$\mathbb{T}$$ denote an intensional Martin-Löf type theory with all the type usual constructors. Further, assume that it has a universe $$U$$ a la Tarski (defined by nLab here).

Recall the syntactic category $$C(\mathbb{T})$$, with objects being the well-formed contexts in $$\mathbb{T}$$ and morphisms being so-called context morphisms, i.e., equivalence classes of sequences of terms $$[(f_1, \ldots, f_m)]$$ such that

$$\begin{array}{c}{x_{1} : A_{1}, \ldots, x_{n} : A_{n} \vdash f_{1} : B_{1}} \\ {\vdots} \\ {x_{1} : A_{1}, \ldots, x_{n} : A_{n} \vdash f_{m} : B_{m}\left(f_{1}, \ldots, f_{m-1}\right)}\end{array}$$

are derivable in $$\mathbb{T}$$ where $$[f_i]=[g_i]$$ when $$x_{1} : A_{1}, \ldots, x_{n} : A_{n} \vdash f_{i} \equiv g_{i} : B_{i}\left(f_{1}, \ldots f_{i-1}\right)$$ is derivable for each $$1\leq i\leq m$$. Composition is given by substitution.

There are two ways in which I'm confused about how this category is supposed to model $$\mathbb{T}$$.

1. I have seen that extensional identity types may be interpreted as diagonal morphisms in $$C(\mathbb{T})$$. Does this work for intensional identity types as well? On the one hand, I have read that intensional identity types are instead supposed to be interpreted as path space objects, which seem to require a weak factorization system. On the other hand, Example 1.2.5 in the article The Simplicial Model of Univalent Foundations (after Voevodsky) (arxiv link) states that $$C(\mathbb{T})$$ carries an "evident" structure for identity types. What would this be? Perhaps it refers to a way of factorizing diagonal morphisms?

(Perhaps you need to regard $$C(\mathbb{T})$$ as an $$(\infty, 1)$$-category with path space objects representing intensional identity types in order to obtain an adjoint pair $$(Syn({-}), Lang({-}))$$. But I'm guessing that the authors of said article are just concerned with getting a sound interpretation of the syntax of $$\mathbb{T}$$.)

2. The same Example states that $$C(\mathbb{T})$$ carries an evident structure for $$U$$. I have read that a universe a la Russell should correspond to an object classifier in $$C(\mathbb{T})$$. Is this the case for a universe a la Tarski as well? If so, what exactly does this look like in $$C(\mathbb{T})$$?

Any clarification on these issues would be greatly appreciated. In particular, I am looking for concrete descriptions of these logical structures within $$C(\mathbb{T})$$.


The paper you linked gives a specification of the structure for identity types in appendix B (at least). It's not as simple as diagonal morphisms; rather, it involves constructions corresponding to the ones in type theory, more or less, which is why the syntactic category has all this 'evident' structure. You just use the type/term constructions corresponding to all the things they are trying to mimic in the contextual category.

For universes, the idea of the object classifier is that you have an object $$U$$ of codes and an object $$\hat{U}$$ which is like a universal type whose values are all the values of all the types coded by the universe. There is a map $$\hat{U} → U$$ saying which (coded) type each value in the universal type comes from. The required pullback squares mean that some families of sets can be represented by maps into $$U$$. However, this works equally well with universes a la Tarski, because the way you'd write $$\hat{U}$$ in type theory is $$Σ_{u:U} T\ u$$ (assuming $$T$$ is the decoding family). The map $$\hat{U} → U$$ is just the first projection.

For universes a la Russell, the only difference is that we say that some types are the values of $$U$$, rather than being coded by the values of $$U$$. So in that situation $$\hat{U}$$ is written $$Σ_{X:U} X$$, but I don't think much else changes.

I would think that the difficulty with the universe is showing that the individual structures ($$Π$$, $$Σ$$, etc.) on the universe cover everything that is supposed to be classified. Then the 'evident' structure is just using all the type theoretic constructions and maybe hand waving a bit.

Edit: I guess I'm not sure which part you want. Is it this?

An Id-type structure consists of...

1. For each $$(Γ,A)$$ an object $$(Γ,A,p^*_AA,Id_A)$$. This is given by the rule $$\frac{Γ ⊢ A \type}{Γ, x:A, y:A ⊢ \Idt_A(x,y) \type}$$ ensuring that the corresponding contexts are well-formed.

2. For each $$(Γ,A)$$ a morphism $$\refl_A : (Γ,A) → (Γ, A, p^*_AA,\Idt_A)$$ .... This is given by the multi-term (syntax just made up, hopefully it's clear): $$Γ,x:A ⊢ Γ,x,x,\refl_A(x)$$ which is justified by the Id-intro rule. The equation on $$\refl_A$$ corresponds to the two uses of $$x$$.

3. For each $$(Γ,A,p^*_AA,\Idt_A,C)$$ and $$d : (Γ,A) → (Γ,A,p^*_AA,\Idt_A,C)$$ with $$p_C\cdot d = \refl_A$$ a section $$\J_{C,d} : (Γ,A,p^*_AA,\Idt_A) → (Γ, A, p^*_AA,\Idt_A,C)$$ .... The section is given by the multi-term: $$Γ,x:A, y:A, u:\Idt_A(x,y) ⊢ Γ, x, y, u, \J_{z,d}(x,y,u)$$ The condition on $$d$$ corresponds to the premise $$Γ, z:A ⊢ d(z) : C(z,z,\refl_A(z))$$ The (unmentioned) equation on $$\J$$ corresponds to the computation rule $$\J_{z,d}(x,x,\refl_A(x)) = d(x)$$

4. Some rules that correspond to being able to substitute inside $$\Idt$$, $$\refl$$ and $$\J$$.

The universe is similar, but there are many more cases, and instead of an eliminator term like $$\J$$ there is a type family $$\mathsf{El}$$ that computes. But every one of the rules of contextual category structure seems designed to correspond to some structure of the type theory.

• Thank you, but I am looking for an explicit, concrete description of identity types and of $U$ within $C(\mathbb{T})$. It seems that you are just explaining Appendix B. – CuriousKid7 Aug 26 '19 at 22:40
• What exactly are we choosing $(\Gamma, A, p^{\ast}_A{A}, Id_A)$ to be in the syntactic category? You said that intensional identity types are not just diagonal morphisms. So how are they interpreted in the syntactic category? – CuriousKid7 Aug 27 '19 at 2:33
• It is the well formed context $Γ, x:A, y:A, u:\mathsf{Id}_A(x,y)$. The rule I mentioned ensures it is well-formed. Intensional type theory's syntax has the type $\mathsf{Id}_A(x,y)$ as well as terms $\mathsf{refl}_A(x)$ and $\mathsf{J}_{z,d}(x,y,u)$, along with equational rules for them. This is in appendix A. I think every rule in appendix B has a corresponding syntactic rule in appendix A, except for the 'stability' rules which correspond to syntactic substitution. – Dan Doel Aug 27 '19 at 2:54
• To make sure, do we choose the universe to be the context $[x: U, y: El(x)]$? – CuriousKid7 Aug 28 '19 at 5:55
• Yes, that's the object part of their specification of universe structure. From the object classifier perspective, that is $\hat{U}$, and $U$ is $[x:U] = \mathsf{ft}[x : U, y : \mathsf{El}(x)]$, and the map from $\hat{U}$ to $U$ is $p_{\mathsf{El}}$, I believe. – Dan Doel Aug 28 '19 at 12:01