×

The \((\Pi,\lambda)\)-structures on the C-systems defined by universe categories. (English) Zbl 1383.03056

From the author’s introduction: The concept of a \(C\)-system in its present form was introduced in [the author, Contemp. Math. 658, 127–137 (2016; Zbl 1452.03040)]. The type of the \(C\)-systems is constructively equivalent to the type of contextual categories defined by J. Cartmell [Generalised algebraic theories and contextual categories. Oxford, UK: Oxford University (Ph.D. Thesis) (1978); Ann. Pure Appl. Logic 32, 209–243 (1986; Zbl 0634.18003)] but the definition of a \(C\)-system is slightly different from Cartmell’s foundational definition.
In this paper, which extends the series started with [the author, Theory Appl. Categ. 30, 1181–1214 (2015; Zbl 1436.03311); Theory Appl. Categ. 31, 1044–1094 (2016; Zbl 1380.03072); Theory Appl. Categ. 32, 53–112 (2017; Zbl 1453.03067)], we continue to consider what might be the most important structure on \(C\)-systems – the structure that corresponds, for the syntactic \(C\)-systems, to the operations of dependent product, \(\lambda\)-abstraction and application. The first \(C\)-system formulation of this structure was introduced by J. Cartmell in [1978, loc. cit.] as a part of what he called a strong M.L. structure. It was later studied by T. Streicher [Semantics of type theory. Correctness, completeness and independence results. Basel: Birkhäuser Verlag (1991; Zbl 0790.68068)] who called a \(C\)-system (contextual category) together with such a structure a “contextual category with products of families of types”. In [the author, 2016, loc. cit.] we introduced an alternative formulation of this structure that we called a \((\Pi, \lambda)\)-structure and constructed a bijection between the sets of Cartmell-Streicher structures and \((\Pi, \lambda)\)-structures on any \(C\)-system \(CC\). In this paper we consider the case of \(C\)-systems of the form \(CC(\mathcal{C}, p)\) introduced in [the author, 2015, loc. cit.]. They are defined, in a functorial way, by a category \(\mathcal{C}\) with a final object and a morphism \(p: \tilde{U} \rightarrow U\) together with the choice of pullbacks of \(p\) along all morphisms in \(\mathcal{C}\). A morphism with such choices is called a universe in \(\mathcal{C}\). As a corollary of general functoriality we obtain a construction of isomorphisms that connect the \(C\)-systems \(CC(\mathcal{C}, p)\) corresponding to different choices of pullbacks and different choices of final objects. It allows us to use the notation \(CC(\mathcal{C}, p)\) that only mentions \(\mathcal{C}\) and \(p\). In [the author, 2017, loc. cit.] a number of results about presheaves on universe categories and on the \(C\)-systems \(CC(\mathcal{C}, p)\) has been established. These results are of general nature and do not refer to the \((\Pi, \lambda)\)-structures. However, they are highly useful for the constructions such as the one presented in this paper. The main result of the paper – Construction 2.4, produces a \((\Pi, \lambda)\)-structure on \(CC(\mathcal{C}, p)\) from what we call a \((P, \tilde{P})\)-structure on \(p\) and what is, in essence, two morphisms in \(\mathcal{C}\) completing two other morphisms to a pullback. Its combination with the construction of [the author, Theory Appl. Categ. 31, 1044–1094 (2016; Zbl 1380.03072)], without the part that concerns the bijection, was originally stated in [the author, “The equivalence axiom and univalent models of type theory”, Preprint, arXiv:1402.5556] with a sketch of a proof given in the 2009 version of the author [“Notes on type systems”, Preprint, https://github.com/vladimirias/old\_notes\_on\_type\_systems]. It and the ideas that it is based on are among the most important ingredients of the construction of the univalent model of the Martin-Löf type theory in Kan simplicial sets. In view of Lemma 2.6, Construction 2.4 can be used not only to construct the \((\Pi, \lambda)\)-structures on \(C\)-systems, but also to prove that such structures do not exist. It is possible, that a similar technique may be used with other systems of inference rules of type theory, for example, to show that for a given universe \(p\) no model of a given kind of higher inductive types exists on \(CC(\mathcal{C}, p)\). In the following section we define homomorphisms of \(C\)-systems with \((\Pi, \lambda)\)-structures and functors of universe categories with \((P, \tilde{P})\)-structures and show, in Theorem 3.3, that our construction is functorial relative to these definitions. Theorem 3.3 is interesting also in that that its proof indirectly uses almost all results of [the author, 2016, loc. cit.]. On the other hand, modulo these results, the proof is very short and straightforward. The \((\Pi, \lambda)\)-structures correspond to the \((\Pi, \lambda, app, \beta, \eta)\)-system of inference rules. In [the author, 2016, loc. cit., Remark 4.4] we outline the definitions of classes of structures that correspond to the similar systems but without the \(\beta\)- or \(\eta\)-rules. Such structures appear as natural variations of the \((\Pi, \lambda)\)-structures. The results of the present paper admit straightforward modifications needed to construct and sometimes classify such partial \((\Pi, \lambda)\)-structures on \(C\)-systems of the form \(CC(\mathcal{C}, p)\). One may wonder how the construction of this paper relates to the earlier ideas of R. A. G. Seely [Math. Proc. Camb. Philos. Soc. 95, 33–48 (1984; Zbl 0539.03048)] and their refinement by P. Clairambault and P. Dybjer [Math. Struct. Comput. Sci. 24, No. 6, Article ID e240606, 54 p. (2014; Zbl 1342.03046)]. This question requires further study.
The methods of this paper are fully constructive and, in fact, almost entirely essentially algebraic. The paper is written in the same formalization-ready style as the previous ones. The main intended base for its formalization is Zermelo-Fraenkel theory. However, it can also be formalized in the existing formal systems for the univalent foundations such as the UniMath.
The author, in contrary to popular usage, uses diagrammatic order of writing compositions, i.e., given the morphisms \(f: X \rightarrow Y\) and \(g: Y \rightarrow Z\) the composite is denoted by \(f\circ g\), instead of the usual \(g\circ f\).

MSC:

03F50 Metamathematics of constructive systems
18C50 Categorical semantics of formal languages
03B15 Higher-order logic; type theory (MSC2010)
18D15 Closed categories (closed monoidal and Cartesian closed categories, etc.)

Software:

GitHub; UniMath
PDFBibTeX XMLCite
Full Text: arXiv EMIS

References:

[1] John Cartmell.Generalised algebraic theories and contextual categories.Ph.D. Thesis, Oxford University, 1978.http://www.cs.ru.nl/ spitters/Cartmell.pdf. · Zbl 0634.18003
[2] John Cartmell. Generalised algebraic theories and contextual categories. Ann. Pure Appl. Logic, 32(3):209-243, 1986. · Zbl 0634.18003
[3] Pierre Clairambault and Peter Dybjer.The biequivalence of locally cartesian closed categories and Martin-L¨of type theories.Math. Structures Comput. Sci., 24(6):e240606, 54, 2014. · Zbl 1342.03046
[4] R. A. G. Seely. Locally Cartesian closed categories and type theory. Math. Proc. Cambridge Philos. Soc., 95(1):33-48, 1984. · Zbl 0539.03048
[5] Thomas Streicher.Semantics of type theory.Progress in Theoretical Computer Science. Birkh¨auser Boston Inc., Boston, MA, 1991. Correctness, completeness and independence results, With a foreword by Martin Wirsing. · Zbl 0790.68068
[6] Vladimir Voevodsky. Notes on type systems. 2009-2012.https://github.com/ vladimirias/old_notes_on_type_systems.
[7] Vladimir Voevodsky. The equivalence axiom and univalent models of type theory. arXiv 1402.5556, pages 1-11, 2010.http://arxiv.org/abs/1402.5556.
[8] Vladimir Voevodsky. A C-system defined by a universe category. Theory Appl. Categ., 30(37):1181-1215, 2015.http://www.tac.mta.ca/tac/volumes/30/37/30-37.pdf. · Zbl 1436.03311
[9] Vladimir Voevodsky.Products of families of types and (Π, λ)-structures on C systems. Theory Appl. Categ., 31(36):1044-1094, 2016.http://www.tac.mta.ca/ tac/volumes/31/36/31-36.pdf. · Zbl 1380.03072
[10] Vladimir Voevodsky. Subsystems and regular quotients of C-systems. In Conference on Mathematics and its Applications, (Kuwait City, 2014), number 658 in Contem porary Mathematics, pages 127-137, 2016. · Zbl 1452.03040
[11] Vladimir Voevodsky. C-systems defined by universe categories: presheaves. Theory Appl. Categ., 32(3):53 - 112, 2017.http://www.tac.mta. · Zbl 1453.03067
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.