diff options
author | Josh Chen | 2020-05-26 16:50:35 +0200 |
---|---|---|
committer | Josh Chen | 2020-05-26 16:50:35 +0200 |
commit | b0ba102b783418560f9b7b15239681b11ea4c877 (patch) | |
tree | 0158979a77c146f254eab072b300b0fb2579f1a4 /hott/Equivalence.thy | |
parent | 028f43a0737128024742234f3ee95b24986d6403 (diff) |
new material
Diffstat (limited to '')
-rw-r--r-- | hott/Equivalence.thy | 15 |
1 files changed, 8 insertions, 7 deletions
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) |