# nLab book homotopy type theory

Contents

### Context

#### Constructivism, Realizability, Computability

intuitionistic mathematics

foundations

# Contents

## Idea

The homotopy type theory presented in the HoTT book.

## Definition

Book homotopy type theory or Book HoTT is a Martin-Löf univalent type theory with all the additional types mentioned in the HoTT book: