Publication Type:
Journal ArticleSource:
Theory and Applications of Categories, Volume 32, Issue 3, p.53-112 (2017)URL:
http://www.tac.mta.ca/tac/volumes/32/3/32-03abs.htmlAbstract:
<p>This paper was written to present the constructions that were originally introduced for the proof of functoriality of $(\Pi,\lambda)$ structures obtained from the $(P,\tilde{P})$ structures. In the process of writing up this proof it became clear that the main objects required for it -- the "almost representations" $\mu_n$ and $\tilde{\mu}_n$ of the presheaves $Ob_n$ and $\tilde{Ob}_n$ on the C-systems defined by locally cartesian closed universe categories with binary product structures and the lemmas describing the behavior of these "almost representations" with respect to the universe category functors, play important role in the general theory that is quite independent from the analysis of the $\Pi,\lambda,\beta,\eta$ system of inference rules. This led to the decision to present these constructions together with the important intermediate ones such as $Sig$ and $D_p$ in a separate paper. Keywords: Type theory, Contextual category, Universe category</p>
