A categorical formulation of Kraus' paradox
<|reference_start|>A categorical formulation of Kraus' paradox: We give a categorical formulation of Kraus' "magic trick" for recovering information from truncated types. Rather than type theory, we work in Van den Berg-Moerdijk path categories with a univalent universe, and rather than propositional truncation we work with arbitrary cofibrations, which includes truncation as a special case. We show, using Kraus' argument that any cofibration with homogeneous domain is a monomorphism. We give some simple concrete examples in groupoids to illustrate the interaction between homogeneous types, cofibrations and univalent fibrations.<|reference_end|>
@article{swan2024a,
    title={A categorical formulation of Kraus' paradox},
    author={Andrew W. Swan},
    journal={arXiv preprint arXiv:2403.17961},
    year={2024},
    archivePrefix={arXiv},
    eprint={2403.17961},
    primaryClass={math.CT cs.LO math.LO}
}