1 files changed, 69 insertions, 6 deletions
diff --git a/EqualProps.thy b/EqualProps.thy
index 5db8487..19c788c 100644
--- a/EqualProps.thy
+++ b/EqualProps.thy
@@ -14,7 +14,7 @@ begin
 
 section \<open>Symmetry / Path inverse\<close>
 
-definition inv :: "Term \<Rightarrow> Term"  ("_\<inverse>" [1000] 1000) where "p\<inverse> \<equiv> ind\<^sub>= (\<lambda>x. (refl x)) p"
+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.
@@ -46,7 +46,7 @@ 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 :: Term where "rpathcomp \<equiv> \<^bold>\<lambda>_ _ p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>_ q. ind\<^sub>= (\<lambda>x. (refl x)) q) p"
+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:
@@ -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>" 120) where
+axiomatization pathcomp :: "[t, t] \<Rightarrow> t"  (infixl "\<bullet>" 120) where
   pathcomp_def: "\<lbrakk>
     A: U i;
     x: A; y: A; z: A;
@@ -216,9 +216,72 @@ 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)
+  
 
 section \<open>Higher groupoid structure of types\<close>
 
@@ -275,7 +338,7 @@ sorry
 
 section \<open>Transport\<close>
 
-definition transport :: "Term \<Rightarrow> Term" where
+definition transport :: "t \<Rightarrow> t" where
   "transport p \<equiv> ind\<^sub>= (\<lambda>x. (\<^bold>\<lambda>x. x)) p"
 
 text "Note that \<open>transport\<close> is a polymorphic function in our formulation."