aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--EqualProps.thy5
-rw-r--r--Prod.thy5
-rw-r--r--Univalence.thy71
3 files changed, 81 insertions, 0 deletions
diff --git a/EqualProps.thy b/EqualProps.thy
index 708eb33..f00020f 100644
--- a/EqualProps.thy
+++ b/EqualProps.thy
@@ -273,4 +273,9 @@ apply (rule assms)+
sorry
+section \<open>Transport\<close>
+
+
+
+
end
diff --git a/Prod.thy b/Prod.thy
index 35d6b07..a7968b6 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -81,4 +81,9 @@ syntax "_COMPOSE" :: "[Term, Term] \<Rightarrow> Term" (infixr "\<circ>" 110)
translations "g \<circ> f" \<rightleftharpoons> "g o f"
+section \<open>Polymorphic identity function\<close>
+
+abbreviation id :: Term where "id \<equiv> \<^bold>\<lambda>x. x"
+
+
end
diff --git a/Univalence.thy b/Univalence.thy
new file mode 100644
index 0000000..b999a55
--- /dev/null
+++ b/Univalence.thy
@@ -0,0 +1,71 @@
+(* Title: HoTT/Univalence.thy
+ Author: Josh Chen
+
+Definitions of homotopy, equivalence and the univalence axiom.
+*)
+
+theory Univalence
+ imports
+ HoTT_Methods
+ Equal
+ ProdProps
+ Sum
+begin
+
+
+section \<open>Homotopy and equivalence\<close>
+
+axiomatization homotopic :: "[Term, Term] \<Rightarrow> Term" (infix "~" 100) where
+ homotopic_def: "\<lbrakk>
+ f: \<Prod>x:A. B x;
+ g: \<Prod>x:A. B x
+ \<rbrakk> \<Longrightarrow> f ~ g \<equiv> \<Prod>x:A. (f`x) =[B x] (g`x)"
+
+axiomatization isequiv :: "Term \<Rightarrow> Term" where
+ isequiv_def: "f: A \<rightarrow> B \<Longrightarrow> isequiv f \<equiv> (\<Sum>g: A \<rightarrow> B. g \<circ> f ~ id) \<times> (\<Sum>g: A \<rightarrow> B. f \<circ> g ~ id)"
+
+definition equivalence :: "[Term, Term] \<Rightarrow> Term" (infix "\<simeq>" 100)
+ where "A \<simeq> B \<equiv> \<Sum>f: A \<rightarrow> B. isequiv f"
+
+
+text "The identity function is an equivalence:"
+
+lemma isequiv_id:
+ assumes "A: U i" and "id: A \<rightarrow> A"
+ shows "<<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>: isequiv id"
+proof (derive lems: assms isequiv_def homotopic_def)
+ fix g assume asm: "g: A \<rightarrow> A"
+ show "id \<circ> g: A \<rightarrow> A"
+ unfolding compose_def by (derive lems: asm assms)
+
+ show "\<Prod>x:A. ((id \<circ> g)`x) =\<^sub>A (id`x): U i"
+ unfolding compose_def by (derive lems: asm assms)
+
+ next
+ show "<\<^bold>\<lambda>x. x, \<^bold>\<lambda>x. refl x>: \<Sum>g:A \<rightarrow> A. (g \<circ> id) ~ id"
+ unfolding compose_def by (derive lems: assms homotopic_def)
+
+ show "<\<^bold>\<lambda>x. x, lambda refl>: \<Sum>g:A \<rightarrow> A. (id \<circ> g) ~ id"
+ unfolding compose_def by (derive lems: assms homotopic_def)
+qed (rule assms)
+
+
+text "The equivalence relation \<open>\<simeq>\<close> is symmetric:"
+
+lemma
+ assumes "A: U i" and "id: A \<rightarrow> A"
+ shows "<id, <<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>>: A \<simeq> A"
+unfolding equivalence_def proof
+ show "<<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>: isequiv id" using assms by (rule isequiv_id)
+
+ fix f assume asm: "f: A \<rightarrow> A" show "isequiv f: U i"
+ by (derive lems: asm assms homotopic_def isequiv_def compose_def)
+qed (rule assms)
+
+
+text "Definition of \<open>idtoeqv\<close>:"
+
+
+
+
+end