The Path Model of Intensional Type Theory

Examensarbete för masterexamen

Please use this identifier to cite or link to this item: https://hdl.handle.net/20.500.12380/228384
Download file(s):
File Description SizeFormat 
228384.pdfFulltext414.69 kBAdobe PDFView/Open
Type: Examensarbete för masterexamen
Master Thesis
Title: The Path Model of Intensional Type Theory
Authors: Ruch, Fabian
Abstract: 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.
Keywords: Informations- och kommunikationsteknik;Data- och informationsvetenskap;Information & Communication Technology;Computer and Information Science
Issue Date: 2015
Publisher: Chalmers tekniska högskola / Institutionen för data- och informationsteknik (Chalmers)
Chalmers University of Technology / Department of Computer Science and Engineering (Chalmers)
URI: https://hdl.handle.net/20.500.12380/228384
Collection:Examensarbeten för masterexamen // Master Theses



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.