Organize this commit as a backup of the work on type inference done so far; learnt that I probably need to take a different approach. In particular, should first make the constants completely monomorphic, and then work on full proper type inference, rather than the heuristic approach taken here.

1 files changed, 24 insertions, 22 deletions

diff --git a/Projections.thy b/Projections.thy
index 509402b..c819240 100644
--- a/Projections.thy
+++ b/Projections.thy
@@ -1,43 +1,45 @@
-(*
-Title:  Projections.thy
-Author: Joshua Chen
-Date:   2018
+(********
+Isabelle/HoTT: Projections
+Feb 2019
 
-Projection functions \<open>fst\<close> and \<open>snd\<close> for the dependent sum type.
-*)
+Projection functions for the dependent sum type.
+
+********)
 
 theory Projections
 imports HoTT_Methods Prod Sum
 
 begin
 
-
-definition fst :: "t \<Rightarrow> t" where "fst p \<equiv> ind\<^sub>\<Sum> (\<lambda>x y. x) p"
-definition snd :: "t \<Rightarrow> t" where "snd p \<equiv> ind\<^sub>\<Sum> (\<lambda>x y. y) p"
+definition fst :: "[t, t] \<Rightarrow> t" where "fst A p \<equiv> indSum (\<lambda>_. A) (\<lambda>x y. x) p"
 
 lemma fst_type:
-  assumes "A: U i" and "B: A \<longrightarrow> U i" and "p: \<Sum>x:A. B x" shows "fst p: A"
+  assumes "A: U i" and "p: \<Sum>x: A. B x" shows "fst A p: A"
 unfolding fst_def by (derive lems: assms)
 
-lemma fst_comp:
-  assumes "A: U i" and "B: A \<longrightarrow> U i" and "a: A" and "b: B a" shows "fst <a,b> \<equiv> a"
+declare fst_type [intro]
+
+lemma fst_cmp:
+  assumes "A: U i" and "B: A \<leadsto> U i" and "a: A" and "b: B a" shows "fst A <a, b> \<equiv> a"
 unfolding fst_def by compute (derive lems: assms)
 
-lemma snd_type:
-  assumes "A: U i" and "B: A \<longrightarrow> U i" and "p: \<Sum>x:A. B x" shows "snd p: B (fst p)"
-unfolding snd_def proof (derive lems: assms)
-  show "\<And>p. p: \<Sum>x:A. B x \<Longrightarrow> fst p: A" using assms(1-2) by (rule fst_type)
+declare fst_cmp [comp]
 
-  fix x y assume asm: "x: A" "y: B x"
-  show "y: B (fst <x,y>)" by (derive lems: asm assms fst_comp)
+definition snd :: "[t, t \<Rightarrow> t, t] \<Rightarrow> t" where "snd A B p \<equiv> indSum (\<lambda>p. B (fst A p)) (\<lambda>x y. y) p"
+
+lemma snd_type:
+  assumes "A: U i" and "B: A \<leadsto> U i" and "p: \<Sum>x: A. B x" shows "snd A B p: B (fst A p)"
+unfolding snd_def proof (routine add: assms)
+  fix x y assume "x: A" and "y: B x"
+  with assms have [comp]: "fst A <x, y> \<equiv> x" by derive
+  note \<open>y: B x\<close> then show "y: B (fst A <x, y>)" by compute
 qed
 
-lemma snd_comp:
-  assumes "A: U i" and "B: A \<longrightarrow> U i" and "a: A" and "b: B a" shows "snd <a,b> \<equiv> b"
+lemma snd_cmp:
+  assumes "A: U i" and "B: A \<leadsto> U i" and "a: A" and "b: B a" shows "snd A B <a,b> \<equiv> b"
 unfolding snd_def by (derive lems: assms)
 
 lemmas Proj_types [intro] = fst_type snd_type
-lemmas Proj_comps [comp] = fst_comp snd_comp
-
+lemmas Proj_comps [comp] = fst_cmp snd_cmp
 
 end