aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJosh Chen2018-09-18 03:04:37 +0200
committerJosh Chen2018-09-18 03:04:37 +0200
commitdcf87145a1059659099bbecde55973de0d36d43f (patch)
tree03707f3dc962e6b762890cff92cb106834b879bc
parent49c008ef405ab8d8229ae1d5b0737339ee46e576 (diff)
Theories fully reorganized. Well-formedness rules removed. New methods etc.
Diffstat (limited to '')
-rw-r--r--Equal.thy10
-rw-r--r--EqualProps.thy398
-rw-r--r--HoTT_Base.thy4
-rw-r--r--HoTT_Methods.thy18
-rw-r--r--Prod.thy5
-rw-r--r--Univalence.thy194
6 files changed, 158 insertions, 471 deletions
diff --git a/Equal.thy b/Equal.thy
index f9bc223..7a31e37 100644
--- a/Equal.thy
+++ b/Equal.thy
@@ -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>
diff --git a/Prod.thy b/Prod.thy
index db18454..4aa7119 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -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