A Coherence Construction for the Propositional Universe
Logic in Computer Science
2024-05-24 v1
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.
Keywords
Cite
@article{arxiv.2405.13435,
title = {A Coherence Construction for the Propositional Universe},
author = {Xu Huang},
journal= {arXiv preprint arXiv:2405.13435},
year = {2024}
}
Comments
5 pages