A Coherence Construction for the Propositional Universe
Xu Huang
TL;DR
This paper presents a straightforward method to interpret a universe of propositions with propositional extensionality within categories equipped with subobject classifiers, building on Lumsdaine's local universes.
Contribution
It introduces a simple coherence construction for propositional universes in categorical models, extending Lumsdaine's local universes framework.
Findings
Provides a categorical interpretation of propositional extensionality
Enables modeling of propositional universes with subobject classifiers
Simplifies the construction of propositional universes in categorical settings
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsComputability, Logic, AI Algorithms · Computational Physics and Python Applications