https://github.com/jaycech3n/Isabelle-HoTT
Revision 831f33468f227c0dc96bd31380236f2c77e70c52 authored by Josh Chen on 09 July 2020, 11:35:39 UTC, committed by Josh Chen on 09 July 2020, 11:35:39 UTC
1 parent fc9ba21
Tip revision: 831f33468f227c0dc96bd31380236f2c77e70c52 authored by Josh Chen on 09 July 2020, 11:35:39 UTC
Non-annotated object lambda
Non-annotated object lambda
Tip revision: 831f334
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."
sessions
"HOL-Eisbach"
theories
Spartan (global)
session Spartan in spartan = Spartan_Core +
description
"Dependent type theory based on Spartan."
directories
lib
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
More_Nat
Computing file changes ...