From the 1 of 3 linked papers with an AI index.
3 papers
math.CT2026
A categorical formulation of Kraus' paradox
Andrew W. Swan
The paper reformulates Kraus' paradox about recovering information from truncated types in categorical terms, using Van den Berg‑Moerdijk path categories with a univalent universe…
math.LO2026
Makkai's lost proof of projectivity of N in the free topos
Henrik Forssell, Peter LeFanu Lumsdaine, Andrew W. Swan
We give a categorical proof of the projectivity of in the free topos -- in proof-theoretic terms, the rule of countable choice for intuitionistic higher-order logic -- based on…
math.LO2024
Oracle modalities
Andrew W Swan
We give a new formulation of Turing reducibility in terms of higher modalities, inspired by an embedding of the Turing degrees in the lattice of subtoposes of the effective topos d…