diff options
| -rw-r--r-- | EqualProps.thy | 15 | ||||
| -rw-r--r-- | HoTT_Base.thy | 16 | ||||
| -rw-r--r-- | Univalence.thy | 66 |
3 files changed, 80 insertions, 17 deletions
diff --git a/EqualProps.thy b/EqualProps.thy index f00020f..0107e8e 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -275,7 +275,22 @@ sorry section \<open>Transport\<close> +definition transport :: "Term \<Rightarrow> Term" where + "transport p \<equiv> ind\<^sub>= (\<lambda>x. (\<^bold>\<lambda>x. x)) p" +lemma transport_type: + assumes + "A: U i" "P: A \<longrightarrow> U i" + "x: A" "y: A" + "p: x =\<^sub>A y" + shows "transport p: P x \<rightarrow> P y" +unfolding transport_def +by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (routine lems: assms) + +lemma transport_comp: + assumes "A: U i" and "x: A" + shows "transport (refl x) \<equiv> id" +unfolding transport_def by (derive lems: assms) end diff --git a/HoTT_Base.thy b/HoTT_Base.thy index a5b88fd..916f6aa 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -32,19 +32,23 @@ typedecl Ord axiomatization O :: Ord and - S :: "Ord \<Rightarrow> Ord" ("S_" [0] 1000) and + S :: "Ord \<Rightarrow> Ord" ("S _" [0] 1000) and lt :: "[Ord, Ord] \<Rightarrow> prop" (infix "<" 999) and leq :: "[Ord, Ord] \<Rightarrow> prop" (infix "\<le>" 999) where - Ord_lt_min: "\<And>n. O < S n" + lt_min: "\<And>n. O < S n" and - Ord_lt_monotone: "\<And>m n. m < n \<Longrightarrow> S m < S n" + lt_monotone1: "\<And>n. n < S n" and - Ord_leq_min: "\<And>n. O \<le> n" + lt_monotone2: "\<And>m n. m < n \<Longrightarrow> S m < S n" and - Ord_leq_monotone: "\<And>m n. m \<le> n \<Longrightarrow> S m \<le> S n" + leq_min: "\<And>n. O \<le> n" +and + leq_monotone1: "\<And>n. n \<le> S n" +and + leq_monotone2: "\<And>m n. m \<le> n \<Longrightarrow> S m \<le> S n" -lemmas Ord_rules [intro] = Ord_lt_min Ord_lt_monotone Ord_leq_min Ord_leq_monotone +lemmas Ord_rules [intro] = lt_min lt_monotone1 lt_monotone2 leq_min leq_monotone1 leq_monotone2 \<comment> \<open>Enables \<open>standard\<close> to automatically solve inequalities.\<close> text "Define the universe types." diff --git a/Univalence.thy b/Univalence.thy index b999a55..e16ea03 100644 --- a/Univalence.thy +++ b/Univalence.thy @@ -7,7 +7,7 @@ Definitions of homotopy, equivalence and the univalence axiom. theory Univalence imports HoTT_Methods - Equal + EqualProps ProdProps Sum begin @@ -22,7 +22,7 @@ axiomatization homotopic :: "[Term, Term] \<Rightarrow> Term" (infix "~" 100) w \<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)" + 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) where "A \<simeq> B \<equiv> \<Sum>f: A \<rightarrow> B. isequiv f" @@ -36,12 +36,12 @@ lemma 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) + 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 (derive lems: asm assms) - + 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) @@ -50,22 +50,66 @@ proof (derive lems: assms isequiv_def 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 +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 asm: "f: A \<rightarrow> A" show "isequiv f: U i" - by (derive lems: asm assms homotopic_def isequiv_def compose_def) + fix f assume "f: A \<rightarrow> A" + with assms(1) assms(1) show "isequiv f: U i" by (rule isequiv_type) qed (rule assms) -text "Definition of \<open>idtoeqv\<close>:" - - +section \<open>idtoeqv and the univalence axiom\<close> + +definition idtoeqv :: Term + 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 "Equal types are equivalent. The proof 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="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 + 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 (derive lems: asm homotopic_def transport_def) + show "id: A \<rightarrow> A" by (routine lems: asm) end |