§ The groupoid interpretation of type theory

The monograph by Martin Hofmann and Thomas Streicher is remarkably lucid. It opens by stating that UIP (uniqueness of identity proofs) is false by providing a model for the axioms of MLTT where UIP fails --- a groupoid!