diff options
Diffstat (limited to 'Univalence.thy')
| -rw-r--r-- | Univalence.thy | 37 |
1 files changed, 18 insertions, 19 deletions
diff --git a/Univalence.thy b/Univalence.thy index b7f4400..001ee33 100644 --- a/Univalence.thy +++ b/Univalence.thy @@ -1,32 +1,31 @@ (* Title: HoTT/Univalence.thy - Author: Josh Chen + Author: Joshua Chen Definitions of homotopy, equivalence and the univalence axiom. *) theory Univalence - imports - HoTT_Methods - EqualProps - ProdProps - Sum +imports + HoTT_Methods + EqualProps + ProdProps + Sum + begin section \<open>Homotopy and equivalence\<close> -text "We define polymorphic constants implementing the definitions of homotopy and equivalence." - -axiomatization homotopic :: "[Term, Term] \<Rightarrow> Term" (infix "~" 100) where +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 :: "Term \<Rightarrow> Term" where +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 :: "[Term, Term] \<Rightarrow> Term" (infix "\<simeq>" 100) +definition equivalence :: "[t, t] \<Rightarrow> t" (infix "\<simeq>" 100) where "A \<simeq> B \<equiv> \<Sum>f: A \<rightarrow> B. isequiv f" @@ -75,7 +74,7 @@ qed (rule assms) section \<open>idtoeqv and the univalence axiom\<close> -definition idtoeqv :: Term +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>" @@ -94,9 +93,9 @@ proof } show "transport p: A \<rightarrow> B" - proof (rule transport_type[where ?P="\<lambda>x. x" and ?A="U i" and ?i="S i"]) - show "\<And>x. x: U i \<Longrightarrow> x: U S i" by (elim U_cumulative) standard - show "U i: U S i" by (rule U_hierarchy) standard + 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)" @@ -112,8 +111,8 @@ proof (\<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 S i" by (rule U_hierarchy) standard - show "U i: U S i" by (rule U_hierarchy) standard + 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)" @@ -164,13 +163,13 @@ proof qed next - show "A =[U i] B: U (S i)" by (derive lems: assms | rule U_hierarchy)+ + 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 :: Term where +axiomatization univalence :: t where UA: "univalence: isequiv idtoeqv" |