diff options
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 |