diff options
author | Josh Chen | 2018-09-19 15:07:05 +0200 |
---|---|---|
committer | Josh Chen | 2018-09-19 15:07:05 +0200 |
commit | 24a0d9c9f72b54151f87332334f8ac488658351c (patch) | |
tree | f857ddd4128b582a7ab61b6e06bbc28a463d83f4 /Proj.thy | |
parent | 150f7eb27880a0081b8ec86d775dd626f507e779 (diff) |
Renaming
Diffstat (limited to 'Proj.thy')
-rw-r--r-- | Proj.thy | 43 |
1 files changed, 0 insertions, 43 deletions
diff --git a/Proj.thy b/Proj.thy deleted file mode 100644 index e76e8d3..0000000 --- a/Proj.thy +++ /dev/null @@ -1,43 +0,0 @@ -(* -Title: Proj.thy -Author: Joshua Chen -Date: 2018 - -Projection functions \<open>fst\<close> and \<open>snd\<close> for the dependent sum type. -*) - -theory Proj -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" - -lemma fst_type: - assumes "A: U i" and "B: A \<longrightarrow> U i" and "p: \<Sum>x:A. B x" shows "fst 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" -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) - - fix x y assume asm: "x: A" "y: B x" - show "y: B (fst <x,y>)" by (derive lems: asm assms fst_comp) -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" -unfolding snd_def by (derive lems: assms) - -lemmas Proj_types [intro] = fst_type snd_type -lemmas Proj_comps [comp] = fst_comp snd_comp - - -end |