new material

5 files changed, 58 insertions, 34 deletions

diff --git a/hott/Eckmann_Hilton.thy b/hott/Eckmann_Hilton.thy
new file mode 100644
index 0000000..7355fde
--- /dev/null
+++ b/hott/Eckmann_Hilton.thy
@@ -0,0 +1,21 @@
+theory Eckmann_Hilton
+imports Identity
+
+begin
+
+Lemma (derive) left_whisker:
+  assumes "A: U i" "a: A" "b: A" "c: A"
+  shows "\<lbrakk>p: a = b; q: a = b; r: b = c; \<alpha>: p =\<^bsub>a = b\<^esub> q\<rbrakk> \<Longrightarrow> p \<bullet> r = q \<bullet> r"
+  apply (eq r)
+  focus prems prms vars x s t \<gamma>
+    proof -
+      have "t \<bullet> refl x = t" by (rule pathcomp_refl)
+      also have ".. = s" by (rule \<open>\<gamma>:_\<close>)
+      also have ".. = s \<bullet> refl x" by (rule pathcomp_refl[symmetric])
+      finally show "t \<bullet> refl x = s \<bullet> refl x" by this
+    qed
+  done
+
+
+
+end
diff --git a/hott/Equivalence.thy b/hott/Equivalence.thy
index 2975738..9e7b83a 100644
--- a/hott/Equivalence.thy
+++ b/hott/Equivalence.thy
@@ -61,6 +61,8 @@ Lemma (derive) htrans:
 
 text \<open>For calculations:\<close>
 
+congruence "f ~ g" rhs g
+
 lemmas
   homotopy_sym [sym] = hsym[rotated 4] and
   homotopy_trans [trans] = htrans[rotated 5]
@@ -81,8 +83,8 @@ Lemma (derive) commute_homotopy:
         \<comment> \<open>Here it would really be nice to have automation for transport and
           propositional equality.\<close>
         apply (rule use_transport[where ?y="H x \<bullet> refl (g x)"])
-          \<guillemotright> by (rule pathcomp_right_refl)
-          \<guillemotright> by (rule pathinv) (rule pathcomp_left_refl)
+          \<guillemotright> by (rule pathcomp_refl)
+          \<guillemotright> by (rule pathinv) (rule refl_pathcomp)
           \<guillemotright> by typechk
     done
   done
@@ -256,12 +258,12 @@ Lemma (derive) biinv_imp_qinv:
       \<close>
       proof -
         have "g ~ g \<circ> (id B)" by reduce refl
-        also have "g \<circ> (id B) ~ g \<circ> f \<circ> h"
+        also have ".. ~ g \<circ> f \<circ> h"
           by (rule homotopy_funcomp_right) (rule \<open>H2:_\<close>[symmetric])
-        also have "g \<circ> f \<circ> h ~ (id A) \<circ> h"
+        also have ".. ~ (id A) \<circ> h"
           by (subst funcomp_assoc[symmetric])
              (rule homotopy_funcomp_left, rule \<open>H1:_\<close>)
-        also have "(id A) \<circ> h ~ h" by reduce refl
+        also have ".. ~ h" by reduce refl
         finally have "g ~ h" by this
 
         then have "f \<circ> g ~ f \<circ> h" by (rule homotopy_funcomp_right)
@@ -348,8 +350,7 @@ text \<open>
 \<close>
 
 Lemma
-  assumes
-    "A: U i" "B: U i" "p: A =\<^bsub>U i\<^esub> B"
+  assumes "A: U i" "B: U i" "p: A =\<^bsub>U i\<^esub> B"
   shows "A \<simeq> B"
   by (eq p) (rule equivalence_refl)
 
diff --git a/hott/Identity.thy b/hott/Identity.thy
index 3fef536..d60f4c2 100644
--- a/hott/Identity.thy
+++ b/hott/Identity.thy
@@ -120,25 +120,7 @@ translations
 
 section \<open>Calculational reasoning\<close>
 
