UF IAS 2012 Archive Setoids, Groupoids, etc

Here are some resources on these:

• Martin Hofmann’s thesis: Extensional concepts in intensional type theory.
• the n-Lab page on exact completions.
• Hofmann-Streicher: the groupoid model.
• Michael Warren’s thesis: contains the construction of models using internal groupoids.
• The strict infinity-groupoid model of type theory by Michael A. Warren.
• Slides from Erik Palmgren's talk on Setoids.
• Setoids in Type Theory On setoids and partial setoids in type theory.
• On the Axiom of Extensionality, Part I by Robin Gandy, 1959, contains a readable explanation of how to interpret the axiom of extensionality for Church’s higher-order logic. This is connected to the notion of logical relation in typed lambda calculus.
• Setoids are locally cartesian cartesian closed in Coq: an illustration of use of dependent setoid constructions.

Please add more.