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

TL;DR

This paper constructs a type-theoretic model using functor categories and projective fibrations, revealing that the natural universe in this setting is not univalent, thus highlighting limitations in certain models of type theory.

Contribution

It introduces a new model of Martin-Löf type theory based on functor categories with projective fibrations and demonstrates the universe's non-univalence in this context.

Findings

The universe in the model is not univalent.

The model supports dependent sums, products, and identity types.

It provides insights into limitations of projective structures in modeling univalence.

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.