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!