  As the groupoid model of Hofmann and Streicher proves, identity proofs in
intensional Martin-L\"of type theory cannot generally be shown to be unique.
Inspired by a theorem by Hedberg, we give some simple characterizations of
types that do have unique identity proofs. A key ingredient in these
constructions are weakly constant endofunctions on identity types. We study
such endofunctions on arbitrary types and show that they always factor through
a propositional type, the truncated or squashed domain. Such a factorization is
impossible for weakly constant functions in general (a result by Shulman), but
we present several non-trivial cases in which it can be done. Based on these
results, we define a new notion of anonymous existence in type theory and
compare different forms of existence carefully. In addition, we show possibly
surprising consequences of the judgmental computation rule of the truncation,
in particular in the context of homotopy type theory. All the results have been
formalized and verified in the dependently typed programming language Agda.
