Annals of Pure and Applied Logic 171 (6):102793 (2020)

Benno Van Den Berg
University of Amsterdam
We show that Martin Hyland's effective topos can be exhibited as the homotopy category of a path category EFF. Path categories are categories of fibrant objects in the sense of Brown satisfying two additional properties and as such provide a context in which one can interpret many notions from homotopy theory and Homotopy Type Theory. Within the path category EFF one can identify a class of discrete fibrations which is closed under push forward along arbitrary fibrations (in other words, this class is polymorphic or closed under impredicative quantification) and satisfies propositional resizing. This class does not have a univalent representation, but if one restricts to those discrete fibrations whose fibres are propositions in the sense of Homotopy Type Theory, then it does. This means that, modulo the usual coherence problems, it can be seen as a model of the Calculus of Constructions with a univalent type of propositions. We will also build a more complicated path category in which the class of discrete fibrations whose fibres are sets in the sense of Homotopy Type Theory has a univalent representation, which means that this will be a model of the Calculus of Constructions with a univalent type of sets.
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1016/j.apal.2020.102793
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Translate to english
Revision history

Download options

Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 50,018
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

No references found.

Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

Univalent Foundations and the UniMath Library.Anthony Bordg - 2019 - In Deniz Sarikaya, Deborah Kant & Stefania Centrone (eds.), Reflections on the Foundations of Mathematics. Springer Verlag.
Spirallike Mappings and Univalent Subordination Chains in Cn.Ian Graham, Hidetaka Hamada, Gabriela Kohr & Mirela Kohr - 2008 - Annali della Scuola Normale Superiore di Pisa 7 (4):717-740.
Plurivalent Logics.Graham Priest - 2014 - Australasian Journal of Logic 11 (1).


Added to PP index

Total views
9 ( #847,326 of 2,324,077 )

Recent downloads (6 months)
9 ( #77,921 of 2,324,077 )

How can I increase my downloads?


My notes