From 80412abb0fdec553d80a56af16d1cfd8da52e7ed Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 5 Jun 2018 17:35:49 +0200
Subject: Proved that the inductor on Sum has the correct type.

---
 HoTT.thy | 48 +++++++++++++++++++++++++++++++-----------------
 1 file changed, 31 insertions(+), 17 deletions(-)

(limited to 'HoTT.thy')

diff --git a/HoTT.thy b/HoTT.thy
index 68de364..ef39734 100644
--- a/HoTT.thy
+++ b/HoTT.thy
@@ -46,14 +46,14 @@ axiomatization
   Prod :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term" and
   lambda :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term"
 syntax
-  "_PROD" :: "[idt, Term, Term] \<Rightarrow> Term"     ("(3\<Prod>_:_./ _)" 10)
-  "_LAMBDA" :: "[idt, Term, Term] \<Rightarrow> Term"  ("(3\<^bold>\<lambda>_:_./ _)" 10)
+  "_PROD" :: "[idt, Term, Term] \<Rightarrow> Term"     ("(3\<Prod>_:_./ _)" 30)
+  "_LAMBDA" :: "[idt, Term, Term] \<Rightarrow> Term"  ("(3\<^bold>\<lambda>_:_./ _)" 30)
 translations
   "\<Prod>x:A. B" \<rightleftharpoons> "CONST Prod A (\<lambda>x. B)"
   "\<^bold>\<lambda>x:A. b" \<rightleftharpoons> "CONST lambda A (\<lambda>x. b)"
 (* The above syntax translations bind the x in the expressions B, b. *)
 
-abbreviation Function :: "[Term, Term] \<Rightarrow> Term"  (infixr "\<rightarrow>" 30)
+abbreviation Function :: "[Term, Term] \<Rightarrow> Term"  (infixr "\<rightarrow>" 10)
   where "A\<rightarrow>B \<equiv> \<Prod>_:A. B"
 
 axiomatization
@@ -69,7 +69,7 @@ where
 
   Prod_comp [simp]: "\<And>(A::Term) (b::Term \<Rightarrow> Term) (a::Term). a : A \<Longrightarrow> (\<^bold>\<lambda>x:A. b(x))`a \<equiv> b(a)" and
 
-  Prod_uniq [simp]: "\<And>(A::Term) (f::Term). \<^bold>\<lambda>x:A. (f`x) \<equiv> f"
+  Prod_uniq [simp]: "\<And>A f::Term. \<^bold>\<lambda>x:A. (f`x) \<equiv> f"
 
 lemmas Prod_formation = Prod_form Prod_form[rotated]
 
@@ -80,7 +80,7 @@ subsubsection \<open>Dependent pair/sum\<close>
 axiomatization
   Sum :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term"
 syntax
-  "_Sum" :: "[idt, Term, Term] \<Rightarrow> Term"  ("(3\<Sum>_:_./ _)" 10)
+  "_Sum" :: "[idt, Term, Term] \<Rightarrow> Term"  ("(3\<Sum>_:_./ _)" 20)
 translations
   "\<Sum>x:A. B" \<rightleftharpoons> "CONST Sum A (\<lambda>x. B)"
 
@@ -89,7 +89,7 @@ abbreviation Pair :: "[Term, Term] \<Rightarrow> Term"   (infixr "\<times>" 50)
 
 axiomatization
   pair :: "[Term, Term] \<Rightarrow> Term"  ("(1'(_,/ _'))") and
-  indSum :: "[Term \<Rightarrow> Term] \<Rightarrow> Term"
+  indSum :: "(Term \<Rightarrow> Term) \<Rightarrow> Term"
 where
   Sum_form: "\<And>(A::Term) (B::Term \<Rightarrow> Term). \<lbrakk>A : U; B: A \<rightarrow> U\<rbrakk> \<Longrightarrow> \<Sum>x:A. B(x) : U" and
 
@@ -97,9 +97,9 @@ where
     \<lbrakk>a : A; b : B(a)\<rbrakk> \<Longrightarrow> (a, b) : \<Sum>x:A. B(x)" and
 
   Sum_elim [elim]: "\<And>(A::Term) (B::Term \<Rightarrow> Term) (C::Term \<Rightarrow> Term) (f::Term) (p::Term).
-    \<lbrakk>C: \<Sum>x:A. B(x) \<rightarrow> U; f : \<Prod>x:A. \<Prod>y:B(x). C((x,y)); p : \<Sum>x:A. B(x)\<rbrakk> \<Longrightarrow> (indSum C)`f`p : C(p)" and
+    \<lbrakk>C: \<Sum>x:A. B(x) \<rightarrow> U; f : \<Prod>x:A. \<Prod>y:B(x). C((x,y)); p : \<Sum>x:A. B(x)\<rbrakk> \<Longrightarrow> indSum(C)`f`p : C(p)" and
 
