aboutsummaryrefslogtreecommitdiff
path: root/Univalence.thy
diff options
context:
space:
mode:
Diffstat (limited to 'Univalence.thy')
-rw-r--r--Univalence.thy176
1 files changed, 176 insertions, 0 deletions
diff --git a/Univalence.thy b/Univalence.thy
new file mode 100644
index 0000000..001ee33
--- /dev/null
+++ b/Univalence.thy
@@ -0,0 +1,176 @@
+(* Title: HoTT/Univalence.thy
+ Author: Joshua Chen
+
+Definitions of homotopy, equivalence and the univalence axiom.
+*)
+
+theory Univalence
+imports
+ HoTT_Methods
+ EqualProps
+ ProdProps
+ Sum
+
+begin
+
+
+section \<open>Homotopy and equivalence\<close>
+
+axiomatization homotopic :: "[t, t] \<Rightarrow> t" (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 :: "t \<Rightarrow> t" where
+ isequiv_def: "f: A \<rightarrow> B \<Longrightarrow> isequiv f \<equiv> (\<Sum>g: B \<rightarrow> A. g \<circ> f ~ id) \<times> (\<Sum>g: B \<rightarrow> A. f \<circ> g ~ id)"
+
+definition equivalence :: "[t, t] \<Rightarrow> t" (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 (routine lems: asm assms)
+
+ show "\<Prod>x:A. ((id \<circ> g)`x) =\<^sub>A (id`x): U i"
+ unfolding compose_def by (routine 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 "We use the following lemma in a few proofs:"
+
+lemma isequiv_type:
+ assumes "A: U i" and "B: U i" and "f: A \<rightarrow> B"
+ shows "isequiv f: U i"
+ by (derive lems: assms isequiv_def homotopic_def compose_def)
+
+
+text "The equivalence relation \<open>\<simeq>\<close> is symmetric:"
+
+lemma equiv_sym:
+ 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 "f: A \<rightarrow> A"
+ with assms(1) assms(1) show "isequiv f: U i" by (rule isequiv_type)
+qed (rule assms)
+
+
+section \<open>idtoeqv and the univalence axiom\<close>
+
+definition idtoeqv :: t
+ where "idtoeqv \<equiv> \<^bold>\<lambda>p. <transport p, ind\<^sub>= (\<lambda>A. <<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>) p>"
+
+
+text "We prove that equal types are equivalent. The proof is long and uses universes."
+
+theorem
+ assumes "A: U i" and "B: U i"
+ shows "idtoeqv: (A =[U i] B) \<rightarrow> A \<simeq> B"
+unfolding idtoeqv_def equivalence_def
+proof
+ fix p assume "p: A =[U i] B"
+ show "<transport p, ind\<^sub>= (\<lambda>A. <<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>) p>: \<Sum>f: A \<rightarrow> B. isequiv f"
+ proof
+ { fix f assume "f: A \<rightarrow> B"
+ with assms show "isequiv f: U i" by (rule isequiv_type)
+ }
+
+ show "transport p: A \<rightarrow> B"
+ proof (rule transport_type[where ?P="\<lambda>x. x" and ?A="U i" and ?i="Suc i"])
+ show "\<And>x. x: U i \<Longrightarrow> x: U (Suc i)" by cumulativity
+ show "U i: U (Suc i)" by hierarchy
+ qed fact+
+
+ show "ind\<^sub>= (\<lambda>A. <<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>) p: isequiv (transport p)"
+ proof (rule Equal_elim[where ?C="\<lambda>_ _ p. isequiv (transport p)"])
+ fix A assume asm: "A: U i"
+ show "<<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>: isequiv (transport (refl A))"
+ proof (derive lems: isequiv_def)
+ show "transport (refl A): A \<rightarrow> A"
+ unfolding transport_def
+ by (compute lems: Equal_comp[where ?A="U i" and ?C="\<lambda>_ _ _. A \<rightarrow> A"]) (derive lems: asm)
+
+ show "<<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>:
+ (\<Sum>g:A \<rightarrow> A. g \<circ> (transport (refl A)) ~ id) \<times>
+ (\<Sum>g:A \<rightarrow> A. (transport (refl A)) \<circ> g ~ id)"
+ proof (subst (1 2) transport_comp)
+ show "U i: U (Suc i)" by (rule U_hierarchy) rule
+ show "U i: U (Suc i)" by (rule U_hierarchy) rule
+
+ show "<<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>:
+ (\<Sum>g:A \<rightarrow> A. g \<circ> id ~ id) \<times> (\<Sum>g:A \<rightarrow> A. id \<circ> g ~ id)"
+ proof
+ show "\<Sum>g:A \<rightarrow> A. id \<circ> g ~ id: U i"
+ proof (derive lems: asm homotopic_def)
+ fix g assume asm': "g: A \<rightarrow> A"
+ show *: "id \<circ> g: A \<rightarrow> A" by (derive lems: asm asm' compose_def)
+ show "\<Prod>x:A. ((id \<circ> g)`x) =\<^sub>A (id`x): U i" by (derive lems: asm *)
+ qed (routine lems: asm)
+
+ show "<id, \<^bold>\<lambda>x. refl x>: \<Sum>g:A \<rightarrow> A. id \<circ> g ~ id"
+ proof
+ fix g assume asm': "g: A \<rightarrow> A"
+ show "id \<circ> g ~ id: U i"
+ proof (derive lems: homotopic_def)
+ show *: "id \<circ> g: A \<rightarrow> A" by (derive lems: asm asm' compose_def)
+ show "\<Prod>x:A. ((id \<circ> g)`x) =\<^sub>A (id`x): U i" by (derive lems: asm *)
+ qed (routine lems: asm)
+ next
+ show "\<^bold>\<lambda>x. refl x: id \<circ> id ~ id"
+ proof compute
+ show "\<^bold>\<lambda>x. refl x: id ~ id" by (subst homotopic_def) (derive lems: asm)
+ qed (rule asm)
+ qed (routine lems: asm)
+
+ show "<id, \<^bold>\<lambda>x. refl x>: \<Sum>g:A \<rightarrow> A. g \<circ> id ~ id"
+ proof
+ fix g assume asm': "g: A \<rightarrow> A"
+ show "g \<circ> id ~ id: U i" by (derive lems: asm asm' homotopic_def compose_def)
+ next
+ show "\<^bold>\<lambda>x. refl x: id \<circ> id ~ id"
+ proof compute
+ show "\<^bold>\<lambda>x. refl x: id ~ id" by (subst homotopic_def) (derive lems: asm)
+ qed (rule asm)
+ qed (routine lems: asm)
+ qed
+ qed fact+
+ qed
+ next
+
+ fix A' B' p' assume asm: "A': U i" "B': U i" "p': A' =[U i] B'"
+ show "isequiv (transport p'): U i"
+ proof (rule isequiv_type)
+ show "transport p': A' \<rightarrow> B'" by (derive lems: asm transport_def)
+ qed fact+
+ qed fact+
+ qed
+ next
+
+ show "A =[U i] B: U (Suc i)" proof (derive lems: assms, (rule U_hierarchy, rule lt_Suc)?)+
+qed
+
+
+text "The univalence axiom."
+
+axiomatization univalence :: t where
+ UA: "univalence: isequiv idtoeqv"
+
+
+end
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-28 15:14:05 +0000