# Categorical semantics of the identity type

In Appendix B of the article Simplicial Model of Univ. Foundations, Definition B.1.3 specifies the structure for identity types in a contextual category $$\mathcal{C}$$ (which in particular is equipped with a grading $$\coprod_nOb_n{\mathcal{C}}$$ of its objects and a choice of projection morphism $$p_X$$ for each $$X\in Ob_{n+1}{\mathcal{C}}$$), in part as follows:

1. for any $$\left(\Gamma, A\right)\in Ob_{n+1}{\mathcal{C}}$$ and sections $$a$$ and $$b$$ of $$p_A$$, an object $$\left(\Gamma, A, p_A^{\ast}{A}, \mathsf{Id}_A\right)$$;
2. for each such $$\left(\Gamma, A\right)$$, a section $$\mathsf{refl}_A$$ of the composite $$p_{p^{\ast}{A}} \circ p_{\mathsf{Id_A}}$$.
3. for each $$\left(\Gamma, A, p_A^{\ast}{A}, \mathsf{Id}_A, B\right)\in Ob_{n+4}{\mathcal{C}}$$ and map $$d: \left(\Gamma, A\right) \to \left(\Gamma, A, p_A^{\ast}{A}, \mathsf{Id}_A, B\right)$$ satisfying $$p_B \circ d = \mathsf{refl}_A$$, a section $$\mathsf{J}_{B,d}$$ of $$p_B$$ such that $$\mathsf{J}_{B,d} \circ \mathsf{refl}_A =d$$.

(Here, notation such as $$(\Gamma, A)$$ refers to any object $$Y$$ in $$\mathcal{C}$$ such that $$\text{ft}(Y) = \Gamma$$, and notation such as $$p_A$$ refers to the projection map $$(\Gamma, A)\to \Gamma$$.)

In particular, Part (2) of the definition interprets the canonical reflexivity term as a section $$\mathsf{refl}_A$$ of the composition of two projection maps, namely $$p_{p^{\ast}{A}} \circ p_{\mathsf{Id_A}}$$.

I understand how the authors obtain this interpretation directly from the corresponding syntactic rule in Appendix A. However, $$\mathsf{refl}_A$$ is technically not a section of a projection map (nor does it seem to induce one). Therefore, it interacts "poorly" with the semantics of, for example, $$\lambda$$ expressions given in part (2) of Definition B.1.1, which specifies the structure for dependent products. In particular:

1. for each $$\left(\Gamma, A, B\right) \in Ob_{n+2}{\mathcal{C}}$$, an object $$\left(\Gamma, \Pi(A, B)\right)\in Ob_{n+1}{\mathcal{C}}$$;
2. for each such $$\left(\Gamma, A, B\right)$$ and each section $$b$$ of $$p_B$$, a section $$\lambda(b)$$ of $$p_{\Pi(A, B)}$$.

Here, we can only form $$\lambda$$ maps in $$\mathcal{C}$$ given genuine sections of projections.

Overall, I've been under the impression that judgements expressing typing declarations must be interpreted as sections of projections.

Am I right to have this concern? If so, how do the authors resolve it? If not, what am I missing?

• Welcome to MO. While you do refer to the original paper (which is great) many of the definitions and notations you use are not self contained in this post. Can you please edit it so as it is readable to someone who will not open the links? Nov 10 '19 at 21:42
• @AmirSagiv I've made it much more readable, I believe. Nov 11 '19 at 1:06
• I don't fully understand, is your concern that refl is interpreted as a section of a composite of projections rather than a section of a single projection? That doesn't seem right, it seems to me it should be a section of the pullback of $p_{\tt Id}$ along the diagonal. Nov 11 '19 at 17:04
• @MikeShulman Yes, that is my concern. It seems that we need to interpret the term introduction rule for $\tt{Id}$ as a section of a display map, not a composite of the them. When you say that doesn't seem right, are you referring to this concern of mine or the interpretation of $\tt{refl}$ given in the paper? It seems that you are referring to the latter since you are proposing a different interpretation. Nov 11 '19 at 19:10
• It looks to me like the interpretation given in the paper (B.1.3(2)) is correct, but your description of it is incorrect. refl is a morphism from $(\Gamma,A)$ to $(\Gamma,A,p_A^*A,{\rm Id}_A)$, but it is not stated to be a section of the composite projection $(\Gamma,A,p_A^*A,{\rm Id}_A) \to (\Gamma,A)$; rather its composite with the single projection $p_{\rm Id} : (\Gamma,A,p_A^*A,{\rm Id}_A) \to (\Gamma,A,p_A^*A)$ is the diagonal $(\Gamma,A) \to (\Gamma,A,p_A^*A)$. This is another way of saying that it is a section of the pullback of $p_{\rm Id}$ along the diagonal, as I said. Nov 12 '19 at 3:14