Added precedences. Need to figure out how to organize metatypes.

1 files changed, 21 insertions, 5 deletions

diff --git a/test.thy b/HoTT_Test.thy
index d22e710..b37ac76 100644
--- a/test.thy
+++ b/HoTT_Test.thy
@@ -1,21 +1,36 @@
-theory test
+theory HoTT_Test
 imports HoTT
 begin
 
 text \<open>Check trivial stuff:\<close>
+
 lemma "Null : U"
   by (rule Null_form)
 
+lemma "\<lbrakk>A \<equiv> B; x : B\<rbrakk> \<Longrightarrow> x : A"
+proof -
+  assume "A \<equiv> B"
+  then have "B \<equiv> A" by (rule Pure.symmetric)
+  then have "x : B \<Longrightarrow> x :A"  by (rule equal_types)
+  oops
+(* qed---figure out how to discharge assumptions *)
+
 text \<open>
 Do functions behave like we expect them to?
 (Or, is my implementation at least somewhat correct?...
 \<close>
 
-lemma "A \<equiv> B \<Longrightarrow> (\<^bold>\<lambda>x. x) : B\<rightarrow>A"
+\<comment> {* NOTE!!! The issues with substitution here.
+We need the HoTT term \<open>b\<close> and the type family \<open>B\<close> to indeed be a Pure \<lambda>-term!
+This seems to mean that I have to implement the HoTT types in more than one Pure type.
+See CTT.thy for examples.
+*}
+
+lemma "A \<equiv> B \<Longrightarrow> (\<^bold>\<lambda>x:A. x) : B\<rightarrow>A"
 proof -
-  have "A \<equiv> B \<Longrightarrow> B \<equiv> A" by (rule DefEq_symmetry)
-  then have "\<And>x. A \<equiv> B \<Longrightarrow> x : B \<Longrightarrow> x : A" by (rule equal_types)
-  thus "A \<equiv> B \<Longrightarrow> (\<^bold>\<lambda>x. x) : B\<rightarrow>A" by (rule Function_intro)
+  have "A \<equiv> B \<Longrightarrow> B \<equiv> A" by (rule Pure.symmetric)
+  then have "\<And>x::Term. A \<equiv> B \<Longrightarrow> x : B \<Longrightarrow> x : A" by (rule equal_types)
+  thus "A \<equiv> B \<Longrightarrow> (\<^bold>\<lambda>x:A. x) : B\<rightarrow>A" by (rule Function_intro)
 qed
 
 lemma "\<^bold>\<lambda>x. \<^bold>\<lambda>y. x : A\<rightarrow>B\<rightarrow>A"
@@ -25,6 +40,7 @@ proof -
 qed
 
 text \<open>Here's a dumb proof that 2 is a natural number:\<close>
+
 lemma "succ(succ 0) : Nat"
 proof -
   have "0 : Nat" by (rule Nat_intro1)