The General Universal Property of the Propositional Truncation

DOI10.4230/LIPIcs.TYPES.2014.111zbMath1434.03150arXiv1411.2682MaRDI QIDQ5277974

Nicolai Kraus

Publication date: 12 July 2017

Full work available at URL: https://arxiv.org/abs/1411.2682

zbMATH Keywords

universal propertycoherence conditionspropositional truncationReedy limitswell-behaved constancy

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Categorical semantics of formal languages (18C50) Type theory (03B38)

Related Items (4)

Unnamed Item ⋮ Higher Homotopies in a Hierarchy of Univalent Universes ⋮ Two-level type theory and applications ⋮ A rewriting coherence theorem with applications in homotopy type theory

This page was built for publication: The General Universal Property of the Propositional Truncation