On the Inadequacy of the Projective Structure with Respect to the Univalence Axiom
arXiv:1712.02652
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öf 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.
15 pages