blob: b05d022a8181e7fae0c5ac3c38152088705008f5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
|
chapter HoTT
session HoTT = Pure +
description {*
Homotopy type theory based on intensional Martin-Löf type theory, with a cumulative universe
hierarchy à la Russell.
Follows the development of the theory in
The Univalent Foundations Program,
Homotopy Type Theory: Univalent Foundations of Mathematics,
Institute for Advanced Study, (2013).
Available online at https://homotopytypetheory.org/book.
Author: Joshua Chen, University of Bonn (2018)
*}
sessions
"HOL-Eisbach"
theories
HoTT (global)
HoTT_Base
HoTT_Methods
"tests/Test"
"ex/Methods"
"ex/Synthesis"
"ex/Book/Ch1"
|
