Merely Inhabited

A type A 𝐴 A is merely inhabited if its Propositional Truncation A norm 𝐴 ||A|| is inhabited.