[[!redirects UIP]] [[!redirects UIP]] "[The groupoid interpretation of type theory](http://www.tcs.ifi.lmu.de/mitarbeiter/martin-hofmann/pdfs/agroupoidinterpretationoftypetheroy.pdf)" [PDF], by Martin Hofmann and Thomas Streicher, 1996. ### See also ### '[[nlab:axiom UIP|Axiom UIP]]' on the nLab wiki. [[!redirects Axiom UIP]]