Clean up Equal.thy + some other tweaks

3 files changed, 28 insertions, 40 deletions

diff --git a/Equal.thy b/Equal.thy
index 7b6acb5..f9bc223 100644
--- a/Equal.thy
+++ b/Equal.thy
@@ -1,66 +1,51 @@
-(*  Title:  HoTT/Equal.thy
-    Author: Josh Chen
+(*
+Title:  Equal.thy
+Author: Joshua Chen
+Date:   2018
 
 Equality type
 *)
 
 theory Equal
-  imports HoTT_Base
+imports HoTT_Base HoTT_Methods
+
 begin
 
 
-section \<open>Constants and syntax\<close>
+section \<open>Basic definitions\<close>
 
 axiomatization
-  Equal :: "[t, t, t] \<Rightarrow> t" and
-  refl :: "t \<Rightarrow> t" and
+  Equal    :: "[t, t, t] \<Rightarrow> t" and
+  refl     :: "t \<Rightarrow> t" and
   indEqual :: "[t \<Rightarrow> t, t] \<Rightarrow> t"  ("(1ind\<^sub>=)")
 
 syntax
-  "_EQUAL" :: "[t, t, t] \<Rightarrow> t"        ("(3_ =\<^sub>_/ _)" [101, 0, 101] 100)
-  "_EQUAL_ASCII" :: "[t, t, t] \<Rightarrow> t"  ("(3_ =[_]/ _)" [101, 0, 101] 100)
+  "_equal" :: "[t, t, t] \<Rightarrow> t"        ("(3_ =\<^sub>_/ _)" [101, 0, 101] 100)
+  "_equal_ascii" :: "[t, t, t] \<Rightarrow> t"  ("(3_ =[_]/ _)" [101, 0, 101] 100)
+
 translations
   "a =[A] b" \<rightleftharpoons> "CONST Equal A a b"
   "a =\<^sub>A b" \<rightharpoonup> "CONST Equal A a b"
 
+axiomatization where
+  Equal_form: "\<lbrakk>A: U i; a: A; b: A\<rbrakk> \<Longrightarrow> a =\<^sub>A b : U i" and
 
-section \<open>Type rules\<close>
+  Equal_intro: "a : A \<Longrightarrow> (refl a): a =\<^sub>A a" and
 
-axiomatization where
-  Equal_form: "\<lbrakk>A: U i; a: A; b: A\<rbrakk> \<Longrightarrow> a =\<^sub>A b : U i"
-and
-  Equal_intro: "a : A \<Longrightarrow> (refl a): a =\<^sub>A a"
-and
   Equal_elim: "\<lbrakk>
+    p: x =\<^sub>A y;
     x: A;
     y: A;
-    p: x =\<^sub>A y;
-    \<And>x. x: A \<Longrightarrow> f x: C x x (refl x);
-    \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U i
-    \<rbrakk> \<Longrightarrow> ind\<^sub>= f p : C x y p"
-and
+    \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U i;
+    \<And>x. x: A \<Longrightarrow> f x: C x x (refl x) \<rbrakk> \<Longrightarrow> ind\<^sub>= (\<lambda>x. f x) p : C x y p" and
+
   Equal_comp: "\<lbrakk>
     a: A;
-    \<And>x. x: A \<Longrightarrow> f x: C x x (refl x);
-    \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U i
-    \<rbrakk> \<Longrightarrow> ind\<^sub>= f (refl a) \<equiv> f a"
-
+    \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U i;
+    \<And>x. x: A \<Longrightarrow> f x: C x x (refl x) \<rbrakk> \<Longrightarrow> ind\<^sub>= (\<lambda>x. f x) (refl a) \<equiv> f a"
 
-text "Admissible inference rules for equality type formation:"
-
-axiomatization where
-  Equal_wellform1: "a =\<^sub>A b: U i \<Longrightarrow> A: U i"
-and
-  Equal_wellform2: "a =\<^sub>A b: U i \<Longrightarrow> a: A"
-and
-  Equal_wellform3: "a =\<^sub>A b: U i \<Longrightarrow> b: A"
-
-
-text "Rule attribute declarations:"
-
-lemmas Equal_comp [comp]
-lemmas Equal_wellform [wellform] = Equal_wellform1 Equal_wellform2 Equal_wellform3
 lemmas Equal_routine [intro] = Equal_form Equal_intro Equal_elim
+lemmas Equal_comp [comp]
 
 
 end
diff --git a/HoTT.thy b/HoTT.thy
index 3f2d475..e2a7e35 100644
--- a/HoTT.thy
+++ b/HoTT.thy
@@ -6,7 +6,6 @@ Homotopy type theory
 
 theory HoTT
 imports
-
 (* Basic theories *)
 HoTT_Base
 HoTT_Methods
@@ -22,18 +21,22 @@ Unit
 
 (* Derived definitions and properties *)
 EqualProps
-ProdProps
 Proj
 
 begin
 
+
 lemmas forms =
   Nat_form Prod_form Sum_form Coprod_form Equal_form Unit_form Empty_form
+
 lemmas intros =
   Nat_intro_0 Nat_intro_succ Prod_intro Sum_intro Equal_intro Coprod_intro_inl Coprod_intro_inr Unit_intro
+
 lemmas elims =
   Nat_elim Prod_elim Sum_elim Equal_elim Coprod_elim Unit_elim Empty_elim
+
 lemmas routines =
   Nat_routine Prod_routine Sum_routine Equal_routine Coprod_routine Unit_routine Empty_routine
 
+
 end
diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index efc6182..17e3142 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -77,7 +77,7 @@ Declare named theorems to be used by proof methods defined in @{file HoTT_Method
 These are used by the \<open>compute\<close> method, and may also be passed to invocations of the method \<open>subst\<close> to perform equational rewriting.
 \<close>
 
-(* Todo: Set up the simplifier! *)
+(* Todo: Set up the Simplifier! *)
 
 
 end