UF IAS 2012 Archive
Setoid model of type theory formalized

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

Created on April 19, 2018 at 17:16:58 by Univalent foundations special year 2012