aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--EqualProps.thy71
1 files changed, 67 insertions, 4 deletions
diff --git a/EqualProps.thy b/EqualProps.thy
index a1d4c45..be8e53e 100644
--- a/EqualProps.thy
+++ b/EqualProps.thy
@@ -33,7 +33,7 @@ text "
"
lemma inv_comp:
- assumes "A : U(i)" and "a : A" shows "(refl a)\<inverse> \<equiv> refl(a)"
+ 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" ..
@@ -194,7 +194,7 @@ qed fact
text "The raw object lambda term is cumbersome to use, so we define a simpler constant instead."
-axiomatization pathcomp :: "[Term, Term] \<Rightarrow> Term" (infixl "\<bullet>" 60) where
+axiomatization pathcomp :: "[Term, Term] \<Rightarrow> Term" (infixl "\<bullet>" 120) where
pathcomp_def: "\<lbrakk>
A: U(i);
x: A; y: A; z: A;
@@ -214,8 +214,71 @@ lemma pathcomp_comp:
by (subst pathcomp_def) (routine lems: assms rpathcomp_comp)
-lemmas EqualProps_type [intro] = inv_type pathcomp_type
-lemmas EqualProps_comp [comp] = inv_comp pathcomp_comp
+lemmas inv_type [intro]
+lemmas pathcomp_type [intro]
+lemmas inv_comp [comp]
+lemmas pathcomp_comp [comp]
+
+
+section \<open>Weak higher groupoid structure of types\<close>
+
+schematic_goal whg1a:
+ 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)
+
+schematic_goal whg1b:
+ assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y"
+ shows "?a: p =[x =\<^sub>A y] (refl(x) \<bullet> 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)
+
+schematic_goal whg2a:
+ 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)+
+
+schematic_goal whg2b:
+ 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)+
+
+schematic_goal whg3:
+ 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)
+
+
+schematic_goal
+ assumes
+ "A: U(i)" and
+ "x: A" "y: A" "z: A" "w: A" and
+ "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)
+
end