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


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

  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.

| cite | improve this answer | |
  • $\begingroup$ 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. $\endgroup$ – CuriousKid7 Aug 26 '19 at 22:40
  • $\begingroup$ 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? $\endgroup$ – CuriousKid7 Aug 27 '19 at 2:33
  • $\begingroup$ 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. $\endgroup$ – Dan Doel Aug 27 '19 at 2:54
  • $\begingroup$ To make sure, do we choose the universe to be the context $[x: U, y: El(x)]$? $\endgroup$ – CuriousKid7 Aug 28 '19 at 5:55
  • $\begingroup$ 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. $\endgroup$ – Dan Doel Aug 28 '19 at 12:01

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.