---
title: Homotopy Type Theory
description: Homotopy type theory merges constructive type theory with algebraic topology. Learners will understand how to treat types as spaces and identity proofs as paths, providing a new foundation for computer-assisted formal mathematics.
category: mathematics
subcategory: category-theory
difficulty: beginner, intermediate, advanced
url: /subject/homotopy-type-theory
---

# Homotopy Type Theory

Homotopy type theory merges constructive type theory with algebraic topology. Learners will understand how to treat types as spaces and identity proofs as paths, providing a new foundation for computer-assisted formal mathematics.

## Available Resources

1 Books • 1 Courses • 3 Websites

## Websites

### 1. nLab: HoTT

The nLab wiki entry on homotopy type theory, a dense reference page linking identity types, univalence, higher inductive types and model-theoretic semantics to the research literature, useful for locating key papers and connecting HoTT to category theory and higher topos theory.

**Difficulty:** Beginner | **Price:** Free

**Link:** https://ncatlab.org/nlab/show/HoTT

**Tags:** homotopy-type-theory, univalent-foundations, category-theory, type-theory, reference

### 2. homotopytypetheory.org

Official hub for Homotopy Type Theory, hosting the freely available HoTT book and accompanying course materials, tutorials, and links to related papers and community resources.

**Difficulty:** Intermediate | **Language:** English | **Price:** Free

**Link:** https://homotopytypetheory.org

**Tags:** websites, mathematics-statistics, category-theory

### 3. nLab

Collaborative wiki for mathematics, physics and philosophy written from a category-theoretic viewpoint, with cross-linked entries on categories, functors, adjunctions, topos theory, higher category theory and homotopy theory. Readers can look up precise definitions, examples and references for advanced structural mathematics.

**Difficulty:** Advanced | **Language:** English | **Price:** Free

**Link:** https://ncatlab.org

**Tags:** category-theory, higher-category-theory, topos-theory, homotopy-theory, reference-wiki

## Courses

### 1. Introduction to Univalent Foundations of Mathematics with Agda

Learn univalent foundations of mathematics and homotopy type theory using Agda. Course by Martin Escardo.

**Difficulty:** Advanced | **Price:** Free

**Link:** https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/

**Tags:** univalent-foundations, homotopy-type-theory, agda, proof-assistants, type-theory

## Books

### 1. Homotopy Type Theory: Univalent Foundations of Mathematics

**Author:** The Univalent Foundations Program

Collaborative exposition written during the Institute for Advanced Study's Univalent Foundations year, presenting type theory as a foundation whose types behave like homotopy types. Covers identity types, the univalence axiom, higher inductive types, and formalised set and homotopy theory.

**Difficulty:** Advanced | **Language:** English | **Price:** Free

**Link:** https://homotopytypetheory.org/book/

**Tags:** homotopy-type-theory, univalence-axiom, higher-inductive-types, type-theory, foundations-of-mathematics

---

*This content is part of Dantes.io - Your Treasure Map to Knowledge*

*Curated by humans at Dantes.io. Personal study use welcome; republishing this curation requires permission (team@dantes.io).*

View this page online: https://dantes.io/subject/homotopy-type-theory