# nLab univalent type theory

Contents

### Context

#### Constructivism, Realizability, Computability

intuitionistic mathematics

foundations

# Contents

## Definition

A univalent type theory is a dependent type theory with type universes and identity types such that all universes satisfy the univalence axiom.

Univalent type theories usually have additional types such as the empty type, the unit type, the booleans, and the natural numbers type, making it into a Martin-Löf dependent type theory.