The groupoid model of type theory

Please expand.

References

The groupoid model of type theory was introduced by Martin Hofmann and Thomas Streicher in 1998:

Hofmann, Martin, and Thomas Streicher. 1998. ‘The Groupoid Interpretation of Type Theory’. In Twenty-Five Years of Constructive Type Theory, edited by Giovanni Sambin and Jan M. Smith, 36:83–111. Oxford Logic Guides. Oxford University Press. terrible citeseer link

@incollection{hofmann_groupoid_1998,
	series = {Oxford {Logic} {Guides}},
	title = {The groupoid interpretation of type theory},
	volume = {36},
	booktitle = {Twenty-{Five} {Years} of {Constructive} {Type} {Theory}},
	publisher = {Oxford University Press},
	author = {Hofmann, Martin and Streicher, Thomas},
	editor = {Sambin, Giovanni and Smith, Jan M.},
	year = {1998},
	pages = {83--111}
}