aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Equal.thy124
1 files changed, 104 insertions, 20 deletions
diff --git a/Equal.thy b/Equal.thy
index 1d8f6ae..c10e1c2 100644
--- a/Equal.thy
+++ b/Equal.thy
@@ -15,7 +15,7 @@ section \<open>Type definitions\<close>
axiomatization
Eq :: "[t, t, t] \<Rightarrow> t" and
refl :: "t \<Rightarrow> t" and
- indEq :: "[[t, t, t] \<Rightarrow> t, t \<Rightarrow> t, t] \<Rightarrow> t"
+ indEq :: "[[t, t, t] \<Rightarrow> t, t \<Rightarrow> t, t, t, t] \<Rightarrow> t"
syntax
"_Eq" :: "[t, t, t] \<Rightarrow> t" ("(3_ =[_]/ _)" [101, 0, 101] 100)
@@ -32,12 +32,12 @@ axiomatization where
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 =[A] y \<leadsto> U i \<rbrakk> \<Longrightarrow> indEq C 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 x y 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 =[A] y \<leadsto> U i \<rbrakk> \<Longrightarrow> indEq C 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 a a (refl a) \<equiv> f a"
lemmas Equal_form [form]
lemmas Equal_routine [intro] = Equal_form Equal_intro Equal_elim
@@ -56,13 +56,29 @@ 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"
+definition inv :: "[t, t, t, t] \<Rightarrow> t"
+where "inv A x y p \<equiv> indEq (\<lambda>x y. ^(y =[A] x)) (\<lambda>x. refl x) x y p"
-lemma inv_type: "\<lbrakk>A: U i; x: A; y: A; p: x =[A] y\<rbrakk> \<Longrightarrow> inv A p: y =[A] x"
+syntax "_inv" :: "t \<Rightarrow> t" ("~_" [1000])
+
+text \<open>Pretty-printing switch for path inverse:\<close>
+
+ML \<open>val pretty_inv = Attrib.setup_config_bool @{binding "pretty_inv"} (K true)\<close>
+
+print_translation \<open>
+let fun inv_tr' ctxt [A, x, y, p] =
+ if Config.get ctxt pretty_inv
+ then Syntax.const @{syntax_const "_inv"} $ p
+ else @{const inv} $ A $ x $ y $ p
+in
+ [(@{const_syntax inv}, inv_tr')]
+end
+\<close>
+
+lemma inv_type: "\<lbrakk>A: U i; x: A; y: A; p: x =[A] y\<rbrakk> \<Longrightarrow> inv A x y 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"
+lemma inv_comp: "\<lbrakk>A: U i; a: A\<rbrakk> \<Longrightarrow> inv A a a (refl a) \<equiv> refl a"
unfolding inv_def by derive
declare
@@ -74,32 +90,100 @@ 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)
+proof (path_ind x y p, quantify_all)
fix x z show "\<And>p. p: x =[A] z \<Longrightarrow> p: x =[A] z" .
qed (routine add: assms)
+definition pathcomp :: "[t, t, t, t, t, t] \<Rightarrow> t"
+where
+ "pathcomp A x y z p q \<equiv>
+ (indEq (\<lambda>x y _. \<Prod>z: A. y =[A] z \<rightarrow> x =[A] z) (\<lambda>x. \<lambda>y: A. id (x =[A] y)) x y p)`z`q"
-syntax "_pathcomp" :: "[t, t] \<Rightarrow> t" (infixl "\<bullet>" 110)
-translations "p \<bullet> q" \<rightleftharpoons> "CONST pathcomp`p`q"
+syntax "_pathcomp" :: "[t, t] \<Rightarrow> t" (infixl "*" 110)
-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)
+text \<open>Pretty-printing switch for path composition:\<close>
+
+ML \<open>val pretty_pathcomp = Attrib.setup_config_bool @{binding "pretty_pathcomp"} (K true)\<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)
+print_translation \<open>
+let fun pathcomp_tr' ctxt [A, x, y, z, p, q] =
+ if Config.get ctxt pretty_pathcomp
+ then Syntax.const @{syntax_const "_pathcomp"} $ p $ q
+ else @{const pathcomp} $ A $ x $ y $ z $ p $ q
+in
+ [(@{const_syntax pathcomp}, pathcomp_tr')]
+end
+\<close>
+
+lemma pathcomp_type:
+ assumes "A: U i" "x: A" "y: A" "z: A" "p: x =[A] y" "q: y =[A] z"
+ shows "pathcomp A x y z p q: x =[A] z"
+unfolding pathcomp_def by (routine add: transitivity assms)
lemma pathcomp_comp:
assumes "A: U i" and "a: A"
- shows "(refl a) \<bullet> (refl a) \<equiv> refl a"
+ shows "pathcomp A a a a (refl a) (refl a) \<equiv> refl a"
unfolding pathcomp_def by (derive lems: assms)
declare
pathcomp_type [intro]
- pathcomp_trans [intro]
pathcomp_comp [comp]
+
+section \<open>Higher groupoid structure of types\<close>
+
+schematic_goal pathcomp_idr:
+ assumes "A: U i" "x: A" "y: A" "p: x =[A] y"
+ shows "?a: pathcomp A x y y p (refl y) =[x =[A] y] p"
+proof (path_ind x y p)
+ show "\<And>x. x: A \<Longrightarrow> refl(refl x): pathcomp A x x x (refl x) (refl x) =[x =[A] x] (refl x)"
+ by (derive lems: assms)
+qed (routine add: assms)
+
+schematic_goal pathcomp_idl:
+ assumes "A: U i" "x: A" "y: A" "p: x =[A] y"
+ shows "?a: pathcomp A x x y (refl x) p =[x =[A] y] p"
+proof (path_ind x y p)
+ show "\<And>x. x: A \<Longrightarrow> refl(refl x): pathcomp A x x x (refl x) (refl x) =[x =[A] x] (refl x)"
+ by (derive lems: assms)
+qed (routine add: assms)
+
+schematic_goal pathcomp_invl:
+ assumes "A: U i" "x: A" "y: A" "p: x =[A] y"
+ shows "?a: pathcomp A y x y (inv A x y p) p =[y =[A] y] refl(y)"
+proof (path_ind x y p)
+ show
+ "\<And>x. x: A \<Longrightarrow> refl(refl x):
+ pathcomp A x x x (inv A x x (refl x)) (refl x) =[x =[A] x] (refl x)"
+ by (derive lems: assms)
+qed (routine add: assms)
+
+schematic_goal pathcomp_right_inv:
+ assumes "A: U i" "x: A" "y: A" "p: x =[A] y"
+ shows "?a: pathcomp A x y x p (inv A x y p) =[x =[A] x] (refl x)"
+proof (path_ind x y p)
+ show
+ "\<And>x. x: A \<Longrightarrow> refl(refl x):
+ pathcomp A x x x (refl x) (inv A x x (refl x)) =[x =[A] x] (refl x)"
+ by (derive lems: assms)
+qed (routine add: assms)
+
+schematic_goal inv_involutive:
+ assumes "A: U i" "x: A" "y: A" "p: x =[A] y"
+ shows "?a: inv A y x (inv A x y p) =[x =[A] y] p"
+proof (path_ind x y p)
+ show "\<And>x. x: A \<Longrightarrow> refl(refl x): inv A x x (inv A x x (refl x)) =[x =[A] x] (refl x)"
+ by (derive lems: assms)
+qed (routine add: assms)
+
+schematic_goal pathcomp_assoc:
+ fixes x y p
+ assumes "A: U i" "x: A" "y: A" "z: A" "w: A" and "p: x =[A] y" "q: y =[A] z" "r: z =[A] w"
+ shows
+ "?a:
+ pathcomp A x y w p (pathcomp A y z w q r) =[x =[A] w]
+ pathcomp A x z w (pathcomp A x y z p q) r"
+proof
+ fix x y p
+
end