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.

- 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.