Some days ago at the HoTT/UF workshop in Warsaw (which was a great event!), I have talked about functions out of truncations. I have focussed on the propositional truncation $latex Vert – Vert$, and I want to write this blog post in case someone could not attend the talk but is interested nevertheless. There are also my slides and the arXiv paper.
The topic of my talk can be summarised as
Question: What is the type $latex Vert A Vert to B$ ?
This question is very easy if $latex B$ is propositional, because then we have
Partial answer (1): If $latex B$ is propositional, then $latex (Vert A Vert to B) simeq (A to B)$
by the usual universal property, with the equivalence given by the canonical map. Without an assumption on $latex B$, it is much harder.
The rest of this post contains a special case which…
View original post 1,913 more words