A categorical formulation of Kraus' paradox
Category Theory
2024-03-28 v1 Logic in Computer Science
Logic
Abstract
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.
Cite
@article{arxiv.2403.17961,
title = {A categorical formulation of Kraus' paradox},
author = {Andrew W. Swan},
journal= {arXiv preprint arXiv:2403.17961},
year = {2024}
}