1
$\begingroup$

This is a follow-up question from my previous question titled Constructing coproduct types and boolean types from universes, where I showed how every basic operation in set theory/topos theory could be constructed from dependent product types, dependent sum types, identity types, an empty type, and a universe $U$ which is closed under the above types, although the types constructed are usually $U$-large.

Now, the HoTT book describes set-truncations in a number of ways. In section 6.9, set-truncations of a type $A$ are first defined as the higher inductive type generated by a function $\vert - \vert_0:A \to \vert A \vert_0$, and for every element $x:A$ and $y:A$ and every path $p:x = y$ and $q:x = y$, a path $\mathrm{trunc}(x, y, p, q):p = q$. Later in the section, set-truncations are defined as a higher inductive type generated by a dependent function

$$\prod_{f:S^1 \to A} \mathrm{ap}_f(p) = \mathrm{ap}_f(q)$$

where $(S^1, 0, 1, p, q)$ is the higher inductive circle type generated by the points $0:S^1$ and $1:S^1$ and the paths $p:0 = 1$ and $q:0 = 1$. Either way, the set-truncation is constructed as a higher inductive type.

Now, is there a way to directly construct the set-truncation of a type from universes, without the use of higher inductive types? No requirements are made of the size of the resulting set-truncation, they could be $U$-large if necessary.

$\endgroup$

1 Answer 1

1
$\begingroup$

Given a universe $U$, the type of $U$-small propositions is given by $$\mathrm{Prop} \equiv \sum_{P:U} \prod_{x:P} \prod_{y:P} x = y$$ Given a type $A:U$, for $x:A$ and $y:A$, the type $$[x = y] \equiv \prod_{P:\mathrm{Prop}} ((x = y) \to P) \to P$$ is the propositional truncation of the identity type $x = y$, and is always an equivalence relation on $A$. The set-truncation of $A$ is the quotient set $$[A]_0 \equiv \sum_{P:A \to \mathrm{Prop}} \exists x:A.\forall y:A.[x = y] \iff P(x)$$

In general, this type is $U$-large unless one has an axiom like propositional resizing or replacement.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.