Stack semantics of type theory

Thierry Coquand; Bassel Mannaa; Fabian  Ruch

doi:10.1109/LICS.2017.8005130

Stack semantics of type theory

Thierry Coquand, Bassel Mannaa, Fabian Ruch

Publikation: Artikel i tidsskrift og konference artikel i tidsskrift › Konferenceartikel › Forskning › peer review

Abstract

We give a model of dependent type theory with one univalent universe and propositional truncation interpreting a type as a stack, generalizing the groupoid model of type theory. As an application, we show that countable choice cannot be proved in dependent type theory with one univalent universe and propositional truncation.

Originalsprog	Engelsk
Tidsskrift	Annual Symposium on Logic in Computer Science
Antal sider	12
ISSN	1043-6871
DOI	https://doi.org/10.1109/LICS.2017.8005130
Status	Udgivet - 23 jun. 2017
Begivenhed	Thirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science - Reykjavik, Island Varighed: 20 jun. 2017 → 23 aug. 2017 Konferencens nummer: 32

Konference

Konference	Thirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science
Nummer	32
Land/Område	Island
By	Reykjavik
Periode	20/06/2017 → 23/08/2017

Adgang til dokumentet

10.1109/LICS.2017.8005130

Stack Semantics of Type TheoryAccepteret manuskript, 399 KBLicens: Ikke-specificeret

Citationsformater

@inproceedings{cb5e351ead204f8d8b9b664f2c31a055,

title = "Stack semantics of type theory",

abstract = "We give a model of dependent type theory with one univalent universe and propositional truncation interpreting a type as a stack, generalizing the groupoid model of type theory. As an application, we show that countable choice cannot be proved in dependent type theory with one univalent universe and propositional truncation.",

keywords = "dependent type theory, univalent universe, propositional truncation, groupoid model, countable choice",

author = "Thierry Coquand and Bassel Mannaa and Fabian Ruch",

year = "2017",

month = jun,

day = "23",

doi = "10.1109/LICS.2017.8005130",

language = "English",

journal = "Annual Symposium on Logic in Computer Science",

issn = "1043-6871",

publisher = "I E E E Computer Society",

note = "Thirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ; Conference date: 20-06-2017 Through 23-08-2017",

}

TY - GEN

T1 - Stack semantics of type theory

AU - Coquand, Thierry

AU - Mannaa, Bassel

AU - Ruch, Fabian

N1 - Conference code: 32

PY - 2017/6/23

Y1 - 2017/6/23

N2 - We give a model of dependent type theory with one univalent universe and propositional truncation interpreting a type as a stack, generalizing the groupoid model of type theory. As an application, we show that countable choice cannot be proved in dependent type theory with one univalent universe and propositional truncation.

AB - We give a model of dependent type theory with one univalent universe and propositional truncation interpreting a type as a stack, generalizing the groupoid model of type theory. As an application, we show that countable choice cannot be proved in dependent type theory with one univalent universe and propositional truncation.

KW - dependent type theory

KW - univalent universe

KW - propositional truncation

KW - groupoid model

KW - countable choice

U2 - 10.1109/LICS.2017.8005130

DO - 10.1109/LICS.2017.8005130

M3 - Conference article

SN - 1043-6871

JO - Annual Symposium on Logic in Computer Science

JF - Annual Symposium on Logic in Computer Science

T2 - Thirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science

Y2 - 20 June 2017 through 23 August 2017

ER -

Stack semantics of type theory

Abstract

Konference

Adgang til dokumentet

Fingeraftryk

Citationsformater