diff options
author | Josh Chen | 2018-09-11 10:20:26 +0200 |
---|---|---|
committer | Josh Chen | 2018-09-11 10:20:26 +0200 |
commit | 637ee546f3eb9a927d83bd19ae0bee09031bd7d5 (patch) | |
tree | 23618624e90f2c84a3576ff528229b54d35d4981 | |
parent | 9b17aac85aa650a7a9d6463d3d01f1eb228d4572 (diff) |
Implementing univalence
-rw-r--r-- | EqualProps.thy | 5 | ||||
-rw-r--r-- | Prod.thy | 5 | ||||
-rw-r--r-- | Univalence.thy | 71 |
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 @@ -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 |