ROOT


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
26
27
28
29
30
31
32
33
34
35

session MLTT_Core in "mltt/core" = Pure +
  description
    "Core MLTT: minimal dependent type theory based on intensional Martin-Löf
    type theory with cumulative Russell-style universes, Pi types and Sigma
    types."
  sessions
    "HOL-Eisbach"
  theories
    MLTT (global)

session MLTT in mltt = MLTT_Core +
  description
    "Dependent type theory based on MLTT_Core."
  directories
    lib
  theories
    Prelude
    Maybe
    List

session HoTT in hott = MLTT +
  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
    Identity
    Equivalence
    Nat
    Propositions
    Univalence
    Bool_HoTT
    List_HoTT