aboutsummaryrefslogtreecommitdiff
path: root/ROOT
blob: 09e304203227b7d84922c84bf6b45a6ecbcb00f5 (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
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
    Base
    Nat