diff options
Diffstat (limited to '')
| -rw-r--r-- | Equal.thy | 10 | ||||
| -rw-r--r-- | EqualProps.thy | 398 | ||||
| -rw-r--r-- | HoTT_Base.thy | 4 | ||||
| -rw-r--r-- | HoTT_Methods.thy | 18 | ||||
| -rw-r--r-- | Prod.thy | 5 | ||||
| -rw-r--r-- | Univalence.thy | 194 |
6 files changed, 158 insertions, 471 deletions
@@ -7,7 +7,7 @@ Equality type *) theory Equal -imports HoTT_Base HoTT_Methods +imports HoTT_Base begin @@ -36,13 +36,13 @@ axiomatization where p: x =\<^sub>A y; x: A; y: A; - \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U i; - \<And>x. x: A \<Longrightarrow> f x: C x x (refl x) \<rbrakk> \<Longrightarrow> ind\<^sub>= (\<lambda>x. f x) p : C x y p" and + \<And>x. x: A \<Longrightarrow> f x: C x x (refl x); + \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U i \<rbrakk> \<Longrightarrow> ind\<^sub>= (\<lambda>x. f x) p : C x y p" and Equal_comp: "\<lbrakk> a: A; - \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U i; - \<And>x. x: A \<Longrightarrow> f x: C x x (refl x) \<rbrakk> \<Longrightarrow> ind\<^sub>= (\<lambda>x. f x) (refl a) \<equiv> f a" + \<And>x. x: A \<Longrightarrow> f x: C x x (refl x); + \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U i \<rbrakk> \<Longrightarrow> ind\<^sub>= (\<lambda>x. f x) (refl a) \<equiv> f a" lemmas Equal_routine [intro] = Equal_form Equal_intro Equal_elim lemmas Equal_comp [comp] diff --git a/EqualProps.thy b/EqualProps.thy index 19c788c..abb2623 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -1,361 +1,137 @@ -(* Title: HoTT/EqualProps.thy - Author: Josh Chen +(* +Title: EqualProps.thy +Author: Joshua Chen +Date: 2018 Properties of equality *) theory EqualProps - imports - HoTT_Methods - Equal - Prod +imports HoTT_Methods Equal Prod + begin -section \<open>Symmetry / Path inverse\<close> - -definition inv :: "t \<Rightarrow> t" ("_\<inverse>" [1000] 1000) where "p\<inverse> \<equiv> ind\<^sub>= (\<lambda>x. (refl x)) p" - -text " - In the proof below we begin by using path induction on \<open>p\<close> with the application of \<open>rule Equal_elim\<close>, telling Isabelle the specific substitutions to use. - The proof is finished with a standard application of the relevant type rules. -" - -lemma inv_type: - assumes "A : U i" and "x : A" and "y : A" and "p: x =\<^sub>A y" shows "p\<inverse>: y =\<^sub>A x" -unfolding inv_def -by (rule Equal_elim[where ?x=x and ?y=y]) (routine lems: assms) - \<comment> \<open>The type doesn't depend on \<open>p\<close> so we don't need to specify \<open>?p\<close> in the \<open>where\<close> clause above.\<close> - -text " - The next proof requires explicitly telling Isabelle what to substitute on the RHS of the typing judgment after the initial application of the type rules. - (If viewing this inside Isabelle, place the cursor after the \<open>proof\<close> statement and observe the second subgoal.) -" - -lemma inv_comp: - assumes "A : U i " and "a : A" shows "(refl a)\<inverse> \<equiv> refl a" -unfolding inv_def -proof compute - show "\<And>x. x: A \<Longrightarrow> refl x: x =\<^sub>A x" .. -qed (routine lems: assms) - - -section \<open>Transitivity / Path composition\<close> - -text " - Raw composition function, of type \<open>\<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)\<close> polymorphic over the type \<open>A\<close>. -" - -definition rpathcomp :: t where "rpathcomp \<equiv> \<^bold>\<lambda>_ _ p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>_ q. ind\<^sub>= (\<lambda>x. (refl x)) q) p" - -text " - More complicated proofs---the nested path inductions require more explicit step-by-step rule applications: -" - -lemma rpathcomp_type: - assumes "A: U i" - shows "rpathcomp: \<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)" -unfolding rpathcomp_def -proof - fix x assume 1: "x: A" - show "\<^bold>\<lambda>y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)" - proof - fix y assume 2: "y: A" - show "\<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)" - proof - fix p assume 3: "p: x =\<^sub>A y" - show "ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z" - proof (rule Equal_elim[where ?x=x and ?y=y]) - show "\<And>u. u: A \<Longrightarrow> \<^bold>\<lambda>z q. ind\<^sub>= refl q: \<Prod>z:A. u =\<^sub>A z \<rightarrow> u =\<^sub>A z" - proof - show "\<And>u z. \<lbrakk>u: A; z: A\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>q. ind\<^sub>= refl q: u =\<^sub>A z \<rightarrow> u =\<^sub>A z" - proof - fix u z q assume asm: "u: A" "z: A" "q: u =\<^sub>A z" - show "ind\<^sub>= refl q: u =\<^sub>A z" - by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms asm) - qed (routine lems: assms) - qed (rule assms) - qed (routine lems: assms 1 2 3) - qed (routine lems: assms 1 2) - qed (rule assms) -qed fact - -corollary - assumes "A: U i" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" - shows "rpathcomp`x`y`p`z`q: x =\<^sub>A z" - by (routine lems: assms rpathcomp_type) - -text " - The following proof is very long, chiefly because for every application of \<open>`\<close> we have to show the wellformedness of the type family appearing in the equality computation rule. -" - -lemma rpathcomp_comp: - assumes "A: U i" and "a: A" - shows "rpathcomp`a`a`(refl a)`a`(refl a) \<equiv> refl a" -unfolding rpathcomp_def -proof compute - fix x assume 1: "x: A" - show "\<^bold>\<lambda>y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)" - proof - fix y assume 2: "y: A" - show "\<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)" - proof - fix p assume 3: "p: x =\<^sub>A y" - show "ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z" - proof (rule Equal_elim[where ?x=x and ?y=y]) - show "\<And>u. u: A \<Longrightarrow> \<^bold>\<lambda>z q. ind\<^sub>= refl q: \<Prod>z:A. u =\<^sub>A z \<rightarrow> u =\<^sub>A z" - proof - show "\<And>u z. \<lbrakk>u: A; z: A\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>q. ind\<^sub>= refl q: u =\<^sub>A z \<rightarrow> u =\<^sub>A z" - proof - fix u z assume asm: "u: A" "z: A" - show "\<And>q. q: u =\<^sub>A z \<Longrightarrow> ind\<^sub>= refl q: u =\<^sub>A z" - by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms asm) - qed (routine lems: assms) - qed (rule assms) - qed (routine lems: assms 1 2 3) - qed (routine lems: assms 1 2) - qed (rule assms) - - next show "(\<^bold>\<lambda>y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p)`a`(refl a)`a`(refl a) \<equiv> refl a" - proof compute - fix y assume 1: "y: A" - show "\<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: a =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> a =\<^sub>A z)" - proof - fix p assume 2: "p: a =\<^sub>A y" - show "ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>z:A. y =\<^sub>A z \<rightarrow> a =\<^sub>A z" - proof (rule Equal_elim[where ?x=a and ?y=y]) - fix u assume 3: "u: A" - show "\<^bold>\<lambda>z q. ind\<^sub>= refl q: \<Prod>z:A. u =\<^sub>A z \<rightarrow> u =\<^sub>A z" - proof - fix z assume 4: "z: A" - show "\<^bold>\<lambda>q. ind\<^sub>= refl q: u =\<^sub>A z \<rightarrow> u =\<^sub>A z" - proof - show "\<And>q. q: u =\<^sub>A z \<Longrightarrow> ind\<^sub>= refl q: u =\<^sub>A z" - by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms 3 4) - qed (routine lems: assms 3 4) - qed fact - qed (routine lems: assms 1 2) - qed (routine lems: assms 1) - - next show "(\<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z. \<^bold>\<lambda>q. ind\<^sub>= refl q) p)`(refl a)`a`(refl a) \<equiv> refl a" - proof compute - fix p assume 1: "p: a =\<^sub>A a" - show "ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>z:A. a =\<^sub>A z \<rightarrow> a =\<^sub>A z" - proof (rule Equal_elim[where ?x=a and ?y=a]) - fix u assume 2: "u: A" - show "\<^bold>\<lambda>z q. ind\<^sub>= refl q: \<Prod>z:A. u =\<^sub>A z \<rightarrow> u =\<^sub>A z" - proof - fix z assume 3: "z: A" - show "\<^bold>\<lambda>q. ind\<^sub>= refl q: u =\<^sub>A z \<rightarrow> u =\<^sub>A z" - proof - show "\<And>q. q: u =\<^sub>A z \<Longrightarrow> ind\<^sub>= refl q: u =\<^sub>A z" - by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms 2 3) - qed (routine lems: assms 2 3) - qed fact - qed (routine lems: assms 1) - - next show "(ind\<^sub>=(\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q)(refl a))`a`(refl a) \<equiv> refl a" - proof compute - fix u assume 1: "u: A" - show "\<^bold>\<lambda>z q. ind\<^sub>= refl q: \<Prod>z:A. u =\<^sub>A z \<rightarrow> u =\<^sub>A z" - proof - fix z assume 2: "z: A" - show "\<^bold>\<lambda>q. ind\<^sub>= refl q: u =\<^sub>A z \<rightarrow> u =\<^sub>A z" - proof - show "\<And>q. q: u =\<^sub>A z \<Longrightarrow> ind\<^sub>= refl q: u =\<^sub>A z" - by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms 1 2) - qed (routine lems: assms 1 2) - qed fact - - next show "(\<^bold>\<lambda>z q. ind\<^sub>= refl q)`a`(refl a) \<equiv> refl a" - proof compute - fix a assume 1: "a: A" - show "\<^bold>\<lambda>q. ind\<^sub>= refl q: a =\<^sub>A a \<rightarrow> a =\<^sub>A a" - proof - show "\<And>q. q: a =\<^sub>A a \<Longrightarrow> ind\<^sub>= refl q: a =\<^sub>A a" - by (rule Equal_elim[where ?x=a and ?y=a]) (routine lems: assms 1) - qed (routine lems: assms 1) - - next show "(\<^bold>\<lambda>q. ind\<^sub>= refl q)`(refl a) \<equiv> refl a" - proof compute - show "\<And>p. p: a =\<^sub>A a \<Longrightarrow> ind\<^sub>= refl p: a =\<^sub>A a" - by (rule Equal_elim[where ?x=a and ?y=a]) (routine lems: assms) - show "ind\<^sub>= refl (refl a) \<equiv> refl a" - proof compute - show "\<And>x. x: A \<Longrightarrow> refl(x): x =\<^sub>A x" .. - qed (routine lems: assms) - qed (routine lems: assms) - qed fact - qed (routine lems: assms) - qed (routine lems: assms) - qed fact -qed fact - - -text "The raw object lambda term is cumbersome to use, so we define a simpler constant instead." - -axiomatization pathcomp :: "[t, t] \<Rightarrow> t" (infixl "\<bullet>" 120) where - pathcomp_def: "\<lbrakk> - A: U i; - x: A; y: A; z: A; - p: x =\<^sub>A y; q: y =\<^sub>A z - \<rbrakk> \<Longrightarrow> p \<bullet> q \<equiv> rpathcomp`x`y`p`z`q" +section \<open>Symmetry of equality/Path inverse\<close> +definition inv :: "t \<Rightarrow> t" ("_\<inverse>" [1000] 1000) where "p\<inverse> \<equiv> ind\<^sub>= (\<lambda>x. refl x) p" -lemma pathcomp_type: - assumes "A: U i" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" - shows "p \<bullet> q: x =\<^sub>A z" +lemma inv_type: "\<lbrakk>A: U i; x: A; y: A; p: x =\<^sub>A y\<rbrakk> \<Longrightarrow> p\<inverse>: y =\<^sub>A x" +unfolding inv_def by (elim Equal_elim) routine -proof (subst pathcomp_def) - show "A: U i" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" by fact+ -qed (routine lems: assms rpathcomp_type) +lemma inv_comp: "\<lbrakk>A: U i; a: A\<rbrakk> \<Longrightarrow> (refl a)\<inverse> \<equiv> refl a" +unfolding inv_def by compute routine -lemma pathcomp_comp: - assumes "A : U i" and "a : A" shows "(refl a) \<bullet> (refl a) \<equiv> refl a" -by (subst pathcomp_def) (routine lems: assms rpathcomp_comp) +section \<open>Transitivity of equality/Path composition\<close> +text \<open> +Composition function, of type @{term "x =\<^sub>A y \<rightarrow> (y =\<^sub>A z) \<rightarrow> (x =\<^sub>A z)"} polymorphic over @{term A}, @{term x}, @{term y}, and @{term z}. +\<close> -lemmas inv_type [intro] -lemmas pathcomp_type [intro] +definition pathcomp :: t where "pathcomp \<equiv> \<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>q. ind\<^sub>= (\<lambda>x. (refl x)) q) p" -lemmas inv_comp [comp] -lemmas pathcomp_comp [comp] +syntax "_pathcomp" :: "[t, t] \<Rightarrow> t" (infixl "\<bullet>" 120) +translations "p \<bullet> q" \<rightleftharpoons> "CONST pathcomp`p`q" +lemma pathcomp_type: + assumes "A: U i" and "x: A" "y: A" "z: A" + shows "pathcomp: x =\<^sub>A y \<rightarrow> (y =\<^sub>A z) \<rightarrow> (x =\<^sub>A z)" +unfolding pathcomp_def by rule (elim Equal_elim, routine add: assms) -section \<open>Weak higher groupoid structure of types\<close> +corollary pathcomp_trans: + assumes "A: U i" and "x: A" "y: A" "z: A" and "p: x =\<^sub>A y" "q: y =\<^sub>A z" + shows "p \<bullet> q: x =\<^sub>A z" +by (routine add: assms pathcomp_type) -schematic_goal whg1a: +lemma pathcomp_comp: + assumes "A: U i" and "a: A" + shows "(refl a) \<bullet> (refl a) \<equiv> refl a" +unfolding pathcomp_def proof compute + show "(ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>q. ind\<^sub>= (\<lambda>x. refl x) q) (refl a))`(refl a) \<equiv> refl a" + proof compute + show "\<^bold>\<lambda>q. (ind\<^sub>= (\<lambda>x. refl x) q): a =\<^sub>A a \<rightarrow> a =\<^sub>A a" + by (routine add: assms) + + show "(\<^bold>\<lambda>q. (ind\<^sub>= (\<lambda>x. refl x) q))`(refl a) \<equiv> refl a" + proof compute + show "\<And>q. q: a =\<^sub>A a \<Longrightarrow> ind\<^sub>= (\<lambda>x. refl x) q: a =\<^sub>A a" by (routine add: assms) + qed (derive lems: assms) + qed (routine add: assms) + + show "\<And>p. p: a =\<^sub>A a \<Longrightarrow> ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>q. ind\<^sub>= (\<lambda>x. refl x) q) p: a =\<^sub>A a \<rightarrow> a =\<^sub>A a" + by (routine add: assms) +qed (routine add: assms) + + +section \<open>Higher groupoid structure of types\<close> + +schematic_goal pathcomp_right_id: assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y" - shows "?a: p =[x =\<^sub>A y] (p \<bullet> (refl(y)))" -proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p]) - show "\<And>x. x: A \<Longrightarrow> refl(refl(x)): refl(x) =[x =\<^sub>A x] (refl(x) \<bullet> refl(x))" - by compute (routine lems: assms) -qed (routine lems: assms) + shows "?a: p \<bullet> (refl y) =[x =\<^sub>A y] p" +proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p]) \<comment> \<open>@{method elim} does not seem to work with schematic goals.\<close> + show "\<And>x. x: A \<Longrightarrow> refl(refl x): (refl x) \<bullet> (refl x) =[x =\<^sub>A x] (refl x)" + by (derive lems: assms pathcomp_comp) +qed (routine add: assms pathcomp_type) -schematic_goal whg1b: +schematic_goal pathcomp_left_id: assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y" - shows "?a: p =[x =\<^sub>A y] (refl(x) \<bullet> p)" + shows "?a: (refl x) \<bullet> p =[x =\<^sub>A y] p" proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p]) - show "\<And>x. x: A \<Longrightarrow> refl(refl(x)): refl(x) =[x =\<^sub>A x] (refl(x) \<bullet> refl(x))" - by compute (routine lems: assms) -qed (routine lems: assms) + show "\<And>x. x: A \<Longrightarrow> refl(refl x): (refl x) \<bullet> (refl x) =[x =\<^sub>A x] (refl x)" + by (derive lems: assms pathcomp_comp) +qed (routine add: assms pathcomp_type) -schematic_goal whg2a: +schematic_goal pathcomp_left_inv: assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y" shows "?a: (p\<inverse> \<bullet> p) =[y =\<^sub>A y] refl(y)" proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p]) - show "\<And>x. x: A \<Longrightarrow> refl(refl(x)): ((refl(x))\<inverse> \<bullet> refl(x)) =[x =\<^sub>A x] refl(x)" - by (compute | routine lems: assms)+ -qed (routine lems: assms)+ + show "\<And>x. x: A \<Longrightarrow> refl(refl x): (refl x)\<inverse> \<bullet> (refl x) =[x =\<^sub>A x] (refl x)" + by (derive lems: assms inv_comp pathcomp_comp) +qed (routine add: assms inv_type pathcomp_type) -schematic_goal whg2b: +schematic_goal pathcomp_right_inv: assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y" shows "?a: (p \<bullet> p\<inverse>) =[x =\<^sub>A x] refl(x)" proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p]) - show "\<And>x. x: A \<Longrightarrow> refl(refl(x)): (refl(x) \<bullet> (refl(x))\<inverse>) =[x =\<^sub>A x] refl(x)" - by (compute | routine lems: assms)+ -qed (routine lems: assms)+ + show "\<And>x. x: A \<Longrightarrow> refl(refl x): (refl x) \<bullet> (refl x)\<inverse> =[x =\<^sub>A x] (refl x)" + by (derive lems: assms inv_comp pathcomp_comp) +qed (routine add: assms inv_type pathcomp_type) -schematic_goal whg3: +schematic_goal inv_involutive: assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y" shows "?a: p\<inverse>\<inverse> =[x =\<^sub>A y] p" proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p]) - show "\<And>x. x: A \<Longrightarrow> refl(refl(x)): (refl(x))\<inverse>\<inverse> =[x =\<^sub>A x] refl(x)" - by (compute | routine lems: assms)+ -qed (routine lems: assms) - - -lemma assumes "A: U(i)" shows "\<And>x. x: A \<Longrightarrow> refl(x): x =\<^sub>A x" -by (rule Prod_atomize[where ?A=A and ?B="\<lambda>x. x =\<^sub>A x"]) (routine lems: assms) - + show "\<And>x. x: A \<Longrightarrow> refl(refl x): (refl x)\<inverse>\<inverse> =[x =\<^sub>A x] (refl x)" + by (derive lems: assms inv_comp) +qed (routine add: assms inv_type) -schematic_goal +schematic_goal pathcomp_assoc: assumes - "A: U(i)" and - "x: A" "y: A" "z: A" "w: A" and + "A: U(i)" + "x: A" "y: A" "z: A" "w: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" "r: z =\<^sub>A w" shows "?a: p \<bullet> (q \<bullet> r) =[x =\<^sub>A w] (p \<bullet> q) \<bullet> r" proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p]) - fix y assume "y: A" - show "refl(q \<bullet> r): refl(y) \<bullet> (q \<bullet> r) =[y =\<^sub>A w] (refl(y) \<bullet> q) \<bullet> r" - proof (compute lems: whg1b) - - -section \<open>Higher groupoid structure of types\<close> - -lemma - assumes "A: U i" "x: A" "y: A" "p: x =\<^sub>A y" - shows - "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p =[x =\<^sub>A y] p \<bullet> (refl y)" and - "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p =[x =\<^sub>A y] (refl x) \<bullet> p" - -proof - - show "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p =[x =[A] y] p \<bullet> (refl y)" - by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (derive lems: assms)+ - - show "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p =[x =[A] y] (refl x) \<bullet> p" - by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (derive lems: assms)+ -qed - - -lemma - assumes "A: U i" "x: A" "y: A" "p: x =\<^sub>A y" - shows - "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p\<inverse> \<bullet> p =[y =\<^sub>A y] (refl y)" and - "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p \<bullet> p\<inverse> =[x =\<^sub>A x] (refl x)" - -proof - - show "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p\<inverse> \<bullet> p =[y =\<^sub>A y] (refl y)" - by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (derive lems: assms)+ - - show "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p \<bullet> p\<inverse> =[x =\<^sub>A x] (refl x)" - by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (derive lems: assms)+ -qed - - -lemma - assumes "A: U i" "x: A" "y: A" "p: x =\<^sub>A y" - shows "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p\<inverse>\<inverse> =[x =\<^sub>A y] p" -by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (derive lems: assms) - -text "Next we construct a proof term of associativity of path composition." - -schematic_goal - assumes - "A: U i" - "x: A" "y: A" "z: A" "w: A" - "p: x =\<^sub>A y" "q: y =\<^sub>A z" "r: z =\<^sub>A w" - shows - "?a: p \<bullet> (q \<bullet> r) =[x =\<^sub>A z] (p \<bullet> q) \<bullet> r" - -apply (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) -apply (rule assms)+ -\<comment> \<open>Continue by substituting \<open>refl x \<bullet> q = q\<close> etc.\<close> -sorry + fix x assume "x: A" + show "refl (q \<bullet> r): (refl x) \<bullet> (q \<bullet> r) =[x =\<^sub>A w] ((refl x) \<bullet> q) \<bullet> r" + \<comment> \<open>This requires substitution of *propositional* equality. \<close> + sorry + oops section \<open>Transport\<close> -definition transport :: "t \<Rightarrow> t" where - "transport p \<equiv> ind\<^sub>= (\<lambda>x. (\<^bold>\<lambda>x. x)) p" +definition transport :: "t \<Rightarrow> t" where "transport p \<equiv> ind\<^sub>= (\<lambda>_. (\<^bold>\<lambda>x. x)) p" -text "Note that \<open>transport\<close> is a polymorphic function in our formulation." +text \<open>Note that @{term transport} is a polymorphic function in our formulation.\<close> -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) +lemma transport_type: "\<lbrakk>p: x =\<^sub>A y; x: A; y: A; A: U i; P: A \<longrightarrow> U i\<rbrakk> \<Longrightarrow> transport p: P x \<rightarrow> P y" +unfolding transport_def by (elim Equal_elim) routine + +lemma transport_comp: "\<lbrakk>A: U i; x: A\<rbrakk> \<Longrightarrow> transport (refl x) \<equiv> id" +unfolding transport_def by derive end diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 17e3142..7453883 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -7,9 +7,7 @@ Basic setup of a homotopy type theory object logic with a cumulative Russell-sty *) theory HoTT_Base -imports - Pure - "HOL-Eisbach.Eisbach" +imports Pure "HOL-Eisbach.Eisbach" begin diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index 411176e..8929f69 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -3,14 +3,11 @@ Title: HoTT_Methods.thy Author: Joshua Chen Date: 2018 -Method setup for the HoTT logic. Relies heavily on Eisbach. +Method setup for the HoTT logic. *) theory HoTT_Methods -imports - "HOL-Eisbach.Eisbach" - "HOL-Eisbach.Eisbach_Tools" - HoTT_Base +imports HoTT_Base "HOL-Eisbach.Eisbach" "HOL-Eisbach.Eisbach_Tools" begin @@ -43,16 +40,19 @@ Premises of the rule(s) applied are added as new subgoals. section \<open>Derivation search\<close> -text \<open>Combine @{method routine} and @{method compute} to search for derivations of judgments.\<close> +text \<open> +Combine @{method routine} and @{method compute} to search for derivations of judgments. +Also handle universes using methods @{method hierarchy} and @{method cumulativity} defined in @{file HoTT_Base.thy}. +\<close> -method derive uses lems = (routine add: lems | compute comp: lems)+ +method derive uses lems = (routine add: lems | compute comp: lems | cumulativity | hierarchy)+ section \<open>Induction\<close> text \<open> - Placeholder section for the automation of induction, i.e. using the elimination rules. - At the moment one must directly apply them with \<open>rule X_elim\<close>. +Placeholder section for the automation of induction, i.e. using the elimination rules. +At the moment one must directly apply them with \<open>rule X_elim\<close>. \<close> @@ -17,7 +17,7 @@ section \<open>Basic definitions\<close> axiomatization Prod :: "[t, tf] \<Rightarrow> t" and lambda :: "(t \<Rightarrow> t) \<Rightarrow> t" (binder "\<^bold>\<lambda>" 30) and - appl :: "[t, t] \<Rightarrow> t" ("(1_`/_)" [60, 61] 60) \<comment> \<open>Application binds tighter than abstraction.\<close> + appl :: "[t, t] \<Rightarrow> t" ("(1_`/_)" [105, 106] 105) \<comment> \<open>Application binds tighter than abstraction.\<close> syntax "_prod" :: "[idt, t, t] \<Rightarrow> t" ("(3\<Prod>_:_./ _)" 30) @@ -43,7 +43,7 @@ axiomatization where Prod_elim: "\<lbrakk>f: \<Prod>x:A. B x; a: A\<rbrakk> \<Longrightarrow> f`a: B a" and - Prod_comp: "\<lbrakk>\<And>x. x: A \<Longrightarrow> b x: B x; a: A\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x. b x)`a \<equiv> b a" and + Prod_comp: "\<lbrakk>a: A; \<And>x. x: A \<Longrightarrow> b x: B x\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x. b x)`a \<equiv> b a" and Prod_uniq: "f: \<Prod>x:A. B x \<Longrightarrow> \<^bold>\<lambda>x. f`x \<equiv> f" and @@ -68,6 +68,7 @@ lemmas Prod_comps [comp] = Prod_comp Prod_uniq section \<open>Additional definitions\<close> definition compose :: "[t, t] \<Rightarrow> t" (infixr "o" 110) where "g o f \<equiv> \<^bold>\<lambda>x. g`(f`x)" + syntax "_compose" :: "[t, t] \<Rightarrow> t" (infixr "\<circ>" 110) translations "g \<circ> f" \<rightleftharpoons> "g o f" diff --git a/Univalence.thy b/Univalence.thy index 001ee33..3c9b520 100644 --- a/Univalence.thy +++ b/Univalence.thy @@ -1,176 +1,88 @@ -(* Title: HoTT/Univalence.thy - Author: Joshua Chen +(* +Title: Univalence.thy +Author: Joshua Chen +Date: 2018 Definitions of homotopy, equivalence and the univalence axiom. *) theory Univalence -imports - HoTT_Methods - EqualProps - ProdProps - Sum +imports HoTT_Methods EqualProps Prod 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)" +definition homotopic :: "[t, tf, t, t] \<Rightarrow> t" where "homotopic A B 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)" +syntax "_homotopic" :: "[t, idt, t, t, t] \<Rightarrow> t" ("(1_ ~[_:_. _]/ _)" [101, 0, 0, 0, 101] 100) +translations "f ~[x:A. B] g" \<rightleftharpoons> "CONST homotopic A (\<lambda>x. B) f g" -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) +declare homotopic_def [comp] +definition isequiv :: "[t, t, t] \<Rightarrow> t" ("(3isequiv[_, _]/ _)") where + "isequiv[A, B] f \<equiv> (\<Sum>g: B \<rightarrow> A. g \<circ> f ~[x:A. A] id) \<times> (\<Sum>g: B \<rightarrow> A. f \<circ> g ~[x:B. B] id)" -text "We use the following lemma in a few proofs:" +text \<open> +The meanings of the syntax defined above are: +\<^item> @{term "f ~[x:A. B x] g"} expresses that @{term f} and @{term g} are homotopic functions of type @{term "\<Prod>x:A. B x"}. +\<^item> @{term "isequiv[A, B] f"} expresses that the non-dependent function @{term f} of type @{term "A \<rightarrow> B"} is an equivalence. +\<close> -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:" +definition equivalence :: "[t, t] \<Rightarrow> t" (infix "\<simeq>" 100) + where "A \<simeq> B \<equiv> \<Sum>f: A \<rightarrow> B. isequiv[A, B] f" + +lemma id_isequiv: + assumes "A: U i" "id: A \<rightarrow> A" + shows "<<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>: isequiv[A, A] id" +unfolding isequiv_def proof (routine add: assms) + show "\<And>g. g: A \<rightarrow> A \<Longrightarrow> id \<circ> g ~[x:A. A] id: U i" by (derive lems: assms) + show "<id, \<^bold>\<lambda>x. refl x>: \<Sum>g:A \<rightarrow> A. (g \<circ> id) ~[x:A. A] id" by (derive lems: assms) + show "<id, \<^bold>\<lambda>x. refl x>: \<Sum>g:A \<rightarrow> A. (id \<circ> g) ~[x:A. A] id" by (derive lems: assms) +qed -lemma equiv_sym: +lemma equivalence_symm: 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) + show "\<And>f. f: A \<rightarrow> A \<Longrightarrow> isequiv[A, A] f: U i" by (derive lems: assms isequiv_def) + show "<<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>: isequiv[A, A] id" using assms by (rule id_isequiv) +qed fact -section \<open>idtoeqv and the univalence axiom\<close> +section \<open>idtoeqv\<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>" +definition idtoeqv :: t where "idtoeqv \<equiv> \<^bold>\<lambda>p. <transport p, ind\<^sub>= (\<lambda>_. <<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." +text \<open>We prove that equal types are equivalent. The proof involves universe types.\<close> 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+ +unfolding idtoeqv_def equivalence_def proof (routine add: assms) + show *: "\<And>f. f: A \<rightarrow> B \<Longrightarrow> isequiv[A, B] f: U i" + unfolding isequiv_def by (derive lems: assms) + + show "\<And>p. p: A =[U i] B \<Longrightarrow> transport p: A \<rightarrow> B" + by (derive lems: assms transport_type[where ?i="Suc i"]) + \<comment> \<open>Instantiate @{thm transport_type} with a suitable universe level here...\<close> + + show "\<And>p. p: A =[U i] B \<Longrightarrow> ind\<^sub>= (\<lambda>_. <<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>) p: isequiv[A, B] (transport p)" + proof (elim Equal_elim) + show "\<And>T. T: U i \<Longrightarrow> <<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>: isequiv[T, T] (transport (refl T))" + by (derive lems: transport_comp[where ?i="Suc i" and ?A="U i"] id_isequiv) + \<comment> \<open>...and also here.\<close> - 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 + show "\<And>A B p. \<lbrakk>A: U i; B: U i; p: A =[U i] B\<rbrakk> \<Longrightarrow> isequiv[A, B] (transport p): U i" + unfolding isequiv_def by (derive lems: assms transport_type) + qed fact+ +qed (derive lems: assms) -text "The univalence axiom." +section \<open>The univalence axiom\<close> -axiomatization univalence :: t where - UA: "univalence: isequiv idtoeqv" +axiomatization univalence :: "[t, t] \<Rightarrow> t" where UA: "univalence A B: isequiv[A, B] idtoeqv" end |