The Path Model of Intensional Type Theory

Publicerad

Författare

Typ

Examensarbete för masterexamen
Master Thesis

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

Citation

Arkitekt (konstruktör)

Geografisk plats

Byggnad (typ)

Byggår

Modelltyp

Skala

Teknik / material

Index

item.page.endorsement

item.page.review

item.page.supplemented

item.page.referenced