To the top

Page Manager: Webmaster
Last update: 9/11/2012 3:13 PM

Tell a friend about this page
Print version

A Model of Type Theory in… - University of Gothenburg, Sweden Till startsida
To content Read more about how we use cookies on

A Model of Type Theory in Cubical Sets

Licentiate thesis
Authors Simon Huber
Date of public defense 2015-05-22
Opponent at public defense Prof. Marcelo Fiore, Computer Laboratory, University of Cambridge, United Kingdom
Publisher University of Gothenburg
Place of publication Göteborg
Publication year 2015
Published at Department of Computer Science and Engineering, Computing Science, Programming Logic
Language en
Keywords Models of dependent type theory, cubical sets, Univalent Foundations
Subject categories Theoretical computer science, Mathematical logic


The intensional identity type is one if the most intricate concepts of dependent type theory. The recently discovered connection between homotopy theory and type theory gives a novel perspective on the identity type. Voevodsky's so-called Univalence Axiom furthermore explains the identity type for type theoretic universes as homotopy equivalences. This licentiate thesis is concerned with understanding these new developments from a computational point of view. While the Univalence Axiom has a model using Kan simplicial sets, this model inherently uses classical logic and thus can not be used to explain the axiom computationally. To preserve the computational properties of type theory it is, however, crucial to give a computational interpretation of the added constants. This thesis presents a model of dependent type theory with dependent products, sums, a universe, and identity types, based on cubical sets. The novelty of this model is that it is formulated in a constructive meta theory.

Page Manager: Webmaster|Last update: 9/11/2012

The University of Gothenburg uses cookies to provide you with the best possible user experience. By continuing on this website, you approve of our use of cookies.  What are cookies?