GUPEA >
IT Faculty / IT-fakulteten >
Department of Computer Science and Engineering / Institutionen för data- och informationsteknik >
Doctoral Theses / Doktorsavhandlingar Institutionen för data- och informationsteknik >

Cubical Intepretations of Type Theory


Please use this identifier to cite or link to this item: http://hdl.handle.net/2077/48890

Files in This Item:

File Description SizeFormat
gupea_2077_48890_1.pdfDissertation1163KbAdobe PDF
View/Open
gupea_2077_48890_2.pdfSpikblad146KbAdobe PDF
View/Open
gupea_2077_48890_3.pdfOmslag1092KbAdobe PDF
View/Open
Title: Cubical Intepretations of Type Theory
Authors: Huber, Simon
E-mail: simon.huber@cse.gu.se
Issue Date: 8-Nov-2016
University: Göteborgs universitet. IT-fakulteten
Institution: Department of Computer Science and Engineering ; Institutionen för data- och informationsteknik
Parts of work: Marc Bezem, Thierry Coquand, and Simon Huber, A model of type theory in cubical sets, 19th International Conference on Types for Proofs and Programs (TYPES 2013) (Dagstuhl, Germany) (R. Matthes and A. Schubert, eds.), Leibniz International Proceedings in Informatics (LIPIcs), vol. 26, Schloss Dagstuhl–Leibniz-Zentrum für Informatik, 2014, pp. 107–128.

Simon Huber, A model of type theory in cubical sets, Licentiate thesis, University of Gothenburg, 2015.

Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg, Cubical type theory: a constructive interpretation of the univalence axiom, to appear in the post-proceedings of the 21st International Conference on Types for Proofs and Programs (TYPES 2015).

Simon Huber, Canonicity for cubical type theory, Preprint arXiv:1607.04156v1 [cs.LO], 2016.
Date of Defence: 2016-11-29
Disputation: Tisdagen den 29 november 2016, kl. 10.00, Hörsal KB, Kemi, Kemigården 4
Degree: Doctor of Philosophy
Publication type: Doctoral thesis
Series/Report no.: 134D
Keywords: Dependent Type Theory
Univalence Axiom
Models of Type Theory
Identity Types
Cubical Sets
Abstract: The interpretation of types in intensional Martin-Löf type theory as spaces and their equalities as paths leads to a surprising new view on the identity type: not only are higher-dimensional equalities explained as homotopies, this view also is compatible with Voevodsky's univalence axiom which explains equality for type-theoretic universes as homotopy equivalences, and formally allows to identify isomorphic structures, a principle often informally used despite its incompatibility with set theor... more
ISBN: 978-91-629-0007-6 (Print)
978-91-629-0008-3 (PDF)
URI: http://hdl.handle.net/2077/48890
Appears in Collections:Doctoral Theses from University of Gothenburg / Doktorsavhandlingar från Göteborgs universitet
Doctoral Theses / Doktorsavhandlingar Institutionen för data- och informationsteknik

 

 

© Göteborgs universitet 2011