blob: e62fa06f27ae71fd93bd4bb8f774f78adb77dc60 (
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
|
session Spartan in "spartan/theories" = Pure +
description "
Spartan type theory: a minimal dependent type theory based on
intensional Martin-Löf type theory with cumulative Russell-style universes,
Pi, Sigma and identity types.
"
sessions
"HOL-Eisbach"
theories
Spartan (global)
Identity
Equivalence
session HoTT in hott = Spartan +
description "
Homotopy type theory, following the development in
The Univalent Foundations Program,
Homotopy Type Theory: Univalent Foundations of Mathematics,
Institute for Advanced Study, (2013).
Available online at https://homotopytypetheory.org/book.
"
theories
Basic_Types
Nat
|
