A Coherence Construction for the Propositional Universe
arXiv:2405.13435
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.
arXiv comment5 pages