proved a few oopses + minor tweaks

2 files changed, 23 insertions, 30 deletions

diff --git a/hott/Equivalence.thy b/hott/Equivalence.thy
index 9c86a95..aa73ec8 100644
--- a/hott/Equivalence.thy
+++ b/hott/Equivalence.thy
@@ -75,7 +75,7 @@ Lemma (derive) commute_homotopy:
     "f: A \<rightarrow> B" "g: A \<rightarrow> B"
     "H: homotopy A (\<lambda>_. B) f g"
   shows "(H x) \<bullet> g[p] = f[p] \<bullet> (H y)"
-  \<comment> \<open>Need this assumption unfolded for typechecking:\<close>
+  \<comment> \<open>Need this assumption unfolded for typechecking\<close>
   supply assms(8)[unfolded homotopy_def]
   apply (eq p)
     focus vars x
@@ -167,8 +167,8 @@ Lemma (derive) id_qinv:
   unfolding qinv_def
   apply intro defer
     apply intro defer
-      apply (rule homotopy_id_right)
-      apply (rule homotopy_id_left)
+      apply htpy_id
+      apply id_htpy
   done
 
 Lemma (derive) quasiinv_qinv:
@@ -176,14 +176,14 @@ Lemma (derive) quasiinv_qinv:
   shows "prf: qinv f \<Longrightarrow> qinv (fst prf)"
   unfolding qinv_def
   apply intro
-    \<guillemotright> by (rule \<open>f:_\<close>)
-    \<guillemotright> apply (elim "prf")
-        focus vars g HH
-          apply intro
-            \<^item> by reduce (snd HH)
-            \<^item> by reduce (fst HH)
-        done
-      done
+  \<guillemotright> by (rule \<open>f:_\<close>)
+  \<guillemotright> apply (elim "prf")
+    focus vars g HH
+      apply intro
+        \<^item> by reduce (snd HH)
+        \<^item> by reduce (fst HH)
+    done
+    done
   done
 
 Lemma (derive) funcomp_qinv:
@@ -272,7 +272,7 @@ Lemma (derive) biinv_imp_qinv:
         also have ".. ~ (id A) \<circ> h" by (subst funcomp_assoc[symmetric]) (htpy_o, fact)
         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)
+        then have "f \<circ> g ~ f \<circ> h" by o_htpy
         also note \<open>H2:_\<close>
         finally show "f \<circ> g ~ id B" by this
       qed
@@ -281,7 +281,7 @@ Lemma (derive) biinv_imp_qinv:
 
 Lemma (derive) id_biinv:
   "A: U i \<Longrightarrow> biinv (id A)"
-    by (rule qinv_imp_biinv) (rule id_qinv)
+  by (rule qinv_imp_biinv) (rule id_qinv)
 
 Lemma (derive) funcomp_biinv:
   assumes
@@ -290,9 +290,8 @@ Lemma (derive) funcomp_biinv:
   shows "biinv f \<rightarrow> biinv g \<rightarrow> biinv (g \<circ> f)"
   apply intros
   focus vars biinv\<^sub>f biinv\<^sub>g
-
-  text \<open>Follows from \<open>funcomp_qinv\<close>.\<close>
-oops
+    by (rule qinv_imp_biinv) (rule funcomp_qinv; rule biinv_imp_qinv)
+  done
 
 
 section \<open>Equivalence\<close>
@@ -343,9 +342,13 @@ Lemma (derive) equivalence_transitive:
   shows "A \<simeq> B \<rightarrow> B \<simeq> C \<rightarrow> A \<simeq> C"
   apply intros
   unfolding equivalence_def
-
-  text \<open>Use \<open>funcomp_biinv\<close>.\<close>
-oops
+    focus vars p q apply (elim p, elim q)
+      focus vars f biinv\<^sub>f g biinv\<^sub>g apply intro
+        \<guillemotright> apply (rule funcompI) defer by assumption known
+        \<guillemotright> by (rule funcomp_biinv)
+      done
+    done
+  done
 
 text \<open>
   Equal types are equivalent. We give two proofs: the first by induction, and
diff --git a/hott/More_List.thy b/hott/More_List.thy
index c3d63f6..a216987 100644
--- a/hott/More_List.thy
+++ b/hott/More_List.thy
@@ -5,24 +5,14 @@ imports
 
 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)"
+definition [implicit]: "len \<equiv> ListRec ? Nat 0 (\<lambda>_ _ rec. suc rec)"
 
 experiment begin
   Lemma "len [] \<equiv> ?n" by (subst comps)+
   Lemma "len [0, suc 0, suc (suc 0)] \<equiv> ?n" by (subst comps)+
 end
 
-section \<open>Equality on lists\<close>
-
-(*Hmmm.*)
-
 
 end