aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJosh Chen2018-09-19 15:06:44 +0200
committerJosh Chen2018-09-19 15:06:44 +0200
commit150f7eb27880a0081b8ec86d775dd626f507e779 (patch)
tree9fe01af79f4dc8ccc50339bf13628912fba5effa
parent1305c6beca2448156b61649da1a719d055aaf7f7 (diff)
Renaming
Diffstat (limited to '')
-rw-r--r--HoTT.thy4
-rw-r--r--Projections.thy43
-rw-r--r--Univalence.thy2
3 files changed, 46 insertions, 3 deletions
diff --git a/HoTT.thy b/HoTT.thy
index 38097b1..6c6ad21 100644
--- a/HoTT.thy
+++ b/HoTT.thy
@@ -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