diff options
Diffstat (limited to 'content/zettel/4e5.md')
| -rw-r--r-- | content/zettel/4e5.md | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/content/zettel/4e5.md b/content/zettel/4e5.md new file mode 100644 index 0000000..78c116b --- /dev/null +++ b/content/zettel/4e5.md @@ -0,0 +1,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. |