Universal Properties of Truncations

Homotopy Type Theory

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

Advertisements
This entry was posted in Philosophie. Bookmark the permalink.

Leave a Reply

Please log in using one of these methods to post your comment:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s