We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
A generalization of the Takeuti–Gandy interpretation.
- Authors
BARRAS, BRUNO; COQUAND, THIERRY; HUBER, SIMON
- Abstract
We present an interpretation of a version of dependent type theory where a type is interpreted by a Kan semisimplicial set. This interprets only a weak notion of conversion similar to the one used in the first published version of Martin-Löf type theory. Each truncated version of this model can be carried out internally in dependent type theory, and we have formalized the first truncated level, which is enough to represent isomorphisms of algebraic structure as equality.
- Subjects
GENERALIZATION; DEPENDENCE (Statistics); TYPE theory; ISOMORPHISM (Mathematics); ORDERED algebraic structures
- Publication
Mathematical Structures in Computer Science, 2015, Vol 25, Issue 5, p1071
- ISSN
0960-1295
- Publication type
Article
- DOI
10.1017/S0960129514000504