-  Sum_comp [simp]: "\<And>(C::Term \<Rightarrow> Term) (f::Term) (a::Term) (b::Term). (indSum C)`f`(a,b) \<equiv> f`a`b"
+  Sum_comp [simp]: "\<And>(C::Term \<Rightarrow> Term) (f::Term) (a::Term) (b::Term). indSum(C)`f`(a,b) \<equiv> f`a`b"
 
 lemmas Sum_formation = Sum_form Sum_form[rotated]
 
@@ -118,16 +118,16 @@ overloading
   snd_nondep \<equiv> snd
 begin
 definition fst_dep :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term" where
-  "fst_dep A B \<equiv> (indSum (\<lambda>_. A))`(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). x)"
+  "fst_dep A B \<equiv> indSum(\<lambda>_. A)`(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). x)"
 
 definition snd_dep :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term" where
-  "snd_dep A B \<equiv> (indSum (\<lambda>_. A))`(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). y)"
+  "snd_dep A B \<equiv> indSum(\<lambda>_. A)`(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). y)"
 
 definition fst_nondep :: "[Term, Term] \<Rightarrow> Term" where
-  "fst_nondep A B \<equiv> (indSum (\<lambda>_. A))`(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. x)"
+  "fst_nondep A B \<equiv> indSum(\<lambda>_. A)`(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. x)"
 
 definition snd_nondep :: "[Term, Term] \<Rightarrow> Term" where
-  "snd_nondep A B \<equiv> (indSum (\<lambda>_. A))`(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. y)"
+  "snd_nondep A B \<equiv> indSum(\<lambda>_. A)`(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. y)"
 end
 
 lemma fst_dep_comp: "\<lbrakk>a : A; b : B(a)\<rbrakk> \<Longrightarrow> fst[A,B]`(a,b) \<equiv> a" unfolding fst_dep_def by simp
@@ -136,18 +136,32 @@ lemma snd_dep_comp: "\<lbrakk>a : A; b : B(a)\<rbrakk> \<Longrightarrow> snd[A,B
 lemma fst_nondep_comp: "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> fst[A,B]`(a,b) \<equiv> a" unfolding fst_nondep_def by simp
 lemma snd_nondep_comp: "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> snd[A,B]`(a,b) \<equiv> b" unfolding snd_nondep_def by simp
 
-\<comment> \<open>Simplification rules for Sum\<close>
+\<comment> \<open>Simplification rules for projections\<close>
 lemmas fst_snd_simps [simp] = fst_dep_comp snd_dep_comp fst_nondep_comp snd_nondep_comp
 
 subsubsection \<open>Equality type\<close>
 
 axiomatization
-  Equal :: "Term \<Rightarrow> Term \<Rightarrow> Term \<Rightarrow> Term"  ("(_ =_ _)") and
-  refl :: "Term \<Rightarrow> Term"                   ("(refl'(_'))")
+  Equal :: "[Term, Term, Term] \<Rightarrow> Term"
+syntax
+  "_EQUAL" :: "[Term, Term, Term] \<Rightarrow> Term"  ("(3_ =\<^sub>_/ _)")
+translations
+  "a =\<^sub>A b" \<rightleftharpoons> "CONST Equal A a b"
+
+axiomatization
+  refl :: "Term \<Rightarrow> Term" and
+  indEqual :: "([Term, Term, Term] \<Rightarrow> Term) \<Rightarrow> Term"
 where
-  Equal_form: "\<And>A a b. \<lbrakk>a : A; b : A\<rbrakk> \<Longrightarrow> a =A b : U" and
-  Equal_intro: "\<And>A x. x : A \<Longrightarrow> refl x : x =A x"
+  Equal_form: "\<And>A a b::Term. \<lbrakk>A : U; a : A; b : A\<rbrakk> \<Longrightarrow> a =\<^sub>A b : U" and
+  
+  Equal_intro [intro]: "\<And>A x::Term. x : A \<Longrightarrow> refl(x) : x =\<^sub>A x"
+
+(* and
+  
+  Equal_elim [elim]: "\<And>(C::[Term, Term, Term] \<Rightarrow> Term) (f::Term) (x::Term) (y::Term) (p::Term).
+    \<lbrakk>\<rbrakk> \<Longrightarrow> (indEqual C)`f`x`y`p  : C(x)(y)(p)"
 
+*)
 (*
 subsubsection \<open>Empty type\<close>
 
-- 
cgit v1.2.3