# Stack Semantics of Type Theory

## TL;DR

This paper introduces a stack-based model of dependent type theory with univalence and propositional truncation, demonstrating limitations on proving countable choice within this framework.

## Contribution

It generalizes the groupoid model by interpreting types as stacks, providing new insights into the semantics of type theory with univalence.

## Key findings

- Countable choice cannot be proved in the given type theory
- Models types as stacks, extending groupoid models
- Provides a new semantic framework for dependent type theory

## 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.