Propositional truncation?

Stream: lean4

[Siddhartha Gadgil]

What is the function that takes a type to a corresponding proposition called (assuming it exists)?

[Anne Baanen]

docs#Nonempty ?

[Anne Baanen]

This is the map Type u → Prop. Or do you mean the map Type u → Type u given by the quotient by the full relation?

[Kevin Buzzard]

(which is docs#Trunc)