A Coherence Construction for the Propositional Universe

TL;DR

Problem: interpret a Coquand-style universe of propositions $Prop$ as the subobject classifier $\Omega$ in a category with families. Approach: build a coherence construction on top of Lumsdaine's local universes to realize $Prop$ by quotienting the presheaf of types $\mathrm{Tp}$ so that judgementally isomorphic types are equal, yielding $Prop \cong \tilde{U}$. Key contribution: shows how to derive a quotient presheaf $\overline{\mathrm{Tp}}$ and $\overline{\mathrm{Tm}}$ that realize $El$ and the encoding, achieving $Prop \cong \tilde{U}$ and enabling propositional extensionality in the model. Significance: offers a coherent, implementation-friendly path to embed a Coquand-style $Prop$ in topos-like settings, distinct from more complex homotopical rigidity constructions and suitable for simpler use cases.

Abstract

We record a particularly simple construction on top of Lumsdaine's local universes that allows for a Coquand-style universe of propositions with propositional extensionality to be interpreted in a category with subobject classifiers.