Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
The example given (propositional truncation) is only correct up to set truncation.
@2
Why does the example of propositional truncation fail for types which aren’t sets?
i.e. what is the difference between
$\prod_{a:A} \prod_{b:A} a =_A b$and
$\prod_{c:A \times A} \pi_1(c) =_A \pi_2(c)$It’s not just that the type has to be a set, but that you have to set-truncate the coequalizer to get the propositional truncation. For instance, if $A=1$ (which is a set) then the coequalizer of the two projections is the circle $S^1$, which is not the propositional truncation of $1$.
There was a section about W-suspensions titled “Higher inductive types generated by graphs” in the article coequalizer type, so I moved the section into its own page at W-suspension.
1 to 8 of 8