The General Universal Property of the Propositional Truncation

Nicolai Kraus

In a type-theoretic fibration category in the sense of Shulman (representing a dependent type theory with at least 1, Sigma, Pi, and identity types), we define the type of constant…