Stack Semantics of Type Theory

2017/01/10 by Thierry Coquand, Coquand, Thierry, Bassel Mannaa +3 · 1 citation
Computer Science · #Advanced Algebra and Logic #F.3.2 #F.4.1 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems

paper · pdf · doi:10.48550/arxiv.1701.02571

openalex publication_date 2017/01/10 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

We give a model of dependent type theory with one univalent universe and propositional truncation interpreting a type as a stack, generalising 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.

Cited by

• Guarded Realization Semantics: Occurrence-Sensitive Certificates and Behavior-Dependent Lower Bounds

Related

• (Pointed) Univalence in Universe Category Models of Type Theory
• Bounded First-Class Universe Levels in Dependent Type Theory
• Type theories in category theory
• Dependent Types Simplified
• A general definition of dependent type theories