This page is about the formalization of the setoid model internally to type theory.

Thierry is giving a talk on Nov 12th to explain the model.

The Coq source file of the model has been updated (12/03): setoid_model_v2.v
It compiles with Coq 8.4 (and also the trunk so far).

Here are some notes about Thierry's talk and the precise rules of the type system
which is interpreted talk

Here is a paper describing the model and a generalization to Kan semisimplicial sets