-consts rhs :: \<open>'a\<close> ("''''")
-
-ML \<open>
-local fun last_rhs ctxt =
-  let
-    val this_name = Name_Space.full_name (Proof_Context.naming_of ctxt)
-      (Binding.name Auto_Bind.thisN)
-    val this = #thms (the (Proof_Context.lookup_fact ctxt this_name))
-      handle Option => []
-    val rhs = case map Thm.prop_of this of
-       [\<^const>\<open>has_type\<close> $ _ $ (\<^const>\<open>Id\<close> $ _ $ _ $ y)] => y
-      | _ => Term.dummy
-  in
-    map_aterms (fn t => case t of Const (\<^const_name>\<open>rhs\<close>, _) => rhs | _ => t)
-  end
-in val _ = Context.>>
-  (Syntax_Phases.term_check 5 "" (fn ctxt => map (last_rhs ctxt)))
-end
-\<close>
+congruence "x = y" rhs y
 
 lemmas
   [sym] = pathinv[rotated 3] and
@@ -147,28 +129,28 @@ lemmas
 
 section \<open>Basic propositional equalities\<close>
 
-Lemma (derive) pathcomp_left_refl:
+Lemma (derive) refl_pathcomp:
   assumes "A: U i" "x: A" "y: A" "p: x =\<^bsub>A\<^esub> y"
   shows "(refl x) \<bullet> p = p"
   apply (eq p)
     apply (reduce; intros)
   done
 
-Lemma (derive) pathcomp_right_refl:
+Lemma (derive) pathcomp_refl:
   assumes "A: U i" "x: A" "y: A" "p: x =\<^bsub>A\<^esub> y"
   shows "p \<bullet> (refl y) = p"
   apply (eq p)
     apply (reduce; intros)
   done
 
-Lemma (derive) pathcomp_left_inv:
+Lemma (derive) inv_pathcomp:
   assumes "A: U i" "x: A" "y: A" "p: x =\<^bsub>A\<^esub> y"
   shows "p\<inverse> \<bullet> p = refl y"
   apply (eq p)
     apply (reduce; intros)
   done
 
-Lemma (derive) pathcomp_right_inv:
+Lemma (derive) pathcomp_inv:
   assumes "A: U i" "x: A" "y: A" "p: x =\<^bsub>A\<^esub> y"
   shows "p \<bullet> p\<inverse> = refl x"
   apply (eq p)
diff --git a/hott/More_List.thy b/hott/More_List.thy
index 2f868b8..aa57635 100644
--- a/hott/More_List.thy
+++ b/hott/More_List.thy
@@ -1,8 +1,28 @@
 theory More_List
-imports Spartan.List
+imports
+  Spartan.List
+  Nat
 
 begin
 
+experiment begin
+  Lemma "map (\<lambda>n: Nat. suc n) [0, suc (suc 0), suc 0] \<equiv> ?xs"
+    unfolding map_def by (subst comps)+
+end
+
+section \<open>Length\<close>
+
+definition [implicit]:
+  "len \<equiv> ListRec ? Nat 0 (\<lambda>_ _ n. suc n)"
+
+experiment begin
+  Lemma "len [] \<equiv> 0" by reduce
+  Lemma "len [0, suc 0, suc (suc 0)] \<equiv> ?n" by (subst comps)+
+end
+
+section \<open>Equality on lists\<close>
+
+(*Hmmm.*)
 
 
 end
diff --git a/hott/Nat.thy b/hott/Nat.thy
index d54ea7b..c36154e 100644
--- a/hott/Nat.thy
+++ b/hott/Nat.thy
@@ -44,7 +44,7 @@ lemmas
 
 text \<open>Non-dependent recursion\<close>
 
-abbreviation "NatRec C \<equiv> NatInd (K C)"
+abbreviation "NatRec C \<equiv> NatInd (\<lambda>_. C)"
 
 
 section \<open>Basic arithmetic\<close>
@@ -100,10 +100,10 @@ Lemma (derive) add_comm:
   shows "m + n = n + m"
   apply (elim m)
     \<guillemotright> by (reduce; rule add_zero[symmetric])
-    \<guillemotright> prems prms vars m ih
+    \<guillemotright> prems vars m ih
       proof reduce
         have "suc (m + n) = suc (n + m)" by (eq ih) intro
-        also have "'' = n + suc m" by (rule add_suc[symmetric])
+        also have ".. = n + suc m" by (rule add_suc[symmetric])
         finally show "suc (m + n) = n + suc m" by this
       qed
   done