Skip to main content
guest
Join

Help

Sign In
UFIAS2012
Home
guest

Join

Help

Sign In
UFIAS2012
Wiki Home
Projects
Recent Changes
Pages and Files
Members
Favorites
20
All Pages
20
Home
Calendar
Categorical Semantics WG
Coq for UF
Coq Working Group
Definitional Equality
Formalized Homotopy Theory
Higher Inductive Types
Homotopy Type System
HomotopyGroupsOfSpheres
how to add a plugin
IAS program participants
Informal Type Theory
Logical Frameworks
Math in HoTT
Meaning Explanations
Modal type theory
Notation and terminology
Notes
Open Problems
see more
Add
Add "All Pages"
Done
Setoid model of type theory formalized
Edit
0
8
…
2
Tags
formal
semantics
Notify
RSS
Backlinks
Source
Print
Export (PDF)
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
Javascript Required
You need to enable Javascript in your browser to edit pages.
help on how to format text
Turn off "Getting Started"
Home
...
Loading...
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