Showing cs.LOShow all
2 papers · 1 filter
cs.LO2024
A Coherence Construction for the Propositional Universe
Xu Huang
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…
cs.LO2023
Synthetic Tait Computability the Hard Way
Xu Huang
We walk through a few proofs of canonicity and normalization, each one with more aspects dissected and re-expressed in category theory, so that readers can compare the difference a…