Propositional truncation

In the homotopical reading of Martin-Löf type theory, the propositional truncation of a type A is a type \Vert A \Vert that has two key properties:

• it is inhabited whenever A is, and
• it is a mere proposition: all its elements are equal.

Universal property

Recall that a mere proposition is a type A for which we have an inhabitant

r_A : \prod_{x, y : A} \textsf{Id}_A(x, y)

Recall also that we have always a function

\eta : A \to \Vert A \Vert

from A to its propositional truncation.

The propositional truncation \Vert A \Vert of a type A has the following universal property: for every mere proposition B, and any function f : A \to B, there exists a unique function (the dotted line) that makes the following diagram commute:

<mxfile host="embed.diagrams.net" modified="2023-02-13T12:59:03.708Z" agent="5.0 (Windows NT 10.0; Win64; x64) AppleWebKit/537.36 (KHTML, like Gecko) Chrome/109.0.0.0 Safari/537.36" version="20.8.20" etag="LmUMqCjzMcYNJ6UiX-6q" type="embed"><diagram id="_w8WMdj2MaDjOXIP_KmT" name="Page-1">5VfbjpswEP0aXlcYAkkec9m2D6200kpt99ENDrg1ODJOFvbrO46HO8mmUVaqFCkSzPF4bM85MzGOv0qLz4rukm8yYsLx3Khw/LXjeSQIPXgYpLTIbEosECseoVMDPPM3hqCL6J5HLO84aimF5rsuuJFZxja6g1Gl5GvXbStFd9UdjdkAeN5QMUR/8EgneApv2uBfGI+TamUSzu1ISitnDJEnNJKvFjoezn90/JWSUtu3tFgxYZJX5cVm4NOJ0XpjimX6kglIxIGKPZ4N96XL6rAsgrOjmckMHkupdCJjmVHxVcod4ATA30zrErmiey0BSnQqcFTJfRYxs6oLFiu4/mneHwJ3ivaL8XxwQzTXRct3XbaMJ6Z4yjRTiNkdm22eTEKVbblXG/Ty62yDTJmEgKoEl9eGT+Ki3BQTVPNDNzxFDcX13Drck+SwsOei3isO3LLSv9sNYbeFs9pk9QKRSTeQ5/YCaapipgeBFkrRsuW2Mw552wNeWllooKNaxpXjjyhnAr+FfQxkpFmhu5KggscZvG+AJkPm8sCU5lBlCxxIeRSZ6UvFcv5Gfx1DGcbxABA3WDrB2sQCweVWeyZ0rpX8w1ZSSNWodsuF6EF4BliXFefFM1RKNYF0SZmh2RJSiFDS6gl+j7q2jDqsnKFgcoICJ1h9hyPBEJDh1tZd0TILxkulXd/kg3gJLmiqWbQwf0Qmz4LmOd+cbZcZ7MD2y8ncr4CXI+DaBmqApmUerbJtXd80bVNBJb/bNIORnAa36aMk7PVRcmUf9XolG17WRq9okuGJCl3eWTXWZXWmHD+qS85uXY0RzZOjQf6hjv6XooHbx5VF07989APdrmrmJ6pme2dVQ+a9hucPq2ZMOreoGjL2ZYCXC6bpnTEx794m6ot4i4jpbYgAs/n6s7XTfEP7j38B</diagram></mxfile>

Please add universal property in terms of type-theoretic equivalences.

Encoding through HITs

The propositional truncation of a type can be defined as a higher inductive type (HIT).

This is originally due to Lumsdaine and Shulman 2014 (still unpublished?).

A textbook account can be found in the HoTT book.

Impredicative encoding

The propositional truncation of a type can also be defined through an impredicative encoding. Assuming we have a universe \textsf{Prop} of propositions, this is given by

\Vert A \Vert = \prod_{P : \textsf{Prop}} (A \to P) \to P

Two things to remember about this:

• Its correctness (i.e. obtaining the universal property) relies on an impredicativity axiom in the type theory, propositional resizing
• It has the consequence that \Vert A \Vert is a type at a higher universe than A.

References

• nLab page on bracket types