A Coherence Construction for the Propositional Universe
<|reference_start|>A Coherence Construction for the Propositional Universe: 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.<|reference_end|>
@article{huang2024a,
    title={A Coherence Construction for the Propositional Universe},
    author={Xu Huang},
    journal={arXiv preprint arXiv:2405.13435},
    year={2024},
    archivePrefix={arXiv},
    eprint={2405.13435},
    primaryClass={cs.LO}
}