A categorical formulation of Kraus' paradox
Andrew W. Swan
TL;DR
The paper presents a categorical reformulation of Kraus' paradox using univalent Van den Berg-Moerdijk path categories and cofibrations to generalize propositional truncation. It proves a central theorem: any cofibration with homogeneous domain is a monomorphism, leveraging univalence and a realignment argument. Through groupoid examples, it clarifies how homogeneous domains interact with cofibrations and truncations, illustrating when truncations remain monic. The work clarifies the relationship between univalence, homogeneity, and injectivity in path categories, and discusses variations, generalizations, and open questions. This framework provides a bridge between higher-inductive-type phenomena in type theory and their categorical counterparts, with potential implications for semantic models and SEO-relevant terminology in formalization work.
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.