Click here to flash read.
arXiv:2403.17961v1 Announce Type: cross
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.
Click here to read this post out
ID: 806216; Unique Viewers: 0
Unique Voters: 0
Total Votes: 0
Votes:
Latest Change: March 28, 2024, 7:31 a.m.
Changes:
Dictionaries:
Words:
Spaces:
Views: 10
CC:
No creative common's license
No creative common's license
Comments: