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

Programming Logic and Semantics

University of Gothenburg

Research output: Journal Article or Conference Article in Journal › Conference article › Research › 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.

Original language	English
Journal	Annual Symposium on Logic in Computer Science
Number of pages	12
ISSN	1043-6871
DOIs	https://doi.org/10.1109/LICS.2017.8005130
Publication status	Published - 23 Jun 2017
Event	Annual ACM/IEEE Symposium on Logic in Computer Science - Reykjavik, Iceland Duration: 20 Jun 2017 → 23 Aug 2017 Conference number: 32

Conference

Conference	Annual ACM/IEEE Symposium on Logic in Computer Science
Number	32
Country/Territory	Iceland
City	Reykjavik
Period	20/06/2017 → 23/08/2017

Keywords

dependent type theory
univalent universe
propositional truncation
groupoid model
countable choice

Access to Document

10.1109/LICS.2017.8005130

Stack Semantics of Type TheoryAccepted author manuscript, 399 KBLicence: Unspecified

Cite this

@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, 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 = "IEEE",

note = "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

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 - Annual ACM/IEEE Symposium on Logic in Computer Science

Y2 - 20 June 2017 through 23 August 2017

ER -

Stack semantics of type theory

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this