|
| | | | |
| | | |
| Stat |
Members: 3645
Articles: 2'501'711
Articles rated: 2609
19 April 2024 |
|
| | | | |
|
Article overview
| |
|
|
Games for Dependent Types | | Samson Abramsky
; Radha Jagadeesan
; Matthijs Vákár
; | | Date: |
20 Aug 2015 | | Abstract: | We present a model of dependent type theory (DTT) with Pi-, 1-, Sigma- and
intensional Id-types, which is based on a slight variation of the category of
AJM-games and history-free winning strategies. The model satisfies Streicher’s
criteria of intensionality and refutes function extensionality. The principle
of uniqueness of identity proofs is satisfied.
We show it contains a submodel as a full subcategory which gives a faithful
model of DTT with Pi-, 1-, Sigma- and intensional Id-types and, additionally,
finite inductive type families. This smaller model is fully (and faithfully)
complete with respect to the syntax at the type hierarchy built without
Id-types, as well as at the class of types where we allow for one strictly
positive occurrence of an Id-type. Definability for the full type hierarchy
with Id-types remains to be investigated. | | Source: | arXiv, 1508.5023 | | Services: | Forum | Review | PDF | Favorites | |
|
|
No review found.
Did you like this article?
Note: answers to reviews or questions about the article must be posted in the forum section.
Authors are not allowed to review their own article. They can use the forum section.
browser Mozilla/5.0 AppleWebKit/537.36 (KHTML, like Gecko; compatible; ClaudeBot/1.0; +claudebot@anthropic.com)
|
| |
|
|
|
|
News, job offers and information for researchers and scientists:
| |
REGISTER