projections

3 files changed, 44 insertions, 40 deletions

diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 9b422c4..7794601 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -2,7 +2,7 @@
     Author: Josh Chen
     Date:   Jun 2018
 
-Basic setup and definitions of a homotopy type theory object logic.
+Basic setup and definitions of a homotopy type theory object logic without universes.
 *)
 
 theory HoTT_Base
@@ -18,16 +18,23 @@ text "Set up type checking routines, proof methods etc."
 section \<open>Metalogical definitions\<close>
 
 text "A single meta-type \<open>Term\<close> suffices to implement the object-logic types and terms.
-Our implementation does not have universes, and we simply use \<open>a : U\<close> as a convenient shorthand meaning ``\<open>a\<close> is a type''."
+We do not implement universes, and simply use \<open>a : U\<close> as a convenient shorthand to mean ``\<open>a\<close> is a type''."
 
 typedecl Term
 
 
 section \<open>Judgments\<close>
 
+text "We formalize the judgments \<open>a : A\<close> and \<open>A : U\<close> separately, in contrast to the HoTT book where the latter is considered an instance of the former.
+
+For judgmental equality we use the existing Pure equality \<open>\<equiv>\<close> and hence do not need to define a separate judgment for it."
+
 consts
-is_a_type :: "Term \<Rightarrow> prop"           ("(1_ :/ U)" [0] 1000)
-is_of_type :: "[Term, Term] \<Rightarrow> prop"  ("(1_ :/ _)" [0, 0] 1000)
+  is_a_type :: "Term \<Rightarrow> prop"           ("(1_ :/ U)" [0] 1000)
+  is_of_type :: "[Term, Term] \<Rightarrow> prop"  ("(1_ :/ _)" [0, 0] 1000)
+
+axiomatization where
+  inhabited_implies_type [intro]: "\<And>a A. a : A \<Longrightarrow> A : U"
 
 
 section \<open>Type families\<close>
@@ -36,31 +43,10 @@ text "A (one-variable) type family is a meta lambda term \<open>P :: Term \<Righ
 
 type_synonym Typefam = "Term \<Rightarrow> Term"
 
-abbreviation is_type_family :: "[Typefam, Term] \<Rightarrow> prop"  ("(3_:/ _ \<rightarrow> U)")
+abbreviation (input) is_type_family :: "[Typefam, Term] \<Rightarrow> prop"  ("(3_:/ _ \<rightarrow> U)")
   where "P: A \<rightarrow> U \<equiv> (\<And>x. x : A \<Longrightarrow> P x : U)"
 
-text "There is an obvious generalization to multivariate type families, but implementing such an abbreviation involves writing ML and is for the moment not really crucial."
-
-
-section \<open>Definitional equality\<close>
-
-text "The Pure equality \<open>\<equiv>\<close> is used for definitional aka judgmental equality of types and terms."
-
-\<comment> \<open>Do these ever need to be used?
-
-theorem equal_types:
-  assumes "A \<equiv> B" and "A : U"
-  shows "B : U" using assms by simp
-
-theorem equal_type_element:
-  assumes "A \<equiv> B" and "x : A"
-  shows "x : B" using assms by simp
+text "There is an obvious generalization to multivariate type families, but implementing such an abbreviation involves writing ML code, and is for the moment not really crucial."
 
-lemmas type_equality =
-  equal_types
-  equal_types[rotated]
-  equal_type_element
-  equal_type_element[rotated]
-\<close>
 
 end
\ No newline at end of file
diff --git a/HoTT_Theorems.thy b/HoTT_Theorems.thy
index 2c2a31d..ab5374d 100644
--- a/HoTT_Theorems.thy
+++ b/HoTT_Theorems.thy
@@ -34,6 +34,9 @@ proof
   fix a
   assume "a : A"
   then show "\<^bold>\<lambda>y:B. a : B \<rightarrow> A" ..
+
+  ML_val \<open>@{context} |> Variable.names_of\<close>
+
 qed
 
 
diff --git a/Sum.thy b/Sum.thy
index 8dab3e8..3db0f23 100644
--- a/Sum.thy
+++ b/Sum.thy
@@ -6,7 +6,7 @@ Dependent sum type.
 *)
 
 theory Sum
-  imports HoTT_Base Prod
+  imports Prod
 
 begin
 
@@ -68,32 +68,47 @@ overloading
   snd_nondep \<equiv> snd
 begin
   definition snd_dep :: "[Term, Typefam] \<Rightarrow> Term" where
-    "snd_dep A B \<equiv> indSum[A,B] (\<lambda>p. B(fst[A,B]`p)) (\<lambda>x y. y)"
+    "snd_dep A B \<equiv> indSum[A,B] (\<lambda>p. B fst[A,B]`p) (\<lambda>x y. y)"
   
   definition snd_nondep :: "[Term, Term] \<Rightarrow> Term" where
-    "snd_nondep A B \<equiv> indSum[A, \<lambda>_. B] (\<lambda>p. B((fst A B)`p)) (\<lambda>x y. y)"
+    "snd_nondep A B \<equiv> indSum[A, \<lambda>_. B] (\<lambda>_. B) (\<lambda>x y. y)"
 end
 
-text "Simplification rules:"
+text "Properties of projections:"
+
+lemma fst_dep_type:
+  assumes "p : \<Sum>x:A. B x"
+  shows "fst[A,B]`p : A"
+proof -
+  have "\<Sum>x:A. B x : U" using assms ..
+  then have "A : U" by (rule Sum_intro)
+  unfolding fst_dep_def using assms by (rule Sum_comp)
+  
 
 lemma fst_dep_comp:
-  assumes "a : A" and "b : B(a)"
+  assumes "a : A" and "b : B a"
   shows "fst[A,B]`(a,b) \<equiv> a"
 proof -
-  show "fst[A,B]`(a,b) \<equiv> a" unfolding fst_dep_def using assms by simp
+  have "A : U" using assms(1) ..
+  then have "\<lambda>_. A: \<Sum>x:A. B x \<rightarrow> U" .
+  moreover have "\<And>x y. x : A \<Longrightarrow> (\<lambda>x y. x) x y : A" .
+  ultimately show "fst[A,B]`(a,b) \<equiv> a" unfolding fst_dep_def using assms by (rule Sum_comp)
 qed
 
-lemma snd_dep_comp: "\<lbrakk>a : A; b : B(a)\<rbrakk> \<Longrightarrow> snd[A,B]`(a,b) \<equiv> b"
+lemma snd_dep_comp:
+  assumes "a : A" and "b : B a"
+  shows "snd[A,B]`(a,b) \<equiv> b"
 proof -
-  assume "a : A" and "b : B(a)"
-  then have "(a, b) : \<Sum>x:A. B(x)" ..
-  then show "snd[A,B]`(a,b) \<equiv> b" unfolding snd_dep_def by simp
+  have "\<lambda>p. B fst[A,B]`p: \<Sum>x:A. B x \<rightarrow> U"
+    
+  ultimately show "snd[A,B]`(a,b) \<equiv> b" unfolding snd_dep_def by (rule Sum_comp)
 qed
 
-lemma fst_nondep_comp: "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> fst[A,B]`(a,b) \<equiv> a"
+lemma fst_nondep_comp:
+  assumes "a : A" and "b : B"
+  shows "fst[A,B]`(a,b) \<equiv> a"
 proof -
-  assume "a : A" and "b : B"
-  then have "(a, b) : A \<times> B" ..
+  have "A : U" using assms(1) ..
   then show "fst[A,B]`(a,b) \<equiv> a" unfolding fst_nondep_def by simp
 qed