diff options
| -rw-r--r-- | HoTT_Base.thy | 2 | ||||
| -rw-r--r-- | ROOT | 18 |
2 files changed, 18 insertions, 2 deletions
diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 2ad0ac5..69cc1b1 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -14,6 +14,8 @@ begin section \<open>Basic setup\<close> +declare[[eta_contract=false]] + typedecl t \<comment> \<open>Type of object types and terms\<close> typedecl ord \<comment> \<open>Type of meta-level numerals\<close> @@ -1,10 +1,24 @@ +chapter HoTT + session HoTT = Pure + + description {* + Homotopy type theory based on intensional Martin-Löf type theory, with a cumulative universe + hierarchy à la Russell. + + Follows the development of the theory in + The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics, + Institute for Advanced Study, (2013). + Available online at https://homotopytypetheory.org/book. + + Author: Joshua Chen, University of Bonn (2018) + *} sessions "HOL-Eisbach" theories + HoTT (global) HoTT_Base - HoTT + HoTT_Methods "tests/Test" "ex/Methods" "ex/Synthesis" - "ex/Book/Ch1"
\ No newline at end of file + "ex/Book/Ch1" |