Till sidans topp

Sidansvarig: Webbredaktion
Sidan uppdaterades: 2012-09-11 15:12

Tipsa en vän
Utskriftsversion

Cubical type theory: a co… - Göteborgs universitet Till startsida
Webbkarta
Till innehåll Läs mer om hur kakor används på gu.se

Cubical type theory: a constructive interpretation of the univalence axiom

Artikel i vetenskaplig tidskrift
Författare Cyril Cohen
Thierry Coquand
Simon Huber
Anders Mörtberg
Publicerad i Journal of Applied Logics
Volym 4
Nummer/häfte 10
Sidor 3127-3169
ISSN 2055-3706
Publiceringsår 2017
Publicerad vid Institutionen för data- och informationsteknik, datavetenskap, programmeringslogik (GU)
Institutionen för data- och informationsteknik (GU)
Sidor 3127-3169
Språk en
Ämneskategorier Datavetenskap (datalogi)

Sammanfattning

This paper presents a type theory in which it is possible to directly manipulate n-dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent type theory in a cubical set model. This enables new ways to reason about identity types, for instance, function extensionality is directly provable in the system. Further, Voevodsky's univalence axiom is provable in this system. We also explain an extension with some higher inductive types like the circle and propositional truncation. Finally we provide semantics for this cubical type theory in a constructive meta-theory.

Sidansvarig: Webbredaktion|Sidan uppdaterades: 2012-09-11
Dela:

På Göteborgs universitet använder vi kakor (cookies) för att webbplatsen ska fungera på ett bra sätt för dig. Genom att surfa vidare godkänner du att vi använder kakor.  Vad är kakor?