Skip to main content

Browse the archive

https://github.com/jaycech3n/Isabelle-HoTT
07 June 2021, 00:05:13 UTC
Revision a9606c980dcc32ade28ebd1515cad33b380ebd64 authored by Josh Chen on 28 May 2020, 10:54:40 UTC, committed by Josh Chen on 28 May 2020, 10:54:40 UTC 
reorganize folder structure
1 parent f12983b
Raw File
Tip revision: a9606c980dcc32ade28ebd1515cad33b380ebd64 authored by Josh Chen on 28 May 2020, 10:54:40 UTC
reorganize folder structure
Tip revision: a9606c9
ROOT 
session Spartan_Core in "spartan/core" = Pure +
  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.
  "
  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.
  "
  directories
    data
  theories
    More_Types
    Maybe
    List

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
    Identity
    Equivalence
    Nat
    More_List
    Eckmann_Hilton
back to top