Not all types are (mere) propositions, but we can "make" them so by truncation, ie. forgetting all the structure of the type except whether it is inhabited.
Let $A$ be a type and $f : A \to P$ be a map into a proposition $P$. If for every proposition $Q$:
$$ -∘f : (P \to Q) \to (A \to Q) $$
is an equivalence.
This property is called the universal property of the propositional truncation of $A$.
The basic idea is $-∘f$ "lowers" the relationship between propositions between $P$ and $Q$ to the relationship between $A$ and $P$.
We can also push it further to set truncation, and even k-truncation.