diff options
Diffstat (limited to 'ROOT')
| -rw-r--r-- | ROOT | 21 |
1 files changed, 10 insertions, 11 deletions
@@ -1,18 +1,16 @@ session Spartan_Core in "spartan/core" = Pure + - description " - Spartan type theory: a minimal dependent type theory based on intensional + description + "Spartan type theory: a minimal dependent type theory based on intensional Martin-Löf type theory with cumulative Russell-style universes, Pi types and - Sigma types. This session consists only of the very core theory files. - " + Sigma types." sessions "HOL-Eisbach" theories Spartan (global) session Spartan in spartan = Spartan_Core + - description " - Type theory based on Spartan, but with a few more bells and whistles. - " + description + "Dependent type theory based on Spartan." directories lib theories @@ -21,15 +19,16 @@ session Spartan in spartan = Spartan_Core + List session HoTT in hott = Spartan + - description " - Homotopy type theory, following the development in + 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. - " + Available online at https://homotopytypetheory.org/book." theories Identity Equivalence Nat More_List + More_Nat + |