+++
title = "Homotopy Type Theory (HOTT)"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["4e4"]
forwardlinks = ["4e6"]
zettelid = "4e5"
+++

Homotopy type theory is essentially extended Martin-Löf Type Theory
(MLTT), with a better formulation of equality which allows it to express
equality of types in a tower of equalities. This notion of equality
comes from homotopy, but doesn't really need homotopy to understand the
formulation of equality. Instead, it is just a different formulation,
using the univalence axiom (UA) as the basis to the system.