The General Universal Property of the Propositional Truncation
(2015)
Journal Article
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 functions from A to B. This involves an infinite tower of coherence c... Read More about The General Universal Property of the Propositional Truncation.