aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--hott/Equivalence.thy41
-rw-r--r--hott/More_List.thy12
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