Univalent polymorphism (Q1987219): Difference between revisions

The \textit{calculus of construction} (CoC), an impredicative type theory lying at the top of Barendregt's lambda cube, is the basis of proof assistants such as Coq and Lean. This paper considers questions whether it is possible to have universes which are both impredicative and univalent, how the type Prop of propositions in CoC relates to the notion of proposition in \textit{Homotopy Type Theory} (HoTT) [The Univalent Foundations Program, Homotopy type theory. Univalent foundations of mathematics. Princeton, NJ: Institute for Advanced Study; Raleigh, NC: Lulu Press (2013; Zbl 1298.03002)] and whether one can obtain models of Voevodsky's resizing axioms. In order to model CoC, one needs a category endowed with two classes of maps, namely, \textit{small fibrations} and \textit{fibrations}, both of which are pullback stable, closed under composition and contain all isomorphisms. One needs a particular small fibration, called a \textit{representation}, such that any small fibration is to be obtained as a pullback of a representation. Besides, one should be able to push fibrations along other fibrations, and it should be the case that small fibrations are closed under being pushed forward along arbitrary fibrations, which is no other than impredicativity in this context. We have an old idea [\textit{J. M. E. Hyland} et al., Proc. Lond. Math. Soc., III. Ser. 60, No. 1, 1--36 (1990; Zbl 0703.18002)] that models of CoC are to be obtained by looking at Hyland's effective topos [\textit{J. M. E. Hyland}, Stud. Logic Found. Math. 110, 165--216 (1982; Zbl 0522.03055)], in which every map is fibration and the small fibrations are discrete maps. This idea does not quite work due to a certain ambiguity in the very notion of a discrete map, but the \textit{standard} model of CoC is to be obtained by being resricted to $\rceil\rceil$-separated objects. This paper gives an alternative solution. The author shows that Martin Hyland's effective topos is to be exhibited as the homotopy category of a path category $\mathbb{EFF}$. The notion of a path category was introduced in [\textit{B. van den Berg} and \textit{I. Moerdijk}, J. Pure Appl. Algebra 222, No. 10, 3137--3181 (2018; Zbl 1420.18034)], providing an abstract framework for doing homotopy theory. Different from Quillen's model categories, path categories are provided with two classes of maps, namely, fibrations and equivalences. From a standpoint of type theory, path categories provide models of \textit{propositional identity types}. One can see that in $\mathbb{EFF}$ we can define a notion of discrete fibration which is stable under push forward along arbitrary fibrations. It turns out that with the class of propositional discrete fibrations as the small fibrations, $\mathbb{EFF}$ is a model of CoC with a univalent Prop. It is interesting to note that $\mathbb{EFF}$ is a model of propositional resizing. One reason why the model in $\mathbb{EFF}$ is somewhat poor is that its universe contains only propositions and excludes many interesting data types such as $\mathbb{N}\rightarrow\mathbb{N}$. With due regard to this, the author constructs a more complicated path category $\mathbb{EFF}_{1}$ in which the class of fibrations of discrete sets is an impredicative of small fibrations with a univalent representation. The natural next step would be the construction of a path category $\mathbb{EFF}_{2}$ in which the class of discrete fibrations of groupoids would be closed under push forward along arbitrary fibrations and would have a univalent representation. Continuing and taking the limit, one would get a path category $\mathbb{EFF}_{\infty}$ in which the class of discrete fibrations would be closed under push forward along arbitrary fibrations and would have a univalent representation. Two significant disclaimers are left open for future study. Firstly, the usual coherence problems related to substitution are ignored. Secondly, many definitional equalities have been replaced by propositional ones. The author intends to discuss these matters in subsequent papers.