diff options
| -rw-r--r-- | HoTT.thy | 4 | ||||
| -rw-r--r-- | Projections.thy | 43 | ||||
| -rw-r--r-- | Univalence.thy | 2 |
3 files changed, 46 insertions, 3 deletions
@@ -22,8 +22,8 @@ Sum Unit (* Derived definitions and properties *) -EqualProps -Proj +Equality +Projections Univalence begin diff --git a/Projections.thy b/Projections.thy new file mode 100644 index 0000000..509402b --- /dev/null +++ b/Projections.thy @@ -0,0 +1,43 @@ +(* +Title: Projections.thy +Author: Joshua Chen +Date: 2018 + +Projection functions \<open>fst\<close> and \<open>snd\<close> 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" + +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 diff --git a/Univalence.thy b/Univalence.thy index 3c9b520..c6733c6 100644 --- a/Univalence.thy +++ b/Univalence.thy @@ -7,7 +7,7 @@ Definitions of homotopy, equivalence and the univalence axiom. *) theory Univalence -imports HoTT_Methods EqualProps Prod Sum +imports HoTT_Methods Equality Prod Sum begin |