diff options
| -rw-r--r-- | hott/Equivalence.thy | 41 | ||||
| -rw-r--r-- | hott/More_List.thy | 12 |
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 |