blob: 78c116b34223f6e1689508cea54bf667f3d083de (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
+++
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.
|
