Cubical sets as a classifying topos

Bas Spitters

Abstract

Coquand’s cubical set model for homotopy type theory provides the basis for a computational interpretation of the univalence axiom and some higher inductive types, as implemented in the cubical proof assistant. We show that the underlying cube category is the opposite of the Lawvere theory of De Morgan algebras. The topos of cubical sets itself classifies the theory of ‘free De Morgan algebras’.
This provides us with a topos with an internal ‘interval’. Using this interval we construct a model of type theory following van den Berg and Garner. We are currently investigating the precise relation with Coquand’s. We do not exclude that the interval can also be used to construct other models.

Originalsprog	Engelsk
Publikationsdato	2015
Antal sider	2
Status	Udgivet - 2015
Begivenhed	21st International Conference on Types for Proofs and Programs, : TYPES 2015 - Tallinn, Estland Varighed: 18 maj 2015 → 21 maj 2015

Konference

Konference	21st International Conference on Types for Proofs and Programs,
Land/Område	Estland
By	Tallinn
Periode	18/05/2015 → 21/05/2015

Adgang til dokumentet

TYPES15Forlagets udgivne version, 188 KBLicens: CC BY-SA

Andre filer og links

http://cs.ioc.ee/types15/

Citationsformater

@conference{e1e6eede6d344205a2e6484af38371e4,

title = "Cubical sets as a classifying topos",

abstract = "Coquand{\textquoteright}s cubical set model for homotopy type theory provides the basis for a computational interpretation of the univalence axiom and some higher inductive types, as implemented in the cubical proof assistant. We show that the underlying cube category is the opposite of the Lawvere theory of De Morgan algebras. The topos of cubical sets itself classifies the theory of {\textquoteleft}free De Morgan algebras{\textquoteright}.This provides us with a topos with an internal {\textquoteleft}interval{\textquoteright}. Using this interval we construct a model of type theory following van den Berg and Garner. We are currently investigating the precise relation with Coquand{\textquoteright}s. We do not exclude that the interval can also be used to construct other models.",

author = "Bas Spitters",

year = "2015",

language = "English",

note = "21st International Conference on Types for Proofs and Programs, : TYPES 2015 ; Conference date: 18-05-2015 Through 21-05-2015",

}

TY - ABST

T1 - Cubical sets as a classifying topos

AU - Spitters, Bas

PY - 2015

Y1 - 2015

N2 - Coquand’s cubical set model for homotopy type theory provides the basis for a computational interpretation of the univalence axiom and some higher inductive types, as implemented in the cubical proof assistant. We show that the underlying cube category is the opposite of the Lawvere theory of De Morgan algebras. The topos of cubical sets itself classifies the theory of ‘free De Morgan algebras’.This provides us with a topos with an internal ‘interval’. Using this interval we construct a model of type theory following van den Berg and Garner. We are currently investigating the precise relation with Coquand’s. We do not exclude that the interval can also be used to construct other models.

AB - Coquand’s cubical set model for homotopy type theory provides the basis for a computational interpretation of the univalence axiom and some higher inductive types, as implemented in the cubical proof assistant. We show that the underlying cube category is the opposite of the Lawvere theory of De Morgan algebras. The topos of cubical sets itself classifies the theory of ‘free De Morgan algebras’.This provides us with a topos with an internal ‘interval’. Using this interval we construct a model of type theory following van den Berg and Garner. We are currently investigating the precise relation with Coquand’s. We do not exclude that the interval can also be used to construct other models.

UR - http://cs.ioc.ee/types15/

M3 - Conference abstract for conference

T2 - 21st International Conference on Types for Proofs and Programs,

Y2 - 18 May 2015 through 21 May 2015

ER -