aboutsummaryrefslogtreecommitdiff
path: root/hott
diff options
context:
space:
mode:
Diffstat (limited to 'hott')
-rw-r--r--hott/HoTT.thy10
-rw-r--r--hott/Identity.thy4
-rw-r--r--hott/More_Types.thy (renamed from hott/Base.thy)10
-rw-r--r--hott/Nat.thy2
4 files changed, 14 insertions, 12 deletions
diff --git a/hott/HoTT.thy b/hott/HoTT.thy
new file mode 100644
index 0000000..0b3040c
--- /dev/null
+++ b/hott/HoTT.thy
@@ -0,0 +1,10 @@
+theory HoTT
+imports
+ Identity
+ Equivalence
+ More_Types
+ Nat
+
+begin
+
+end
diff --git a/hott/Identity.thy b/hott/Identity.thy
index 3a982f6..3fef536 100644
--- a/hott/Identity.thy
+++ b/hott/Identity.thy
@@ -30,13 +30,13 @@ axiomatization where
b: A;
\<And>x y p. \<lbrakk>p: x =\<^bsub>A\<^esub> y; x: A; y: A\<rbrakk> \<Longrightarrow> C x y p: U i;
\<And>x. x: A \<Longrightarrow> f x: C x x (refl x)
- \<rbrakk> \<Longrightarrow> IdInd A (\<lambda>x y p. C x y p) f a b p: C a b p" and
+ \<rbrakk> \<Longrightarrow> IdInd A (\<lambda>x y p. C x y p) (\<lambda>x. f x) a b p: C a b p" and
Id_comp: "\<lbrakk>
a: A;
\<And>x y p. \<lbrakk>x: A; y: A; p: x =\<^bsub>A\<^esub> y\<rbrakk> \<Longrightarrow> C x y p: U i;
\<And>x. x: A \<Longrightarrow> f x: C x x (refl x)
- \<rbrakk> \<Longrightarrow> IdInd A (\<lambda>x y p. C x y p) f a a (refl a) \<equiv> f a"
+ \<rbrakk> \<Longrightarrow> IdInd A (\<lambda>x y p. C x y p) (\<lambda>x. f x) a a (refl a) \<equiv> f a"
lemmas
[intros] = IdF IdI and
diff --git a/hott/Base.thy b/hott/More_Types.thy
index 610a373..17789f8 100644
--- a/hott/Base.thy
+++ b/hott/More_Types.thy
@@ -1,17 +1,9 @@
-theory Base
+theory More_Types
imports 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
diff --git a/hott/Nat.thy b/hott/Nat.thy
index 311f2d9..e129be0 100644
--- a/hott/Nat.thy
+++ b/hott/Nat.thy
@@ -1,5 +1,5 @@
theory Nat
-imports Base
+imports Equivalence
begin