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_Theorems.thy | 77 ++++++++++++++++++++++++++++++++++++-------------------
 1 file changed, 50 insertions(+), 27 deletions(-)

(limited to 'HoTT_Theorems.thy')

diff --git a/HoTT_Theorems.thy b/HoTT_Theorems.thy
index a44c8f9..1ac4484 100644
--- a/HoTT_Theorems.thy
+++ b/HoTT_Theorems.thy
@@ -21,19 +21,19 @@ text "Declaring \<open>Prod_intro\<close> with the \<open>intro\<close> attribut
 lemma "\<^bold>\<lambda>x:A. x : A\<rightarrow>A" ..
 
 proposition "A \<equiv> B \<Longrightarrow> \<^bold>\<lambda>x:A. x : B\<rightarrow>A"
-  proof -
-    assume assm: "A \<equiv> B"
-    have id: "\<^bold>\<lambda>x:A. x : A\<rightarrow>A" ..
-    from assm have "A\<rightarrow>A \<equiv> B\<rightarrow>A" by simp
-    with id show "\<^bold>\<lambda>x:A. x : B\<rightarrow>A" ..
-  qed
+proof -
+  assume assm: "A \<equiv> B"
+  have id: "\<^bold>\<lambda>x:A. x : A\<rightarrow>A" ..
+  from assm have "A\<rightarrow>A \<equiv> B\<rightarrow>A" by simp
+  with id show "\<^bold>\<lambda>x:A. x : B\<rightarrow>A" ..
+qed
 
 proposition "\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. x : A\<rightarrow>B\<rightarrow>A"
-  proof
-    fix a
-    assume "a : A"
-    then show "\<^bold>\<lambda>y:B. a : B \<rightarrow> A" .. 
-  qed
+proof
+  fix a
+  assume "a : A"
+  then show "\<^bold>\<lambda>y:B. a : B \<rightarrow> A" .. 
+qed
 
 subsection \<open>Function application\<close>
 
@@ -61,9 +61,9 @@ proof (rule Prod_formation)
   fix x::Term
   assume *: "x : A"
   show "\<Prod>y:B(x). C x y : U"
-    proof (rule Prod_formation)
-      show "B(x) : U" using * by (rule assms)
-    qed (rule assms)
+  proof (rule Prod_formation)
+    show "B(x) : U" using * by (rule assms)
+  qed (rule assms)
 qed (rule assms)
 
 proposition triply_curried:
@@ -81,36 +81,59 @@ proposition triply_curried:
 proof (rule Prod_formation)
   fix x::Term assume 1: "x : A"
   show "\<Prod>y:B(x). \<Prod>z:C(x)(y). D(x)(y)(z) : U"
+  proof (rule Prod_formation)
+    show "B(x) : U" using 1 by (rule assms)
+    
+    fix y::Term assume 2: "y : B(x)"  
+    show "\<Prod>z:C(x)(y). D(x)(y)(z) : U"
     proof (rule Prod_formation)
-      show "B(x) : U" using 1 by (rule assms)
-      
-      fix y::Term assume 2: "y : B(x)"  
-      show "\<Prod>z:C(x)(y). D(x)(y)(z) : U"
-        proof (rule Prod_formation)
-          show "C x y : U" using 2 by (rule assms)
-          show "\<And>z::Term. z : C(x)(y) \<Longrightarrow> D(x)(y)(z) : U" by (rule assms)
-        qed
+      show "C x y : U" using 2 by (rule assms)
+      show "\<And>z::Term. z : C(x)(y) \<Longrightarrow> D(x)(y)(z) : U" by (rule assms)
     qed
+  qed
 qed (rule assms)
 
-lemma
+lemma curried_type:
   fixes
     a b A::Term and
     B::"Term \<Rightarrow> Term" and
     f C::"[Term, Term] \<Rightarrow> Term"
-  assumes "\<And>x y::Term. f x y : C x y"
+  assumes "\<And>x y::Term. \<lbrakk>x : A; y : B(x)\<rbrakk> \<Longrightarrow> f x y : C x y"
   shows "\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). f x y : \<Prod>x:A. \<Prod>y:B(x). C x y"
 proof
   fix x::Term
+  assume *: "x : A"
   show "\<^bold>\<lambda>y:B(x). f x y : \<Prod>y:B(x). C x y"
-    proof
-      show "\<And>y. f x y : C x y" by (rule assms)
-    qed
+  proof
+    fix y::Term
+    assume **: "y : B(x)"
+    show "f x y : C x y" using * ** by (rule assms)
+  qed
 qed
 
 text "Note that the propositions and proofs above often say nothing about the well-formedness of the types, or the well-typedness of the lambdas involved; one has to be very explicit and prove such things separately!
 This is the result of the choices made regarding the premises of the type rules."
 
+text "The following shows that the dependent sum inductor has the type we expect it to have:"
+
+lemma
+  assumes "C: \<Sum>x:A. B(x) \<rightarrow> U"
+  shows "indSum(C) : \<Prod>f:(\<Prod>x:A. \<Prod>y:B(x). C((x,y))). \<Prod>p:(\<Sum>x:A. B(x)). C(p)"
+proof -
+  define F and P where
+    "F \<equiv> \<Prod>x:A. \<Prod>y:B(x). C((x,y))" and
+    "P \<equiv> \<Sum>x:A. B(x)"
+
+  have "\<^bold>\<lambda>f:F. \<^bold>\<lambda>p:P. indSum(C)`f`p : \<Prod>f:F. \<Prod>p:P. C(p)"
+  proof (rule curried_type)
+    fix f p::Term
+    assume "f : F" and "p : P"
+    with assms show "indSum(C)`f`p : C(p)" unfolding F_def P_def ..
+  qed
+  
+  then show "indSum(C) : \<Prod>f:F. \<Prod>p:P. C(p)" by simp
+qed
+
 text "Polymorphic identity function."
 
 consts Ui::Term
-- 
cgit v1.2.3