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.
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.
| Original language | English |
|---|---|
| Publication date | 2015 |
| Number of pages | 2 |
| Publication status | Published - 2015 |
| Event | 21st International Conference on Types for Proofs and Programs, : TYPES 2015 - Tallinn, Estonia Duration: 18 May 2015 → 21 May 2015 |
Conference
| Conference | 21st International Conference on Types for Proofs and Programs, |
|---|---|
| Country/Territory | Estonia |
| City | Tallinn |
| Period | 18/05/2015 → 21/05/2015 |