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}$.
-
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}$.)
-
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})$.
Best Answer
$\newcommand{\type}{\ \mathsf{type}}$ $\newcommand{\Idt}{\mathsf{Id}}$ $\newcommand{\refl}{\mathsf{refl}}$ $\newcommand{\J}{\mathsf{J}}$
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...
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.
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$.
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)$$
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.