diff options
| author | Josh Chen | 2020-04-03 01:13:29 +0200 |
|---|---|---|
| committer | Josh Chen | 2020-04-03 01:13:34 +0200 |
| commit | 97f3c05e0511a1ed9a95babc800a8e3f3b6a2ea8 (patch) | |
| tree | b435de3037203e615d606d9c85fea6927ff6919d /hott/Base.thy | |
| parent | 2781c68f0fdb435827097efc497c2172d6050e50 (diff) | |
1. Base theory. 2. Fix Nat axioms, addition.
Diffstat (limited to '')
| -rw-r--r-- | hott/Base.thy (renamed from hott/Basic_Types.thy) | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/hott/Basic_Types.thy b/hott/Base.thy index 85f22a8..2a4ff9c 100644 --- a/hott/Basic_Types.thy +++ b/hott/Base.thy @@ -1,8 +1,17 @@ -theory Basic_Types -imports Spartan +theory Base +imports Spartan.Equivalence begin + +section \<open>Notation\<close> + +syntax "_dollar" :: \<open>logic \<Rightarrow> logic \<Rightarrow> logic\<close> (infixr "$" 3) +translations "a $ b" \<rightharpoonup> "a (b)" + +abbreviation (input) K where "K x \<equiv> \<lambda>_. x" + + section \<open>Sum type\<close> axiomatization |