We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

math.CT
< prev | next >
new | recent | 1712

Change to browse by:

math
math.AT
math.LO

References & Citations

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo

Mathematics > Category Theory

Title: On the Inadequacy of the Projective Structure with Respect to the Univalence Axiom

Authors: Anthony Bordg
(Submitted on 6 Dec 2017 (v1), last revised 8 Sep 2020 (this version, v3))
Abstract: In this article the author endows the functor category [B(C2),Gpd] with the structure of a type-theoretic fibration category with a universe using the projective fibrations. It offers a new model of Martin-L\"of type theory with dependent sums, dependent products, identity types and a universe. It turns out that this universe, the natural candidate that lifts the univalent universe of small discrete groupoids in the groupoid model of Hofmann and Streicher, is not univalent.
Comments: 15 pages
Subjects: Category Theory (math.CT); Algebraic Topology (math.AT); Logic (math.LO)
MSC classes: 55P
Cite as: arXiv:1712.02652 [math.CT]
  (or arXiv:1712.02652v3 [math.CT] for this version)

Submission history

From: Anthony Bordg [view email]
[v1] Wed, 6 Dec 2017 18:40:48 GMT (29kb)
[v2] Tue, 12 Dec 2017 14:31:05 GMT (29kb)
[v3] Tue, 8 Sep 2020 10:21:14 GMT (24kb)
Which authors of this paper are endorsers? | Disable MathJax (What is MathJax?)

Link back to: arXiv, form interface, contact.