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:

- 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)$;
- for each such $\left(\Gamma, A\right)$, a section $\mathsf{refl}_A$ of the composite $p_{p^{\ast}{A}} \circ p_{\mathsf{Id_A}}$.
- 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:

- 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}}$;
- 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?

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