  The origin of these ideas was the remarkable discovery by (Hofmann and Streicher 1998) that the axioms of intensional type theory do not force all proofs of an identity to be equal, that is, not all paths need to be trivial. This was shown by a model construction where each type is interpreted as a groupoid. 