The Path Model of Intensional Type Theory
Ladda ner
Typ
Examensarbete för masterexamen
Master Thesis
Master Thesis
Program
Computer science – algorithms, languages and logic (MPALG), MSc
Publicerad
2015
Författare
Ruch, Fabian
Modellbyggare
Tidskriftstitel
ISSN
Volymtitel
Utgivare
Sammanfattning
The groupoid interpretation of Martin-Löf type theory not only shows the independence of uniqueness of identity proofs from the axioms of intensional type theory but is also constructive and validates the computation rules as definitional equalities. The groupoid semantics are very clear when interpreting dependent types and in particular the identity types but less so when defining equality preservation for terms, interpreting context extension or constructing the transport for identity proofs. The indirections stem from the fact that paths over paths is a derived notion in the groupoid interpretation. The notion is, however, a primitive in so called relational models which have been employed to prove abstraction theorems for type theories. We generalise the groupoid interpretation to a refined relational interpretation of intensional type theory and show that it is a model in the sense of categories with families. The refined relations support a concatenation operator that has identities and inverses; hence a model of paths.
Beskrivning
Ämne/nyckelord
Informations- och kommunikationsteknik , Data- och informationsvetenskap , Information & Communication Technology , Computer and Information Science