diff options
Diffstat (limited to 'Equal.thy')
-rw-r--r-- | Equal.thy | 95 |
1 files changed, 74 insertions, 21 deletions
@@ -1,52 +1,105 @@ -(* -Title: Equal.thy -Author: Joshua Chen -Date: 2018 +(******** +Isabelle/HoTT: Equality +Feb 2019 -Equality type -*) +********) theory Equal -imports HoTT_Base +imports Prod HoTT_Methods begin -section \<open>Basic definitions\<close> +section \<open>Type definitions\<close> axiomatization - Equal :: "[t, t, t] \<Rightarrow> t" and - refl :: "t \<Rightarrow> t" and - indEqual :: "[t \<Rightarrow> t, t] \<Rightarrow> t" ("(1ind\<^sub>=)") + Eq :: "[t, t, t] \<Rightarrow> t" and + refl :: "t \<Rightarrow> t" and + indEq :: "[[t, t, t] \<Rightarrow> t, t \<Rightarrow> t, t] \<Rightarrow> t" syntax - "_equal" :: "[t, t, t] \<Rightarrow> t" ("(3_ =\<^sub>_/ _)" [101, 0, 101] 100) - "_equal_ascii" :: "[t, t, t] \<Rightarrow> t" ("(3_ =[_]/ _)" [101, 0, 101] 100) - + "_Eq" :: "[t, t, t] \<Rightarrow> t" ("(3_ =[_]/ _)" [101, 0, 101] 100) translations - "a =[A] b" \<rightleftharpoons> "CONST Equal A a b" - "a =\<^sub>A b" \<rightharpoonup> "CONST Equal A a b" + "a =[A] b" \<rightleftharpoons> "(CONST Eq) A a b" axiomatization where - Equal_form: "\<lbrakk>A: U i; a: A; b: A\<rbrakk> \<Longrightarrow> a =\<^sub>A b : U i" and + Equal_form: "\<lbrakk>A: U i; a: A; b: A\<rbrakk> \<Longrightarrow> a =[A] b: U i" and - Equal_intro: "a : A \<Longrightarrow> (refl a): a =\<^sub>A a" and + Equal_intro: "a: A \<Longrightarrow> (refl a): a =[A] a" and Equal_elim: "\<lbrakk> - p: x =\<^sub>A y; + p: x =[A] y; x: A; y: 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>= f p : C x y p" and + \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =[A] y \<leadsto> U i \<rbrakk> \<Longrightarrow> indEq C f p : C x y p" and Equal_comp: "\<lbrakk> a: 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>= f (refl a) \<equiv> f a" + \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =[A] y \<leadsto> U i \<rbrakk> \<Longrightarrow> indEq C f (refl a) \<equiv> f a" lemmas Equal_form [form] lemmas Equal_routine [intro] = Equal_form Equal_intro Equal_elim lemmas Equal_comp [comp] +section \<open>Path induction\<close> + +text \<open>We set up rudimentary automation of path induction:\<close> + +method path_ind for x y p :: t = + (rule Equal_elim[where ?x=x and ?y=y and ?p=p]; (fact | assumption)?) + + +section \<open>Properties of equality\<close> + +subsection \<open>Symmetry (path inverse)\<close> + +definition inv :: "[t, t] \<Rightarrow> t" +where "inv A p \<equiv> indEq (\<lambda>x y. ^(y =[A] x)) (\<lambda>x. refl x) p" + +lemma inv_type: "\<lbrakk>A: U i; x: A; y: A; p: x =[A] y\<rbrakk> \<Longrightarrow> inv A p: y =[A] x" +unfolding inv_def by derive + +lemma inv_comp: "\<lbrakk>A: U i; a: A\<rbrakk> \<Longrightarrow> inv A (refl a) \<equiv> refl a" +unfolding inv_def by derive + +declare + inv_type [intro] + inv_comp [comp] + +subsection \<open>Transitivity (path composition)\<close> + +schematic_goal transitivity: + assumes "A: U i" "x: A" "y: A" "p: x =[A] y" + shows "?p: \<Prod>z: A. y =[A]z \<rightarrow> x =[A] z" +proof (path_ind x y p, quantify 2) + fix x z show "\<And>p. p: x =[A] z \<Longrightarrow> p: x =[A] z" . +qed (routine add: assms) + + +syntax "_pathcomp" :: "[t, t] \<Rightarrow> t" (infixl "\<bullet>" 110) +translations "p \<bullet> q" \<rightleftharpoons> "CONST pathcomp`p`q" + +lemma pathcomp_type: + assumes "A: U i" "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) + +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) + +lemma pathcomp_comp: + assumes "A: U i" and "a: A" + shows "(refl a) \<bullet> (refl a) \<equiv> refl a" +unfolding pathcomp_def by (derive lems: assms) + +declare + pathcomp_type [intro] + pathcomp_trans [intro] + pathcomp_comp [comp] + end |