src/HOL/Analysis/Homotopy.thy
changeset 69986 f2d327275065
parent 69922 4a9167f377b0
child 70033 6cbc7634135c
     1.1 --- a/src/HOL/Analysis/Homotopy.thy	Sun Mar 24 20:31:53 2019 +0100
     1.2 +++ b/src/HOL/Analysis/Homotopy.thy	Tue Mar 26 17:01:36 2019 +0000
     1.3 @@ -5,172 +5,299 @@
     1.4  section \<open>Homotopy of Maps\<close>
     1.5  
     1.6  theory Homotopy
     1.7 -  imports Path_Connected Continuum_Not_Denumerable
     1.8 +  imports Path_Connected Continuum_Not_Denumerable Product_Topology
     1.9  begin
    1.10  
    1.11 -definition%important homotopic_with ::
    1.12 -  "[('a::topological_space \<Rightarrow> 'b::topological_space) \<Rightarrow> bool, 'a set, 'b set, 'a \<Rightarrow> 'b, 'a \<Rightarrow> 'b] \<Rightarrow> bool"
    1.13 +definition%important homotopic_with
    1.14  where
    1.15 - "homotopic_with P X Y p q \<equiv>
    1.16 -   (\<exists>h:: real \<times> 'a \<Rightarrow> 'b.
    1.17 -       continuous_on ({0..1} \<times> X) h \<and>
    1.18 -       h ` ({0..1} \<times> X) \<subseteq> Y \<and>
    1.19 -       (\<forall>x. h(0, x) = p x) \<and>
    1.20 -       (\<forall>x. h(1, x) = q x) \<and>
    1.21 -       (\<forall>t \<in> {0..1}. P(\<lambda>x. h(t, x))))"
    1.22 + "homotopic_with P X Y f g \<equiv>
    1.23 +   (\<exists>h. continuous_map (prod_topology (subtopology euclideanreal {0..1}) X) Y h \<and>
    1.24 +       (\<forall>x. h(0, x) = f x) \<and>
    1.25 +       (\<forall>x. h(1, x) = g x) \<and>
    1.26 +       (\<forall>t \<in> {0..1}. P(\<lambda>x. h(t,x))))"
    1.27  
    1.28  text\<open>\<open>p\<close>, \<open>q\<close> are functions \<open>X \<rightarrow> Y\<close>, and the property \<open>P\<close> restricts all intermediate maps.
    1.29  We often just want to require that \<open>P\<close> fixes some subset, but to include the case of a loop homotopy,
    1.30  it is convenient to have a general property \<open>P\<close>.\<close>
    1.31  
    1.32 +abbreviation homotopic_with_canon ::
    1.33 +  "[('a::topological_space \<Rightarrow> 'b::topological_space) \<Rightarrow> bool, 'a set, 'b set, 'a \<Rightarrow> 'b, 'a \<Rightarrow> 'b] \<Rightarrow> bool"
    1.34 +where
    1.35 + "homotopic_with_canon P S T p q \<equiv> homotopic_with P (top_of_set S) (top_of_set T) p q"
    1.36 +
    1.37 +lemma split_01: "{0..1::real} = {0..1/2} \<union> {1/2..1}"
    1.38 +  by force
    1.39 +
    1.40 +lemma split_01_prod: "{0..1::real} \<times> X = ({0..1/2} \<times> X) \<union> ({1/2..1} \<times> X)"
    1.41 +  by force
    1.42 +
    1.43 +lemma image_Pair_const: "(\<lambda>x. (x, c)) ` A = A \<times> {c}"
    1.44 +  by auto
    1.45 +
    1.46 +lemma fst_o_paired [simp]: "fst \<circ> (\<lambda>(x,y). (f x y, g x y)) = (\<lambda>(x,y). f x y)"
    1.47 +  by auto
    1.48 +
    1.49 +lemma snd_o_paired [simp]: "snd \<circ> (\<lambda>(x,y). (f x y, g x y)) = (\<lambda>(x,y). g x y)"
    1.50 +  by auto
    1.51 +
    1.52 +lemma continuous_on_o_Pair: "\<lbrakk>continuous_on (T \<times> X) h; t \<in> T\<rbrakk> \<Longrightarrow> continuous_on X (h \<circ> Pair t)"
    1.53 +  by (fast intro: continuous_intros elim!: continuous_on_subset)
    1.54 +
    1.55 +lemma continuous_map_o_Pair: 
    1.56 +  assumes h: "continuous_map (prod_topology X Y) Z h" and t: "t \<in> topspace X"
    1.57 +  shows "continuous_map Y Z (h \<circ> Pair t)"
    1.58 +  apply (intro continuous_map_compose [OF _ h] continuous_map_id [unfolded id_def] continuous_intros)
    1.59 +  apply (simp add: t)
    1.60 +  done
    1.61 +
    1.62 +subsection%unimportant\<open>Trivial properties\<close>
    1.63 +
    1.64  text \<open>We often want to just localize the ending function equality or whatever.\<close>
    1.65  text%important \<open>%whitespace\<close>
    1.66  proposition homotopic_with:
    1.67 -  fixes X :: "'a::topological_space set" and Y :: "'b::topological_space set"
    1.68 -  assumes "\<And>h k. (\<And>x. x \<in> X \<Longrightarrow> h x = k x) \<Longrightarrow> (P h \<longleftrightarrow> P k)"
    1.69 +  assumes "\<And>h k. (\<And>x. x \<in> topspace X \<Longrightarrow> h x = k x) \<Longrightarrow> (P h \<longleftrightarrow> P k)"
    1.70    shows "homotopic_with P X Y p q \<longleftrightarrow>
    1.71 -           (\<exists>h :: real \<times> 'a \<Rightarrow> 'b.
    1.72 -              continuous_on ({0..1} \<times> X) h \<and>
    1.73 -              h ` ({0..1} \<times> X) \<subseteq> Y \<and>
    1.74 -              (\<forall>x \<in> X. h(0,x) = p x) \<and>
    1.75 -              (\<forall>x \<in> X. h(1,x) = q x) \<and>
    1.76 +           (\<exists>h. continuous_map (prod_topology (subtopology euclideanreal {0..1}) X) Y h \<and>
    1.77 +              (\<forall>x \<in> topspace X. h(0,x) = p x) \<and>
    1.78 +              (\<forall>x \<in> topspace X. h(1,x) = q x) \<and>
    1.79                (\<forall>t \<in> {0..1}. P(\<lambda>x. h(t, x))))"
    1.80    unfolding homotopic_with_def
    1.81    apply (rule iffI, blast, clarify)
    1.82 -  apply (rule_tac x="\<lambda>(u,v). if v \<in> X then h(u,v) else if u = 0 then p v else q v" in exI)
    1.83 +  apply (rule_tac x="\<lambda>(u,v). if v \<in> topspace X then h(u,v) else if u = 0 then p v else q v" in exI)
    1.84    apply auto
    1.85 -  apply (force elim: continuous_on_eq)
    1.86 +  using continuous_map_eq apply fastforce
    1.87    apply (drule_tac x=t in bspec, force)
    1.88    apply (subst assms; simp)
    1.89    done
    1.90  
    1.91 -proposition homotopic_with_eq:
    1.92 -   assumes h: "homotopic_with P X Y f g"
    1.93 -       and f': "\<And>x. x \<in> X \<Longrightarrow> f' x = f x"
    1.94 -       and g': "\<And>x. x \<in> X \<Longrightarrow> g' x = g x"
    1.95 -       and P:  "(\<And>h k. (\<And>x. x \<in> X \<Longrightarrow> h x = k x) \<Longrightarrow> (P h \<longleftrightarrow> P k))"
    1.96 -   shows "homotopic_with P X Y f' g'"
    1.97 -  using h unfolding homotopic_with_def
    1.98 -  apply safe
    1.99 -  apply (rule_tac x="\<lambda>(u,v). if v \<in> X then h(u,v) else if u = 0 then f' v else g' v" in exI)
   1.100 -  apply (simp add: f' g', safe)
   1.101 -  apply (fastforce intro: continuous_on_eq, fastforce)
   1.102 -  apply (subst P; fastforce)
   1.103 +lemma homotopic_with_mono:
   1.104 +  assumes hom: "homotopic_with P X Y f g"
   1.105 +    and Q: "\<And>h. \<lbrakk>continuous_map X Y h; P h\<rbrakk> \<Longrightarrow> Q h"
   1.106 +  shows "homotopic_with Q X Y f g"
   1.107 +  using hom
   1.108 +  apply (simp add: homotopic_with_def)
   1.109 +  apply (erule ex_forward)
   1.110 +  apply (force simp: o_def dest: continuous_map_o_Pair intro: Q)
   1.111    done
   1.112  
   1.113 -proposition homotopic_with_equal:
   1.114 -   assumes contf: "continuous_on X f" and fXY: "f ` X \<subseteq> Y"
   1.115 -       and gf: "\<And>x. x \<in> X \<Longrightarrow> g x = f x"
   1.116 -       and P:  "P f" "P g"
   1.117 -   shows "homotopic_with P X Y f g"
   1.118 +lemma homotopic_with_imp_continuous_maps:
   1.119 +    assumes "homotopic_with P X Y f g"
   1.120 +    shows "continuous_map X Y f \<and> continuous_map X Y g"
   1.121 +proof -
   1.122 +  obtain h
   1.123 +    where conth: "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X) Y h"
   1.124 +      and h: "\<forall>x. h (0, x) = f x" "\<forall>x. h (1, x) = g x"
   1.125 +    using assms by (auto simp: homotopic_with_def)
   1.126 +  have *: "t \<in> {0..1} \<Longrightarrow> continuous_map X Y (h \<circ> (\<lambda>x. (t,x)))" for t
   1.127 +    by (rule continuous_map_compose [OF _ conth]) (simp add: o_def continuous_map_pairwise)
   1.128 +  show ?thesis
   1.129 +    using h *[of 0] *[of 1] by (simp add: continuous_map_eq)
   1.130 +qed
   1.131 +
   1.132 +lemma homotopic_with_imp_continuous:
   1.133 +    assumes "homotopic_with_canon P X Y f g"
   1.134 +    shows "continuous_on X f \<and> continuous_on X g"
   1.135 +  by (meson assms continuous_map_subtopology_eu homotopic_with_imp_continuous_maps)
   1.136 +
   1.137 +lemma homotopic_with_imp_property:
   1.138 +  assumes "homotopic_with P X Y f g"
   1.139 +  shows "P f \<and> P g"
   1.140 +proof
   1.141 +  obtain h where h: "\<And>x. h(0, x) = f x" "\<And>x. h(1, x) = g x" and P: "\<And>t. t \<in> {0..1::real} \<Longrightarrow> P(\<lambda>x. h(t,x))"
   1.142 +    using assms by (force simp: homotopic_with_def)
   1.143 +  show "P f" "P g"
   1.144 +    using P [of 0] P [of 1] by (force simp: h)+
   1.145 +qed
   1.146 +
   1.147 +lemma homotopic_with_equal:
   1.148 +  assumes "P f" "P g" and contf: "continuous_map X Y f" and fg: "\<And>x. x \<in> topspace X \<Longrightarrow> f x = g x"
   1.149 +  shows "homotopic_with P X Y f g"
   1.150    unfolding homotopic_with_def
   1.151 -  apply (rule_tac x="\<lambda>(u,v). if u = 1 then g v else f v" in exI)
   1.152 -  using assms
   1.153 -  apply (intro conjI)
   1.154 -  apply (rule continuous_on_eq [where f = "f \<circ> snd"])
   1.155 -  apply (rule continuous_intros | force)+
   1.156 -  apply clarify
   1.157 -  apply (case_tac "t=1"; force)
   1.158 +proof (intro exI conjI allI ballI)
   1.159 +  let ?h = "\<lambda>(t::real,x). if t = 1 then g x else f x"
   1.160 +  show "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X) Y ?h"
   1.161 +  proof (rule continuous_map_eq)
   1.162 +    show "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X) Y (f \<circ> snd)"
   1.163 +      by (simp add: contf continuous_map_of_snd)
   1.164 +  qed (auto simp: fg)
   1.165 +  show "P (\<lambda>x. ?h (t, x))" if "t \<in> {0..1}" for t
   1.166 +    by (cases "t = 1") (simp_all add: assms)
   1.167 +qed auto
   1.168 +
   1.169 +lemma homotopic_with_imp_subset1:
   1.170 +     "homotopic_with_canon P X Y f g \<Longrightarrow> f ` X \<subseteq> Y"
   1.171 +  by (simp add: homotopic_with_def image_subset_iff) (metis atLeastAtMost_iff order_refl zero_le_one)
   1.172 +
   1.173 +lemma homotopic_with_imp_subset2:
   1.174 +     "homotopic_with_canon P X Y f g \<Longrightarrow> g ` X \<subseteq> Y"
   1.175 +  by (simp add: homotopic_with_def image_subset_iff) (metis atLeastAtMost_iff order_refl zero_le_one)
   1.176 +
   1.177 +lemma homotopic_with_subset_left:
   1.178 +     "\<lbrakk>homotopic_with_canon P X Y f g; Z \<subseteq> X\<rbrakk> \<Longrightarrow> homotopic_with_canon P Z Y f g"
   1.179 +  apply (simp add: homotopic_with_def)
   1.180 +  apply (fast elim!: continuous_on_subset ex_forward)
   1.181 +  done
   1.182 +
   1.183 +lemma homotopic_with_subset_right:
   1.184 +     "\<lbrakk>homotopic_with_canon P X Y f g; Y \<subseteq> Z\<rbrakk> \<Longrightarrow> homotopic_with_canon P X Z f g"
   1.185 +  apply (simp add: homotopic_with_def)
   1.186 +  apply (fast elim!: continuous_on_subset ex_forward)
   1.187    done
   1.188  
   1.189 -
   1.190 -lemma image_Pair_const: "(\<lambda>x. (x, c)) ` A = A \<times> {c}"
   1.191 -  by auto
   1.192 -
   1.193 -lemma homotopic_constant_maps:
   1.194 -   "homotopic_with (\<lambda>x. True) s t (\<lambda>x. a) (\<lambda>x. b) \<longleftrightarrow> s = {} \<or> path_component t a b"
   1.195 -proof (cases "s = {} \<or> t = {}")
   1.196 -  case True with continuous_on_const show ?thesis
   1.197 -    by (auto simp: homotopic_with path_component_def)
   1.198 -next
   1.199 -  case False
   1.200 -  then obtain c where "c \<in> s" by blast
   1.201 +subsection\<open>Homotopy with P is an equivalence relation\<close>
   1.202 +
   1.203 +text \<open>(on continuous functions mapping X into Y that satisfy P, though this only affects reflexivity)\<close>
   1.204 +
   1.205 +lemma homotopic_with_refl [simp]: "homotopic_with P X Y f f \<longleftrightarrow> continuous_map X Y f \<and> P f"
   1.206 +  by (auto simp: homotopic_with_imp_continuous_maps intro: homotopic_with_equal dest: homotopic_with_imp_property)
   1.207 +
   1.208 +lemma homotopic_with_symD:
   1.209 +    assumes "homotopic_with P X Y f g"
   1.210 +      shows "homotopic_with P X Y g f"
   1.211 +proof -
   1.212 +  let ?I01 = "subtopology euclideanreal {0..1}"
   1.213 +  let ?j = "\<lambda>y. (1 - fst y, snd y)"
   1.214 +  have 1: "continuous_map (prod_topology ?I01 X) (prod_topology euclideanreal X) ?j"
   1.215 +    apply (intro continuous_intros)
   1.216 +    apply (simp_all add: prod_topology_subtopology continuous_map_from_subtopology [OF continuous_map_fst])
   1.217 +    done
   1.218 +  have *: "continuous_map (prod_topology ?I01 X) (prod_topology ?I01 X) ?j"
   1.219 +  proof -
   1.220 +    have "continuous_map (prod_topology ?I01 X) (subtopology (prod_topology euclideanreal X) ({0..1} \<times> topspace X)) ?j"
   1.221 +      by (simp add: continuous_map_into_subtopology [OF 1] image_subset_iff)
   1.222 +    then show ?thesis
   1.223 +      by (simp add: prod_topology_subtopology(1))
   1.224 +  qed
   1.225    show ?thesis
   1.226 -  proof
   1.227 -    assume "homotopic_with (\<lambda>x. True) s t (\<lambda>x. a) (\<lambda>x. b)"
   1.228 -    then obtain h :: "real \<times> 'a \<Rightarrow> 'b"
   1.229 -        where conth: "continuous_on ({0..1} \<times> s) h"
   1.230 -          and h: "h ` ({0..1} \<times> s) \<subseteq> t" "(\<forall>x\<in>s. h (0, x) = a)" "(\<forall>x\<in>s. h (1, x) = b)"
   1.231 -      by (auto simp: homotopic_with)
   1.232 -    have "continuous_on {0..1} (h \<circ> (\<lambda>t. (t, c)))"
   1.233 -      apply (rule continuous_intros conth | simp add: image_Pair_const)+
   1.234 -      apply (blast intro:  \<open>c \<in> s\<close> continuous_on_subset [OF conth])
   1.235 -      done
   1.236 -    with \<open>c \<in> s\<close> h show "s = {} \<or> path_component t a b"
   1.237 -      apply (simp_all add: homotopic_with path_component_def, auto)
   1.238 -      apply (drule_tac x="h \<circ> (\<lambda>t. (t, c))" in spec)
   1.239 -      apply (auto simp: pathstart_def pathfinish_def path_image_def path_def)
   1.240 -      done
   1.241 -  next
   1.242 -    assume "s = {} \<or> path_component t a b"
   1.243 -    with False show "homotopic_with (\<lambda>x. True) s t (\<lambda>x. a) (\<lambda>x. b)"
   1.244 -      apply (clarsimp simp: homotopic_with path_component_def pathstart_def pathfinish_def path_image_def path_def)
   1.245 -      apply (rule_tac x="g \<circ> fst" in exI)
   1.246 -      apply (rule conjI continuous_intros | force)+
   1.247 +    using assms
   1.248 +    apply (clarsimp simp add: homotopic_with_def)
   1.249 +    apply (rename_tac h)
   1.250 +    apply (rule_tac x="h \<circ> (\<lambda>y. (1 - fst y, snd y))" in exI)
   1.251 +    apply (simp add: continuous_map_compose [OF *])
   1.252 +    done
   1.253 +qed
   1.254 +
   1.255 +lemma homotopic_with_sym:
   1.256 +   "homotopic_with P X Y f g \<longleftrightarrow> homotopic_with P X Y g f"
   1.257 +  by (metis homotopic_with_symD)
   1.258 +
   1.259 +proposition homotopic_with_trans:
   1.260 +    assumes "homotopic_with P X Y f g"  "homotopic_with P X Y g h"
   1.261 +    shows "homotopic_with P X Y f h"
   1.262 +proof -
   1.263 +  let ?X01 = "prod_topology (subtopology euclideanreal {0..1}) X"
   1.264 +  obtain k1 k2
   1.265 +    where contk1: "continuous_map ?X01 Y k1" and contk2: "continuous_map ?X01 Y k2"
   1.266 +      and k12: "\<forall>x. k1 (1, x) = g x" "\<forall>x. k2 (0, x) = g x"
   1.267 +      "\<forall>x. k1 (0, x) = f x" "\<forall>x. k2 (1, x) = h x"
   1.268 +      and P:   "\<forall>t\<in>{0..1}. P (\<lambda>x. k1 (t, x))" "\<forall>t\<in>{0..1}. P (\<lambda>x. k2 (t, x))"
   1.269 +    using assms by (auto simp: homotopic_with_def)
   1.270 +  define k where "k \<equiv> \<lambda>y. if fst y \<le> 1/2
   1.271 +                             then (k1 \<circ> (\<lambda>x. (2 *\<^sub>R fst x, snd x))) y
   1.272 +                             else (k2 \<circ> (\<lambda>x. (2 *\<^sub>R fst x -1, snd x))) y"
   1.273 +  have keq: "k1 (2 * u, v) = k2 (2 * u -1, v)" if "u = 1/2"  for u v
   1.274 +    by (simp add: k12 that)
   1.275 +  show ?thesis
   1.276 +    unfolding homotopic_with_def
   1.277 +  proof (intro exI conjI)
   1.278 +    show "continuous_map ?X01 Y k"
   1.279 +      unfolding k_def
   1.280 +    proof (rule continuous_map_cases_le)
   1.281 +      show fst: "continuous_map ?X01 euclideanreal fst"
   1.282 +        using continuous_map_fst continuous_map_in_subtopology by blast
   1.283 +      show "continuous_map ?X01 euclideanreal (\<lambda>x. 1/2)"
   1.284 +        by simp
   1.285 +      show "continuous_map (subtopology ?X01 {y \<in> topspace ?X01. fst y \<le> 1/2}) Y
   1.286 +               (k1 \<circ> (\<lambda>x. (2 *\<^sub>R fst x, snd x)))"
   1.287 +        apply (rule fst continuous_map_compose [OF _ contk1] continuous_intros continuous_map_into_subtopology | simp)+
   1.288 +          apply (intro continuous_intros fst continuous_map_from_subtopology)
   1.289 +         apply (force simp: prod_topology_subtopology)
   1.290 +        using continuous_map_snd continuous_map_from_subtopology by blast
   1.291 +      show "continuous_map (subtopology ?X01 {y \<in> topspace ?X01. 1/2 \<le> fst y}) Y
   1.292 +               (k2 \<circ> (\<lambda>x. (2 *\<^sub>R fst x -1, snd x)))"
   1.293 +        apply (rule fst continuous_map_compose [OF _ contk2] continuous_intros continuous_map_into_subtopology | simp)+
   1.294 +          apply (rule continuous_intros fst continuous_map_from_subtopology | simp)+
   1.295 +         apply (force simp: topspace_subtopology prod_topology_subtopology)
   1.296 +        using continuous_map_snd  continuous_map_from_subtopology by blast
   1.297 +      show "(k1 \<circ> (\<lambda>x. (2 *\<^sub>R fst x, snd x))) y = (k2 \<circ> (\<lambda>x. (2 *\<^sub>R fst x -1, snd x))) y"
   1.298 +        if "y \<in> topspace ?X01" and "fst y = 1/2" for y
   1.299 +        using that by (simp add: keq)
   1.300 +    qed
   1.301 +    show "\<forall>x. k (0, x) = f x"
   1.302 +      by (simp add: k12 k_def)
   1.303 +    show "\<forall>x. k (1, x) = h x"
   1.304 +      by (simp add: k12 k_def)
   1.305 +    show "\<forall>t\<in>{0..1}. P (\<lambda>x. k (t, x))"
   1.306 +      using P
   1.307 +      apply (clarsimp simp add: k_def)
   1.308 +      apply (case_tac "t \<le> 1/2", auto)
   1.309        done
   1.310    qed
   1.311  qed
   1.312  
   1.313 -
   1.314 -subsection%unimportant\<open>Trivial properties\<close>
   1.315 -
   1.316 -lemma homotopic_with_imp_property: "homotopic_with P X Y f g \<Longrightarrow> P f \<and> P g"
   1.317 -  unfolding homotopic_with_def Ball_def
   1.318 +lemma homotopic_with_id2: 
   1.319 +  "(\<And>x. x \<in> topspace X \<Longrightarrow> g (f x) = x) \<Longrightarrow> homotopic_with (\<lambda>x. True) X X (g \<circ> f) id"
   1.320 +  by (metis comp_apply continuous_map_id eq_id_iff homotopic_with_equal homotopic_with_symD)
   1.321 +
   1.322 +subsection\<open>Continuity lemmas\<close>
   1.323 +
   1.324 +lemma homotopic_with_compose_continuous_map_left:
   1.325 +  "\<lbrakk>homotopic_with p X1 X2 f g; continuous_map X2 X3 h; \<And>j. p j \<Longrightarrow> q(h \<circ> j)\<rbrakk>
   1.326 +   \<Longrightarrow> homotopic_with q X1 X3 (h \<circ> f) (h \<circ> g)"
   1.327 +  unfolding homotopic_with_def
   1.328    apply clarify
   1.329 -  apply (frule_tac x=0 in spec)
   1.330 -  apply (drule_tac x=1 in spec, auto)
   1.331 +  apply (rename_tac k)
   1.332 +  apply (rule_tac x="h \<circ> k" in exI)
   1.333 +  apply (rule conjI continuous_map_compose | simp add: o_def)+
   1.334    done
   1.335  
   1.336 -lemma continuous_on_o_Pair: "\<lbrakk>continuous_on (T \<times> X) h; t \<in> T\<rbrakk> \<Longrightarrow> continuous_on X (h \<circ> Pair t)"
   1.337 -  by (fast intro: continuous_intros elim!: continuous_on_subset)
   1.338 -
   1.339 -lemma homotopic_with_imp_continuous:
   1.340 -    assumes "homotopic_with P X Y f g"
   1.341 -    shows "continuous_on X f \<and> continuous_on X g"
   1.342 +lemma homotopic_compose_continuous_map_left:
   1.343 +   "\<lbrakk>homotopic_with (\<lambda>k. True) X1 X2 f g; continuous_map X2 X3 h\<rbrakk>
   1.344 +        \<Longrightarrow> homotopic_with (\<lambda>k. True) X1 X3 (h \<circ> f) (h \<circ> g)"
   1.345 +  by (simp add: homotopic_with_compose_continuous_map_left)
   1.346 +
   1.347 +lemma homotopic_with_compose_continuous_map_right:
   1.348 +  assumes hom: "homotopic_with p X2 X3 f g" and conth: "continuous_map X1 X2 h"
   1.349 +    and q: "\<And>j. p j \<Longrightarrow> q(j \<circ> h)"
   1.350 +  shows "homotopic_with q X1 X3 (f \<circ> h) (g \<circ> h)"
   1.351  proof -
   1.352 -  obtain h :: "real \<times> 'a \<Rightarrow> 'b"
   1.353 -    where conth: "continuous_on ({0..1} \<times> X) h"
   1.354 -      and h: "\<forall>x. h (0, x) = f x" "\<forall>x. h (1, x) = g x"
   1.355 -    using assms by (auto simp: homotopic_with_def)
   1.356 -  have *: "t \<in> {0..1} \<Longrightarrow> continuous_on X (h \<circ> (\<lambda>x. (t,x)))" for t
   1.357 -    by (rule continuous_intros continuous_on_subset [OF conth] | force)+
   1.358 +  obtain k
   1.359 +    where contk: "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X2) X3 k"
   1.360 +      and k: "\<forall>x. k (0, x) = f x" "\<forall>x. k (1, x) = g x" and p: "\<And>t. t\<in>{0..1} \<Longrightarrow> p (\<lambda>x. k (t, x))"
   1.361 +    using hom unfolding homotopic_with_def by blast
   1.362 +  have hsnd: "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X1) X2 (h \<circ> snd)"
   1.363 +    by (rule continuous_map_compose [OF continuous_map_snd conth])
   1.364 +  let ?h = "k \<circ> (\<lambda>(t,x). (t,h x))"
   1.365    show ?thesis
   1.366 -    using h *[of 0] *[of 1] by auto
   1.367 +    unfolding homotopic_with_def
   1.368 +  proof (intro exI conjI allI ballI)
   1.369 +    have "continuous_map (prod_topology (top_of_set {0..1}) X1)
   1.370 +     (prod_topology (top_of_set {0..1::real}) X2) (\<lambda>(t, x). (t, h x))"
   1.371 +      by (metis (mono_tags, lifting) case_prod_beta' comp_def continuous_map_eq continuous_map_fst continuous_map_pairedI hsnd)
   1.372 +    then show "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X1) X3 ?h"
   1.373 +      by (intro conjI continuous_map_compose [OF _ contk])
   1.374 +    show "q (\<lambda>x. ?h (t, x))" if "t \<in> {0..1}" for t
   1.375 +      using q [OF p [OF that]] by (simp add: o_def)
   1.376 +  qed (auto simp: k)
   1.377  qed
   1.378  
   1.379 -proposition homotopic_with_imp_subset1:
   1.380 -     "homotopic_with P X Y f g \<Longrightarrow> f ` X \<subseteq> Y"
   1.381 -  by (simp add: homotopic_with_def image_subset_iff) (metis atLeastAtMost_iff order_refl zero_le_one)
   1.382 -
   1.383 -proposition homotopic_with_imp_subset2:
   1.384 -     "homotopic_with P X Y f g \<Longrightarrow> g ` X \<subseteq> Y"
   1.385 -  by (simp add: homotopic_with_def image_subset_iff) (metis atLeastAtMost_iff order_refl zero_le_one)
   1.386 -
   1.387 -proposition homotopic_with_mono:
   1.388 -    assumes hom: "homotopic_with P X Y f g"
   1.389 -        and Q: "\<And>h. \<lbrakk>continuous_on X h; image h X \<subseteq> Y \<and> P h\<rbrakk> \<Longrightarrow> Q h"
   1.390 -      shows "homotopic_with Q X Y f g"
   1.391 -  using hom
   1.392 -  apply (simp add: homotopic_with_def)
   1.393 -  apply (erule ex_forward)
   1.394 -  apply (force simp: intro!: Q dest: continuous_on_o_Pair)
   1.395 -  done
   1.396 -
   1.397 -proposition homotopic_with_subset_left:
   1.398 -     "\<lbrakk>homotopic_with P X Y f g; Z \<subseteq> X\<rbrakk> \<Longrightarrow> homotopic_with P Z Y f g"
   1.399 -  apply (simp add: homotopic_with_def)
   1.400 -  apply (fast elim!: continuous_on_subset ex_forward)
   1.401 -  done
   1.402 -
   1.403 -proposition homotopic_with_subset_right:
   1.404 -     "\<lbrakk>homotopic_with P X Y f g; Y \<subseteq> Z\<rbrakk> \<Longrightarrow> homotopic_with P X Z f g"
   1.405 -  apply (simp add: homotopic_with_def)
   1.406 -  apply (fast elim!: continuous_on_subset ex_forward)
   1.407 -  done
   1.408 +lemma homotopic_compose_continuous_map_right:
   1.409 +   "\<lbrakk>homotopic_with (\<lambda>k. True) X2 X3 f g; continuous_map X1 X2 h\<rbrakk>
   1.410 +        \<Longrightarrow> homotopic_with (\<lambda>k. True) X1 X3 (f \<circ> h) (g \<circ> h)"
   1.411 +  by (meson homotopic_with_compose_continuous_map_right)
   1.412 +
   1.413 +corollary homotopic_compose:
   1.414 +      shows "\<lbrakk>homotopic_with (\<lambda>x. True) X Y f f'; homotopic_with (\<lambda>x. True) Y Z g g'\<rbrakk>
   1.415 +             \<Longrightarrow> homotopic_with (\<lambda>x. True) X Z (g \<circ> f) (g' \<circ> f')"
   1.416 +  apply (rule homotopic_with_trans [where g = "g \<circ> f'"])
   1.417 +  apply (simp add: homotopic_compose_continuous_map_left homotopic_with_imp_continuous_maps)
   1.418 +  by (simp add: homotopic_compose_continuous_map_right homotopic_with_imp_continuous_maps)
   1.419 +
   1.420 +
   1.421  
   1.422  proposition homotopic_with_compose_continuous_right:
   1.423 -    "\<lbrakk>homotopic_with (\<lambda>f. p (f \<circ> h)) X Y f g; continuous_on W h; h ` W \<subseteq> X\<rbrakk>
   1.424 -     \<Longrightarrow> homotopic_with p W Y (f \<circ> h) (g \<circ> h)"
   1.425 +    "\<lbrakk>homotopic_with_canon (\<lambda>f. p (f \<circ> h)) X Y f g; continuous_on W h; h ` W \<subseteq> X\<rbrakk>
   1.426 +     \<Longrightarrow> homotopic_with_canon p W Y (f \<circ> h) (g \<circ> h)"
   1.427    apply (clarsimp simp add: homotopic_with_def)
   1.428    apply (rename_tac k)
   1.429    apply (rule_tac x="k \<circ> (\<lambda>y. (fst y, h (snd y)))" in exI)
   1.430 @@ -180,13 +307,13 @@
   1.431    done
   1.432  
   1.433  proposition homotopic_compose_continuous_right:
   1.434 -     "\<lbrakk>homotopic_with (\<lambda>f. True) X Y f g; continuous_on W h; h ` W \<subseteq> X\<rbrakk>
   1.435 -      \<Longrightarrow> homotopic_with (\<lambda>f. True) W Y (f \<circ> h) (g \<circ> h)"
   1.436 +     "\<lbrakk>homotopic_with_canon (\<lambda>f. True) X Y f g; continuous_on W h; h ` W \<subseteq> X\<rbrakk>
   1.437 +      \<Longrightarrow> homotopic_with_canon (\<lambda>f. True) W Y (f \<circ> h) (g \<circ> h)"
   1.438    using homotopic_with_compose_continuous_right by fastforce
   1.439  
   1.440  proposition homotopic_with_compose_continuous_left:
   1.441 -     "\<lbrakk>homotopic_with (\<lambda>f. p (h \<circ> f)) X Y f g; continuous_on Y h; h ` Y \<subseteq> Z\<rbrakk>
   1.442 -      \<Longrightarrow> homotopic_with p X Z (h \<circ> f) (h \<circ> g)"
   1.443 +     "\<lbrakk>homotopic_with_canon (\<lambda>f. p (h \<circ> f)) X Y f g; continuous_on Y h; h ` Y \<subseteq> Z\<rbrakk>
   1.444 +      \<Longrightarrow> homotopic_with_canon p X Z (h \<circ> f) (h \<circ> g)"
   1.445    apply (clarsimp simp add: homotopic_with_def)
   1.446    apply (rename_tac k)
   1.447    apply (rule_tac x="h \<circ> k" in exI)
   1.448 @@ -196,150 +323,171 @@
   1.449    done
   1.450  
   1.451  proposition homotopic_compose_continuous_left:
   1.452 -   "\<lbrakk>homotopic_with (\<lambda>_. True) X Y f g;
   1.453 +   "\<lbrakk>homotopic_with_canon (\<lambda>_. True) X Y f g;
   1.454       continuous_on Y h; h ` Y \<subseteq> Z\<rbrakk>
   1.455 -    \<Longrightarrow> homotopic_with (\<lambda>f. True) X Z (h \<circ> f) (h \<circ> g)"
   1.456 +    \<Longrightarrow> homotopic_with_canon (\<lambda>f. True) X Z (h \<circ> f) (h \<circ> g)"
   1.457    using homotopic_with_compose_continuous_left by fastforce
   1.458  
   1.459 -proposition homotopic_with_Pair:
   1.460 -   assumes hom: "homotopic_with p s t f g" "homotopic_with p' s' t' f' g'"
   1.461 -       and q: "\<And>f g. \<lbrakk>p f; p' g\<rbrakk> \<Longrightarrow> q(\<lambda>(x,y). (f x, g y))"
   1.462 -     shows "homotopic_with q (s \<times> s') (t \<times> t')
   1.463 -                  (\<lambda>(x,y). (f x, f' y)) (\<lambda>(x,y). (g x, g' y))"
   1.464 -  using hom
   1.465 -  apply (clarsimp simp add: homotopic_with_def)
   1.466 -  apply (rename_tac k k')
   1.467 -  apply (rule_tac x="\<lambda>z. ((k \<circ> (\<lambda>x. (fst x, fst (snd x)))) z, (k' \<circ> (\<lambda>x. (fst x, snd (snd x)))) z)" in exI)
   1.468 -  apply (rule conjI continuous_intros | erule continuous_on_subset | clarsimp)+
   1.469 -  apply (auto intro!: q [unfolded case_prod_unfold])
   1.470 -  done
   1.471 -
   1.472 -lemma homotopic_on_empty [simp]: "homotopic_with (\<lambda>x. True) {} t f g"
   1.473 -  by (metis continuous_on_def empty_iff homotopic_with_equal image_subset_iff)
   1.474 -
   1.475 -
   1.476 -text\<open>Homotopy with P is an equivalence relation (on continuous functions mapping X into Y that satisfy P,
   1.477 -     though this only affects reflexivity.\<close>
   1.478 -
   1.479 -
   1.480 -proposition homotopic_with_refl:
   1.481 -   "homotopic_with P X Y f f \<longleftrightarrow> continuous_on X f \<and> image f X \<subseteq> Y \<and> P f"
   1.482 -  apply (rule iffI)
   1.483 -  using homotopic_with_imp_continuous homotopic_with_imp_property homotopic_with_imp_subset2 apply blast
   1.484 -  apply (simp add: homotopic_with_def)
   1.485 -  apply (rule_tac x="f \<circ> snd" in exI)
   1.486 -  apply (rule conjI continuous_intros | force)+
   1.487 -  done
   1.488 -
   1.489 -lemma homotopic_with_symD:
   1.490 -  fixes X :: "'a::real_normed_vector set"
   1.491 -    assumes "homotopic_with P X Y f g"
   1.492 -      shows "homotopic_with P X Y g f"
   1.493 -  using assms
   1.494 -  apply (clarsimp simp add: homotopic_with_def)
   1.495 -  apply (rename_tac h)
   1.496 -  apply (rule_tac x="h \<circ> (\<lambda>y. (1 - fst y, snd y))" in exI)
   1.497 -  apply (rule conjI continuous_intros | erule continuous_on_subset | force simp: image_subset_iff)+
   1.498 +lemma homotopic_from_subtopology:
   1.499 +   "homotopic_with P X X' f g \<Longrightarrow> homotopic_with P (subtopology X s) X' f g"
   1.500 +  unfolding homotopic_with_def
   1.501 +  apply (erule ex_forward)
   1.502 +  by (simp add: continuous_map_from_subtopology prod_topology_subtopology(2))
   1.503 +
   1.504 +lemma homotopic_on_emptyI:
   1.505 +    assumes "topspace X = {}" "P f" "P g"
   1.506 +    shows "homotopic_with P X X' f g"
   1.507 +  unfolding homotopic_with_def
   1.508 +proof (intro exI conjI ballI)
   1.509 +  show "P (\<lambda>x. (\<lambda>(t,x). if t = 0 then f x else g x) (t, x))" if "t \<in> {0..1}" for t::real
   1.510 +    by (cases "t = 0", auto simp: assms)
   1.511 +qed (auto simp: continuous_map_atin assms)
   1.512 +
   1.513 +lemma homotopic_on_empty:
   1.514 +   "topspace X = {} \<Longrightarrow> (homotopic_with P X X' f g \<longleftrightarrow> P f \<and> P g)"
   1.515 +  using homotopic_on_emptyI homotopic_with_imp_property by metis
   1.516 +
   1.517 +lemma homotopic_with_canon_on_empty [simp]: "homotopic_with_canon (\<lambda>x. True) {} t f g"
   1.518 +  by (auto intro: homotopic_with_equal)
   1.519 +
   1.520 +lemma homotopic_constant_maps:
   1.521 +   "homotopic_with (\<lambda>x. True) X X' (\<lambda>x. a) (\<lambda>x. b) \<longleftrightarrow>
   1.522 +    topspace X = {} \<or> path_component_of X' a b" (is "?lhs = ?rhs")
   1.523 +proof (cases "topspace X = {}")
   1.524 +  case False
   1.525 +  then obtain c where c: "c \<in> topspace X"
   1.526 +    by blast
   1.527 +  have "\<exists>g. continuous_map (top_of_set {0..1::real}) X' g \<and> g 0 = a \<and> g 1 = b"
   1.528 +    if "x \<in> topspace X" and hom: "homotopic_with (\<lambda>x. True) X X' (\<lambda>x. a) (\<lambda>x. b)" for x
   1.529 +  proof -
   1.530 +    obtain h :: "real \<times> 'a \<Rightarrow> 'b"
   1.531 +      where conth: "continuous_map (prod_topology (top_of_set {0..1}) X) X' h"
   1.532 +        and h: "\<And>x. h (0, x) = a" "\<And>x. h (1, x) = b"
   1.533 +      using hom by (auto simp: homotopic_with_def)
   1.534 +    have cont: "continuous_map (top_of_set {0..1}) X' (h \<circ> (\<lambda>t. (t, c)))"
   1.535 +      apply (rule continuous_map_compose [OF _ conth])
   1.536 +      apply (rule continuous_intros c | simp)+
   1.537 +      done
   1.538 +    then show ?thesis
   1.539 +      by (force simp: h)
   1.540 +  qed
   1.541 +  moreover have "homotopic_with (\<lambda>x. True) X X' (\<lambda>x. g 0) (\<lambda>x. g 1)"
   1.542 +    if "x \<in> topspace X" "a = g 0" "b = g 1" "continuous_map (top_of_set {0..1}) X' g"
   1.543 +    for x and g :: "real \<Rightarrow> 'b"
   1.544 +    unfolding homotopic_with_def
   1.545 +    by (force intro!: continuous_map_compose continuous_intros c that)
   1.546 +  ultimately show ?thesis
   1.547 +    using False by (auto simp: path_component_of_def pathin_def)
   1.548 +qed (simp add: homotopic_on_empty)
   1.549 +
   1.550 +proposition homotopic_with_eq:
   1.551 +   assumes h: "homotopic_with P X Y f g"
   1.552 +       and f': "\<And>x. x \<in> topspace X \<Longrightarrow> f' x = f x"
   1.553 +       and g': "\<And>x. x \<in> topspace X \<Longrightarrow> g' x = g x"
   1.554 +       and P:  "(\<And>h k. (\<And>x. x \<in> topspace X \<Longrightarrow> h x = k x) \<Longrightarrow> P h \<longleftrightarrow> P k)"
   1.555 +   shows "homotopic_with P X Y f' g'"
   1.556 +  using h unfolding homotopic_with_def
   1.557 +  apply safe
   1.558 +  apply (rule_tac x="\<lambda>(u,v). if v \<in> topspace X then h(u,v) else if u = 0 then f' v else g' v" in exI)
   1.559 +  apply (simp add: f' g', safe)
   1.560 +  apply (fastforce intro: continuous_map_eq)
   1.561 +  apply (subst P; fastforce)
   1.562    done
   1.563  
   1.564 -proposition homotopic_with_sym:
   1.565 -    fixes X :: "'a::real_normed_vector set"
   1.566 -    shows "homotopic_with P X Y f g \<longleftrightarrow> homotopic_with P X Y g f"
   1.567 -  using homotopic_with_symD by blast
   1.568 -
   1.569 -lemma split_01: "{0..1::real} = {0..1/2} \<union> {1/2..1}"
   1.570 -  by force
   1.571 -
   1.572 -lemma split_01_prod: "{0..1::real} \<times> X = ({0..1/2} \<times> X) \<union> ({1/2..1} \<times> X)"
   1.573 -  by force
   1.574 -
   1.575 -proposition homotopic_with_trans:
   1.576 -    fixes X :: "'a::real_normed_vector set"
   1.577 -    assumes "homotopic_with P X Y f g" and "homotopic_with P X Y g h"
   1.578 -      shows "homotopic_with P X Y f h"
   1.579 +lemma homotopic_with_prod_topology:
   1.580 +  assumes "homotopic_with p X1 Y1 f f'" and "homotopic_with q X2 Y2 g g'"
   1.581 +    and r: "\<And>i j. \<lbrakk>p i; q j\<rbrakk> \<Longrightarrow> r(\<lambda>(x,y). (i x, j y))"
   1.582 +  shows "homotopic_with r (prod_topology X1 X2) (prod_topology Y1 Y2)
   1.583 +                          (\<lambda>z. (f(fst z),g(snd z))) (\<lambda>z. (f'(fst z), g'(snd z)))"
   1.584  proof -
   1.585 -  have clo1: "closedin (top_of_set ({0..1/2} \<times> X \<union> {1/2..1} \<times> X)) ({0..1/2::real} \<times> X)"
   1.586 -    apply (simp add: closedin_closed split_01_prod [symmetric])
   1.587 -    apply (rule_tac x="{0..1/2} \<times> UNIV" in exI)
   1.588 -    apply (force simp: closed_Times)
   1.589 -    done
   1.590 -  have clo2: "closedin (top_of_set ({0..1/2} \<times> X \<union> {1/2..1} \<times> X)) ({1/2..1::real} \<times> X)"
   1.591 -    apply (simp add: closedin_closed split_01_prod [symmetric])
   1.592 -    apply (rule_tac x="{1/2..1} \<times> UNIV" in exI)
   1.593 -    apply (force simp: closed_Times)
   1.594 -    done
   1.595 -  { fix k1 k2:: "real \<times> 'a \<Rightarrow> 'b"
   1.596 -    assume cont: "continuous_on ({0..1} \<times> X) k1" "continuous_on ({0..1} \<times> X) k2"
   1.597 -       and Y: "k1 ` ({0..1} \<times> X) \<subseteq> Y" "k2 ` ({0..1} \<times> X) \<subseteq> Y"
   1.598 -       and geq: "\<forall>x. k1 (1, x) = g x" "\<forall>x. k2 (0, x) = g x"
   1.599 -       and k12: "\<forall>x. k1 (0, x) = f x" "\<forall>x. k2 (1, x) = h x"
   1.600 -       and P:   "\<forall>t\<in>{0..1}. P (\<lambda>x. k1 (t, x))" "\<forall>t\<in>{0..1}. P (\<lambda>x. k2 (t, x))"
   1.601 -    define k where "k y =
   1.602 -      (if fst y \<le> 1 / 2
   1.603 -       then (k1 \<circ> (\<lambda>x. (2 *\<^sub>R fst x, snd x))) y
   1.604 -       else (k2 \<circ> (\<lambda>x. (2 *\<^sub>R fst x -1, snd x))) y)" for y
   1.605 -    have keq: "k1 (2 * u, v) = k2 (2 * u - 1, v)" if "u = 1/2"  for u v
   1.606 -      by (simp add: geq that)
   1.607 -    have "continuous_on ({0..1} \<times> X) k"
   1.608 -      using cont
   1.609 -      apply (simp add: split_01_prod k_def)
   1.610 -      apply (rule clo1 clo2 continuous_on_cases_local continuous_intros | erule continuous_on_subset | simp add: linear image_subset_iff)+
   1.611 -      apply (force simp: keq)
   1.612 +  obtain h
   1.613 +    where h: "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X1) Y1 h"
   1.614 +      and h0: "\<And>x. h (0, x) = f x"
   1.615 +      and h1: "\<And>x. h (1, x) = f' x"
   1.616 +      and p: "\<And>t. \<lbrakk>0 \<le> t; t \<le> 1\<rbrakk> \<Longrightarrow> p (\<lambda>x. h (t,x))"
   1.617 +    using assms unfolding homotopic_with_def by auto
   1.618 +  obtain k
   1.619 +    where k: "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X2) Y2 k"
   1.620 +      and k0: "\<And>x. k (0, x) = g x"
   1.621 +      and k1: "\<And>x. k (1, x) = g' x"
   1.622 +      and q: "\<And>t. \<lbrakk>0 \<le> t; t \<le> 1\<rbrakk> \<Longrightarrow> q (\<lambda>x. k (t,x))"
   1.623 +    using assms unfolding homotopic_with_def by auto
   1.624 +  let ?hk = "\<lambda>(t,x,y). (h(t,x), k(t,y))"
   1.625 +  show ?thesis
   1.626 +    unfolding homotopic_with_def
   1.627 +  proof (intro conjI allI exI)
   1.628 +    show "continuous_map (prod_topology (subtopology euclideanreal {0..1}) (prod_topology X1 X2))
   1.629 +                         (prod_topology Y1 Y2) ?hk"
   1.630 +      unfolding continuous_map_pairwise case_prod_unfold
   1.631 +      by (rule conjI continuous_map_pairedI continuous_intros continuous_map_id [unfolded id_def]
   1.632 +          continuous_map_fst_of [unfolded o_def] continuous_map_snd_of [unfolded o_def]
   1.633 +          continuous_map_compose [OF _ h, unfolded o_def]
   1.634 +          continuous_map_compose [OF _ k, unfolded o_def])+
   1.635 +  next
   1.636 +    fix x
   1.637 +    show "?hk (0, x) = (f (fst x), g (snd x))" "?hk (1, x) = (f' (fst x), g' (snd x))"
   1.638 +      by (auto simp: case_prod_beta h0 k0 h1 k1)
   1.639 +  qed (auto simp: p q r)
   1.640 +qed
   1.641 +
   1.642 +
   1.643 +lemma homotopic_with_product_topology:
   1.644 +  assumes ht: "\<And>i. i \<in> I \<Longrightarrow> homotopic_with (p i) (X i) (Y i) (f i) (g i)"
   1.645 +    and pq: "\<And>h. (\<And>i. i \<in> I \<Longrightarrow> p i (h i)) \<Longrightarrow> q(\<lambda>x. (\<lambda>i\<in>I. h i (x i)))"
   1.646 +  shows "homotopic_with q (product_topology X I) (product_topology Y I)
   1.647 +                          (\<lambda>z. (\<lambda>i\<in>I. (f i) (z i))) (\<lambda>z. (\<lambda>i\<in>I. (g i) (z i)))"
   1.648 +proof -
   1.649 +  obtain h
   1.650 +    where h: "\<And>i. i \<in> I \<Longrightarrow> continuous_map (prod_topology (subtopology euclideanreal {0..1}) (X i)) (Y i) (h i)"
   1.651 +      and h0: "\<And>i x. i \<in> I \<Longrightarrow> h i (0, x) = f i x"
   1.652 +      and h1: "\<And>i x. i \<in> I \<Longrightarrow> h i (1, x) = g i x"
   1.653 +      and p: "\<And>i t. \<lbrakk>i \<in> I; t \<in> {0..1}\<rbrakk> \<Longrightarrow> p i (\<lambda>x. h i (t,x))"
   1.654 +    using ht unfolding homotopic_with_def by metis
   1.655 +  show ?thesis
   1.656 +    unfolding homotopic_with_def
   1.657 +  proof (intro conjI allI exI)
   1.658 +    let ?h = "\<lambda>(t,z). \<lambda>i\<in>I. h i (t,z i)"
   1.659 +    have "continuous_map (prod_topology (subtopology euclideanreal {0..1}) (product_topology X I))
   1.660 +                         (Y i) (\<lambda>x. h i (fst x, snd x i))" if "i \<in> I" for i
   1.661 +      unfolding continuous_map_pairwise case_prod_unfold
   1.662 +      apply (intro conjI that  continuous_intros continuous_map_compose [OF _ h, unfolded o_def])
   1.663 +      using continuous_map_componentwise continuous_map_snd that apply fastforce
   1.664        done
   1.665 -    moreover have "k ` ({0..1} \<times> X) \<subseteq> Y"
   1.666 -      using Y by (force simp: k_def)
   1.667 -    moreover have "\<forall>x. k (0, x) = f x"
   1.668 -      by (simp add: k_def k12)
   1.669 -    moreover have "(\<forall>x. k (1, x) = h x)"
   1.670 -      by (simp add: k_def k12)
   1.671 -    moreover have "\<forall>t\<in>{0..1}. P (\<lambda>x. k (t, x))"
   1.672 -      using P
   1.673 -      apply (clarsimp simp add: k_def)
   1.674 -      apply (case_tac "t \<le> 1/2", auto)
   1.675 -      done
   1.676 -    ultimately have *: "\<exists>k :: real \<times> 'a \<Rightarrow> 'b.
   1.677 -                       continuous_on ({0..1} \<times> X) k \<and> k ` ({0..1} \<times> X) \<subseteq> Y \<and>
   1.678 -                       (\<forall>x. k (0, x) = f x) \<and> (\<forall>x. k (1, x) = h x) \<and> (\<forall>t\<in>{0..1}. P (\<lambda>x. k (t, x)))"
   1.679 -      by blast
   1.680 -  } note * = this
   1.681 -  show ?thesis
   1.682 -    using assms by (auto intro: * simp add: homotopic_with_def)
   1.683 +    then show "continuous_map (prod_topology (subtopology euclideanreal {0..1}) (product_topology X I))
   1.684 +         (product_topology Y I) ?h"
   1.685 +      by (auto simp: continuous_map_componentwise case_prod_beta)
   1.686 +    show "?h (0, x) = (\<lambda>i\<in>I. f i (x i))" "?h (1, x) = (\<lambda>i\<in>I. g i (x i))" for x
   1.687 +      by (auto simp: case_prod_beta h0 h1)
   1.688 +    show "\<forall>t\<in>{0..1}. q (\<lambda>x. ?h (t, x))"
   1.689 +      by (force intro: p pq)
   1.690 +  qed
   1.691  qed
   1.692  
   1.693 -proposition homotopic_compose:
   1.694 -      fixes s :: "'a::real_normed_vector set"
   1.695 -      shows "\<lbrakk>homotopic_with (\<lambda>x. True) s t f f'; homotopic_with (\<lambda>x. True) t u g g'\<rbrakk>
   1.696 -             \<Longrightarrow> homotopic_with (\<lambda>x. True) s u (g \<circ> f) (g' \<circ> f')"
   1.697 -  apply (rule homotopic_with_trans [where g = "g \<circ> f'"])
   1.698 -  apply (metis homotopic_compose_continuous_left homotopic_with_imp_continuous homotopic_with_imp_subset1)
   1.699 -  by (metis homotopic_compose_continuous_right homotopic_with_imp_continuous homotopic_with_imp_subset2)
   1.700 -
   1.701 -
   1.702  text\<open>Homotopic triviality implicitly incorporates path-connectedness.\<close>
   1.703  lemma homotopic_triviality:
   1.704 -  fixes S :: "'a::real_normed_vector set"
   1.705    shows  "(\<forall>f g. continuous_on S f \<and> f ` S \<subseteq> T \<and>
   1.706                   continuous_on S g \<and> g ` S \<subseteq> T
   1.707 -                 \<longrightarrow> homotopic_with (\<lambda>x. True) S T f g) \<longleftrightarrow>
   1.708 +                 \<longrightarrow> homotopic_with_canon (\<lambda>x. True) S T f g) \<longleftrightarrow>
   1.709            (S = {} \<or> path_connected T) \<and>
   1.710 -          (\<forall>f. continuous_on S f \<and> f ` S \<subseteq> T \<longrightarrow> (\<exists>c. homotopic_with (\<lambda>x. True) S T f (\<lambda>x. c)))"
   1.711 +          (\<forall>f. continuous_on S f \<and> f ` S \<subseteq> T \<longrightarrow> (\<exists>c. homotopic_with_canon (\<lambda>x. True) S T f (\<lambda>x. c)))"
   1.712            (is "?lhs = ?rhs")
   1.713  proof (cases "S = {} \<or> T = {}")
   1.714 -  case True then show ?thesis by auto
   1.715 +  case True then show ?thesis
   1.716 +    by (auto simp: homotopic_on_emptyI)
   1.717  next
   1.718    case False show ?thesis
   1.719    proof
   1.720      assume LHS [rule_format]: ?lhs
   1.721      have pab: "path_component T a b" if "a \<in> T" "b \<in> T" for a b
   1.722      proof -
   1.723 -      have "homotopic_with (\<lambda>x. True) S T (\<lambda>x. a) (\<lambda>x. b)"
   1.724 +      have "homotopic_with_canon (\<lambda>x. True) S T (\<lambda>x. a) (\<lambda>x. b)"
   1.725          by (simp add: LHS continuous_on_const image_subset_iff that)
   1.726        then show ?thesis
   1.727 -        using False homotopic_constant_maps by blast
   1.728 +        using False homotopic_constant_maps [of "top_of_set S" "top_of_set T" a b] by auto
   1.729      qed
   1.730 -      moreover
   1.731 -    have "\<exists>c. homotopic_with (\<lambda>x. True) S T f (\<lambda>x. c)" if "continuous_on S f" "f ` S \<subseteq> T" for f
   1.732 -      by (metis (full_types) False LHS equals0I homotopic_constant_maps homotopic_with_imp_continuous homotopic_with_imp_subset2 pab that)
   1.733 +    moreover
   1.734 +    have "\<exists>c. homotopic_with_canon (\<lambda>x. True) S T f (\<lambda>x. c)" if "continuous_on S f" "f ` S \<subseteq> T" for f
   1.735 +      using False LHS continuous_on_const that by blast
   1.736      ultimately show ?rhs
   1.737        by (simp add: path_connected_component)
   1.738    next
   1.739 @@ -350,15 +498,15 @@
   1.740      proof clarify
   1.741        fix f g
   1.742        assume "continuous_on S f" "f ` S \<subseteq> T" "continuous_on S g" "g ` S \<subseteq> T"
   1.743 -      obtain c d where c: "homotopic_with (\<lambda>x. True) S T f (\<lambda>x. c)" and d: "homotopic_with (\<lambda>x. True) S T g (\<lambda>x. d)"
   1.744 +      obtain c d where c: "homotopic_with_canon (\<lambda>x. True) S T f (\<lambda>x. c)" and d: "homotopic_with_canon (\<lambda>x. True) S T g (\<lambda>x. d)"
   1.745          using False \<open>continuous_on S f\<close> \<open>f ` S \<subseteq> T\<close>  RHS \<open>continuous_on S g\<close> \<open>g ` S \<subseteq> T\<close> by blast
   1.746        then have "c \<in> T" "d \<in> T"
   1.747 -        using False homotopic_with_imp_subset2 by fastforce+
   1.748 +        using False homotopic_with_imp_continuous_maps by fastforce+
   1.749        with T have "path_component T c d"
   1.750          using path_connected_component by blast
   1.751 -      then have "homotopic_with (\<lambda>x. True) S T (\<lambda>x. c) (\<lambda>x. d)"
   1.752 +      then have "homotopic_with_canon (\<lambda>x. True) S T (\<lambda>x. c) (\<lambda>x. d)"
   1.753          by (simp add: homotopic_constant_maps)
   1.754 -      with c d show "homotopic_with (\<lambda>x. True) S T f g"
   1.755 +      with c d show "homotopic_with_canon (\<lambda>x. True) S T f g"
   1.756          by (meson homotopic_with_symD homotopic_with_trans)
   1.757      qed
   1.758    qed
   1.759 @@ -371,7 +519,7 @@
   1.760  definition%important homotopic_paths :: "['a set, real \<Rightarrow> 'a, real \<Rightarrow> 'a::topological_space] \<Rightarrow> bool"
   1.761    where
   1.762       "homotopic_paths s p q \<equiv>
   1.763 -       homotopic_with (\<lambda>r. pathstart r = pathstart p \<and> pathfinish r = pathfinish p) {0..1} s p q"
   1.764 +       homotopic_with_canon (\<lambda>r. pathstart r = pathstart p \<and> pathfinish r = pathfinish p) {0..1} s p q"
   1.765  
   1.766  lemma homotopic_paths:
   1.767     "homotopic_paths s p q \<longleftrightarrow>
   1.768 @@ -393,14 +541,14 @@
   1.769  
   1.770  lemma homotopic_paths_imp_path:
   1.771       "homotopic_paths s p q \<Longrightarrow> path p \<and> path q"
   1.772 -  using homotopic_paths_def homotopic_with_imp_continuous path_def by blast
   1.773 +  using homotopic_paths_def homotopic_with_imp_continuous_maps path_def continuous_map_subtopology_eu by blast
   1.774  
   1.775  lemma homotopic_paths_imp_subset:
   1.776       "homotopic_paths s p q \<Longrightarrow> path_image p \<subseteq> s \<and> path_image q \<subseteq> s"
   1.777 -  by (simp add: homotopic_paths_def homotopic_with_imp_subset1 homotopic_with_imp_subset2 path_image_def)
   1.778 +  by (metis (mono_tags) continuous_map_subtopology_eu homotopic_paths_def homotopic_with_imp_continuous_maps path_image_def)
   1.779  
   1.780  proposition homotopic_paths_refl [simp]: "homotopic_paths s p p \<longleftrightarrow> path p \<and> path_image p \<subseteq> s"
   1.781 -by (simp add: homotopic_paths_def homotopic_with_refl path_def path_image_def)
   1.782 +  by (simp add: homotopic_paths_def path_def path_image_def)
   1.783  
   1.784  proposition homotopic_paths_sym: "homotopic_paths s p q \<Longrightarrow> homotopic_paths s q p"
   1.785    by (metis (mono_tags) homotopic_paths_def homotopic_paths_imp_pathfinish homotopic_paths_imp_pathstart homotopic_with_symD)
   1.786 @@ -409,10 +557,16 @@
   1.787    by (metis homotopic_paths_sym)
   1.788  
   1.789  proposition homotopic_paths_trans [trans]:
   1.790 -     "\<lbrakk>homotopic_paths s p q; homotopic_paths s q r\<rbrakk> \<Longrightarrow> homotopic_paths s p r"
   1.791 -  apply (simp add: homotopic_paths_def)
   1.792 -  apply (rule homotopic_with_trans, assumption)
   1.793 -  by (metis (mono_tags, lifting) homotopic_with_imp_property homotopic_with_mono)
   1.794 +  assumes "homotopic_paths s p q" "homotopic_paths s q r"
   1.795 +  shows "homotopic_paths s p r"
   1.796 +proof -
   1.797 +  have "pathstart q = pathstart p" "pathfinish q = pathfinish p"
   1.798 +    using assms by (simp_all add: homotopic_paths_imp_pathstart homotopic_paths_imp_pathfinish)
   1.799 +  then have "homotopic_with_canon (\<lambda>f. pathstart f = pathstart p \<and> pathfinish f = pathfinish p) {0..1} s q r"
   1.800 +    using \<open>homotopic_paths s q r\<close> homotopic_paths_def by force
   1.801 +  then show ?thesis
   1.802 +    using assms homotopic_paths_def homotopic_with_trans by blast
   1.803 +qed
   1.804  
   1.805  proposition homotopic_paths_eq:
   1.806       "\<lbrakk>path p; path_image p \<subseteq> s; \<And>t. t \<in> {0..1} \<Longrightarrow> p t = q t\<rbrakk> \<Longrightarrow> homotopic_paths s p q"
   1.807 @@ -460,7 +614,7 @@
   1.808  qed
   1.809  
   1.810  lemma homotopic_paths_subset: "\<lbrakk>homotopic_paths s p q; s \<subseteq> t\<rbrakk> \<Longrightarrow> homotopic_paths t p q"
   1.811 -  using homotopic_paths_def homotopic_with_subset_right by blast
   1.812 +  unfolding homotopic_paths by fast
   1.813  
   1.814  
   1.815  text\<open> A slightly ad-hoc but useful lemma in constructing homotopies.\<close>
   1.816 @@ -514,9 +668,7 @@
   1.817  proposition homotopic_paths_continuous_image:
   1.818      "\<lbrakk>homotopic_paths s f g; continuous_on s h; h ` s \<subseteq> t\<rbrakk> \<Longrightarrow> homotopic_paths t (h \<circ> f) (h \<circ> g)"
   1.819    unfolding homotopic_paths_def
   1.820 -  apply (rule homotopic_with_compose_continuous_left [of _ _ _ s])
   1.821 -  apply (auto simp: pathstart_def pathfinish_def elim!: homotopic_with_mono)
   1.822 -  done
   1.823 +  by (simp add: homotopic_with_compose_continuous_map_left pathfinish_compose pathstart_compose)
   1.824  
   1.825  
   1.826  subsection\<open>Group properties for homotopy of paths\<close>
   1.827 @@ -586,7 +738,7 @@
   1.828  
   1.829  definition%important homotopic_loops :: "'a::topological_space set \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> bool"  where
   1.830   "homotopic_loops s p q \<equiv>
   1.831 -     homotopic_with (\<lambda>r. pathfinish r = pathstart r) {0..1} s p q"
   1.832 +     homotopic_with_canon (\<lambda>r. pathfinish r = pathstart r) {0..1} s p q"
   1.833  
   1.834  lemma homotopic_loops:
   1.835     "homotopic_loops s p q \<longleftrightarrow>
   1.836 @@ -604,17 +756,17 @@
   1.837  proposition homotopic_loops_imp_path:
   1.838       "homotopic_loops s p q \<Longrightarrow> path p \<and> path q"
   1.839    unfolding homotopic_loops_def path_def
   1.840 -  using homotopic_with_imp_continuous by blast
   1.841 +  using homotopic_with_imp_continuous_maps continuous_map_subtopology_eu by blast
   1.842  
   1.843  proposition homotopic_loops_imp_subset:
   1.844       "homotopic_loops s p q \<Longrightarrow> path_image p \<subseteq> s \<and> path_image q \<subseteq> s"
   1.845    unfolding homotopic_loops_def path_image_def
   1.846 -  by (metis homotopic_with_imp_subset1 homotopic_with_imp_subset2)
   1.847 +  by (meson continuous_map_subtopology_eu homotopic_with_imp_continuous_maps)
   1.848  
   1.849  proposition homotopic_loops_refl:
   1.850       "homotopic_loops s p p \<longleftrightarrow>
   1.851        path p \<and> path_image p \<subseteq> s \<and> pathfinish p = pathstart p"
   1.852 -  by (simp add: homotopic_loops_def homotopic_with_refl path_image_def path_def)
   1.853 +  by (simp add: homotopic_loops_def path_image_def path_def)
   1.854  
   1.855  proposition homotopic_loops_sym: "homotopic_loops s p q \<Longrightarrow> homotopic_loops s q p"
   1.856    by (simp add: homotopic_loops_def homotopic_with_sym)
   1.857 @@ -628,7 +780,7 @@
   1.858  
   1.859  proposition homotopic_loops_subset:
   1.860     "\<lbrakk>homotopic_loops s p q; s \<subseteq> t\<rbrakk> \<Longrightarrow> homotopic_loops t p q"
   1.861 -  by (simp add: homotopic_loops_def homotopic_with_subset_right)
   1.862 +  by (fastforce simp add: homotopic_loops)
   1.863  
   1.864  proposition homotopic_loops_eq:
   1.865     "\<lbrakk>path p; path_image p \<subseteq> s; pathfinish p = pathstart p; \<And>t. t \<in> {0..1} \<Longrightarrow> p(t) = q(t)\<rbrakk>
   1.866 @@ -642,16 +794,14 @@
   1.867  proposition homotopic_loops_continuous_image:
   1.868     "\<lbrakk>homotopic_loops s f g; continuous_on s h; h ` s \<subseteq> t\<rbrakk> \<Longrightarrow> homotopic_loops t (h \<circ> f) (h \<circ> g)"
   1.869    unfolding homotopic_loops_def
   1.870 -  apply (rule homotopic_with_compose_continuous_left)
   1.871 -  apply (erule homotopic_with_mono)
   1.872 -  by (simp add: pathfinish_def pathstart_def)
   1.873 +  by (simp add: homotopic_with_compose_continuous_map_left pathfinish_def pathstart_def)
   1.874  
   1.875  
   1.876  subsection\<open>Relations between the two variants of homotopy\<close>
   1.877  
   1.878  proposition homotopic_paths_imp_homotopic_loops:
   1.879      "\<lbrakk>homotopic_paths s p q; pathfinish p = pathstart p; pathfinish q = pathstart p\<rbrakk> \<Longrightarrow> homotopic_loops s p q"
   1.880 -  by (auto simp: homotopic_paths_def homotopic_loops_def intro: homotopic_with_mono)
   1.881 +  by (auto simp: homotopic_with_def homotopic_paths_def homotopic_loops_def)
   1.882  
   1.883  proposition homotopic_loops_imp_homotopic_paths_null:
   1.884    assumes "homotopic_loops s p (linepath a a)"
   1.885 @@ -828,7 +978,7 @@
   1.886    assumes contf: "continuous_on s f"
   1.887        and contg:"continuous_on s g"
   1.888        and sub: "\<And>x. x \<in> s \<Longrightarrow> closed_segment (f x) (g x) \<subseteq> t"
   1.889 -    shows "homotopic_with (\<lambda>z. True) s t f g"
   1.890 +    shows "homotopic_with_canon (\<lambda>z. True) s t f g"
   1.891    apply (simp add: homotopic_with_def)
   1.892    apply (rule_tac x="\<lambda>y. ((1 - (fst y)) *\<^sub>R f(snd y) + (fst y) *\<^sub>R g(snd y))" in exI)
   1.893    apply (intro conjI)
   1.894 @@ -1208,7 +1358,7 @@
   1.895  subsection\<open>Contractible sets\<close>
   1.896  
   1.897  definition%important contractible where
   1.898 - "contractible S \<equiv> \<exists>a. homotopic_with (\<lambda>x. True) S S id (\<lambda>x. a)"
   1.899 + "contractible S \<equiv> \<exists>a. homotopic_with_canon (\<lambda>x. True) S S id (\<lambda>x. a)"
   1.900  
   1.901  proposition contractible_imp_simply_connected:
   1.902    fixes S :: "_::real_normed_vector set"
   1.903 @@ -1217,10 +1367,10 @@
   1.904    case True then show ?thesis by force
   1.905  next
   1.906    case False
   1.907 -  obtain a where a: "homotopic_with (\<lambda>x. True) S S id (\<lambda>x. a)"
   1.908 +  obtain a where a: "homotopic_with_canon (\<lambda>x. True) S S id (\<lambda>x. a)"
   1.909      using assms by (force simp: contractible_def)
   1.910    then have "a \<in> S"
   1.911 -    by (metis False homotopic_constant_maps homotopic_with_symD homotopic_with_trans path_component_mem(2))
   1.912 +    by (metis False homotopic_constant_maps homotopic_with_symD homotopic_with_trans path_component_in_topspace topspace_euclidean_subtopology)
   1.913    show ?thesis
   1.914      apply (simp add: simply_connected_eq_contractible_loop_all False)
   1.915      apply (rule bexI [OF _ \<open>a \<in> S\<close>])
   1.916 @@ -1246,14 +1396,14 @@
   1.917    assumes f: "continuous_on S f" "f ` S \<subseteq> T"
   1.918        and g: "continuous_on T g" "g ` T \<subseteq> U"
   1.919        and T: "contractible T"
   1.920 -    obtains c where "homotopic_with (\<lambda>h. True) S U (g \<circ> f) (\<lambda>x. c)"
   1.921 +    obtains c where "homotopic_with_canon (\<lambda>h. True) S U (g \<circ> f) (\<lambda>x. c)"
   1.922  proof -
   1.923 -  obtain b where b: "homotopic_with (\<lambda>x. True) T T id (\<lambda>x. b)"
   1.924 +  obtain b where b: "homotopic_with_canon (\<lambda>x. True) T T id (\<lambda>x. b)"
   1.925      using assms by (force simp: contractible_def)
   1.926 -  have "homotopic_with (\<lambda>f. True) T U (g \<circ> id) (g \<circ> (\<lambda>x. b))"
   1.927 -    by (rule homotopic_compose_continuous_left [OF b g])
   1.928 -  then have "homotopic_with (\<lambda>f. True) S U (g \<circ> id \<circ> f) (g \<circ> (\<lambda>x. b) \<circ> f)"
   1.929 -    by (rule homotopic_compose_continuous_right [OF _ f])
   1.930 +  have "homotopic_with_canon (\<lambda>f. True) T U (g \<circ> id) (g \<circ> (\<lambda>x. b))"
   1.931 +    by (metis Abstract_Topology.continuous_map_subtopology_eu b g homotopic_compose_continuous_map_left)
   1.932 +  then have "homotopic_with_canon (\<lambda>f. True) S U (g \<circ> id \<circ> f) (g \<circ> (\<lambda>x. b) \<circ> f)"
   1.933 +    by (simp add: f homotopic_with_compose_continuous_map_right)
   1.934    then show ?thesis
   1.935      by (simp add: comp_def that)
   1.936  qed
   1.937 @@ -1261,7 +1411,7 @@
   1.938  lemma nullhomotopic_into_contractible:
   1.939    assumes f: "continuous_on S f" "f ` S \<subseteq> T"
   1.940        and T: "contractible T"
   1.941 -    obtains c where "homotopic_with (\<lambda>h. True) S T f (\<lambda>x. c)"
   1.942 +    obtains c where "homotopic_with_canon (\<lambda>h. True) S T f (\<lambda>x. c)"
   1.943  apply (rule nullhomotopic_through_contractible [OF f, of id T])
   1.944  using assms
   1.945  apply (auto simp: continuous_on_id)
   1.946 @@ -1270,7 +1420,7 @@
   1.947  lemma nullhomotopic_from_contractible:
   1.948    assumes f: "continuous_on S f" "f ` S \<subseteq> T"
   1.949        and S: "contractible S"
   1.950 -    obtains c where "homotopic_with (\<lambda>h. True) S T f (\<lambda>x. c)"
   1.951 +    obtains c where "homotopic_with_canon (\<lambda>h. True) S T f (\<lambda>x. c)"
   1.952  apply (rule nullhomotopic_through_contractible [OF continuous_on_id _ f S, of S])
   1.953  using assms
   1.954  apply (auto simp: comp_def)
   1.955 @@ -1283,13 +1433,13 @@
   1.956            "continuous_on S f2" "f2 ` S \<subseteq> T"
   1.957            "continuous_on T g2" "g2 ` T \<subseteq> U"
   1.958            "contractible T" "path_connected U"
   1.959 -   shows "homotopic_with (\<lambda>h. True) S U (g1 \<circ> f1) (g2 \<circ> f2)"
   1.960 +   shows "homotopic_with_canon (\<lambda>h. True) S U (g1 \<circ> f1) (g2 \<circ> f2)"
   1.961  proof -
   1.962 -  obtain c1 where c1: "homotopic_with (\<lambda>h. True) S U (g1 \<circ> f1) (\<lambda>x. c1)"
   1.963 +  obtain c1 where c1: "homotopic_with_canon (\<lambda>h. True) S U (g1 \<circ> f1) (\<lambda>x. c1)"
   1.964      apply (rule nullhomotopic_through_contractible [of S f1 T g1 U])
   1.965      using assms apply auto
   1.966      done
   1.967 -  obtain c2 where c2: "homotopic_with (\<lambda>h. True) S U (g2 \<circ> f2) (\<lambda>x. c2)"
   1.968 +  obtain c2 where c2: "homotopic_with_canon (\<lambda>h. True) S U (g2 \<circ> f2) (\<lambda>x. c2)"
   1.969      apply (rule nullhomotopic_through_contractible [of S f2 T g2 U])
   1.970      using assms apply auto
   1.971      done
   1.972 @@ -1299,7 +1449,7 @@
   1.973    next
   1.974      case False
   1.975      with c1 c2 have "c1 \<in> U" "c2 \<in> U"
   1.976 -      using homotopic_with_imp_subset2 all_not_in_conv image_subset_iff by blast+
   1.977 +      using homotopic_with_imp_continuous_maps by fastforce+
   1.978      with \<open>path_connected U\<close> show ?thesis by blast
   1.979    qed
   1.980    show ?thesis
   1.981 @@ -1315,24 +1465,24 @@
   1.982    assumes f: "continuous_on S f" "f ` S \<subseteq> T"
   1.983        and g: "continuous_on S g" "g ` S \<subseteq> T"
   1.984        and T: "contractible T"
   1.985 -    shows "homotopic_with (\<lambda>h. True) S T f g"
   1.986 +    shows "homotopic_with_canon (\<lambda>h. True) S T f g"
   1.987  using homotopic_through_contractible [of S f T id T g id]
   1.988 -by (simp add: assms contractible_imp_path_connected continuous_on_id)
   1.989 +by (simp add: assms contractible_imp_path_connected)
   1.990  
   1.991  lemma homotopic_from_contractible:
   1.992    fixes S :: "'a::real_normed_vector set" and T:: "'b::real_normed_vector set"
   1.993    assumes f: "continuous_on S f" "f ` S \<subseteq> T"
   1.994        and g: "continuous_on S g" "g ` S \<subseteq> T"
   1.995        and "contractible S" "path_connected T"
   1.996 -    shows "homotopic_with (\<lambda>h. True) S T f g"
   1.997 +    shows "homotopic_with_canon (\<lambda>h. True) S T f g"
   1.998  using homotopic_through_contractible [of S id S f T id g]
   1.999 -by (simp add: assms contractible_imp_path_connected continuous_on_id)
  1.1000 +by (simp add: assms contractible_imp_path_connected)
  1.1001  
  1.1002  lemma starlike_imp_contractible_gen:
  1.1003    fixes S :: "'a::real_normed_vector set"
  1.1004    assumes S: "starlike S"
  1.1005        and P: "\<And>a T. \<lbrakk>a \<in> S; 0 \<le> T; T \<le> 1\<rbrakk> \<Longrightarrow> P(\<lambda>x. (1 - T) *\<^sub>R x + T *\<^sub>R a)"
  1.1006 -    obtains a where "homotopic_with P S S (\<lambda>x. x) (\<lambda>x. a)"
  1.1007 +    obtains a where "homotopic_with_canon P S S (\<lambda>x. x) (\<lambda>x. a)"
  1.1008  proof -
  1.1009    obtain a where "a \<in> S" and a: "\<And>x. x \<in> S \<Longrightarrow> closed_segment a x \<subseteq> S"
  1.1010      using S by (auto simp: starlike_def)
  1.1011 @@ -1385,7 +1535,7 @@
  1.1012  using convex_imp_simply_connected is_interval_convex_1 is_interval_path_connected_1 simply_connected_imp_path_connected by auto
  1.1013  
  1.1014  lemma contractible_empty [simp]: "contractible {}"
  1.1015 -  by (simp add: contractible_def homotopic_with)
  1.1016 +  by (simp add: contractible_def homotopic_on_emptyI)
  1.1017  
  1.1018  lemma contractible_convex_tweak_boundary_points:
  1.1019    fixes S :: "'a::euclidean_space set"
  1.1020 @@ -1445,27 +1595,6 @@
  1.1021      done
  1.1022  qed
  1.1023  
  1.1024 -lemma homotopy_dominated_contractibility:
  1.1025 -  fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set"
  1.1026 -  assumes S: "contractible S"
  1.1027 -      and f: "continuous_on S f" "image f S \<subseteq> T"
  1.1028 -      and g: "continuous_on T g" "image g T \<subseteq> S"
  1.1029 -      and hom: "homotopic_with (\<lambda>x. True) T T (f \<circ> g) id"
  1.1030 -    shows "contractible T"
  1.1031 -proof -
  1.1032 -  obtain b where "homotopic_with (\<lambda>h. True) S T f (\<lambda>x. b)"
  1.1033 -    using nullhomotopic_from_contractible [OF f S] .
  1.1034 -  then have homg: "homotopic_with (\<lambda>x. True) T T ((\<lambda>x. b) \<circ> g) (f \<circ> g)"
  1.1035 -    by (rule homotopic_with_compose_continuous_right [OF homotopic_with_symD g])
  1.1036 -  show ?thesis
  1.1037 -    apply (simp add: contractible_def)
  1.1038 -    apply (rule exI [where x = b])
  1.1039 -    apply (rule homotopic_with_symD)
  1.1040 -    apply (rule homotopic_with_trans [OF _ hom])
  1.1041 -    using homg apply (simp add: o_def)
  1.1042 -    done
  1.1043 -qed
  1.1044 -
  1.1045  
  1.1046  subsection\<open>Local versions of topological properties in general\<close>
  1.1047  
  1.1048 @@ -1541,7 +1670,7 @@
  1.1049  apply (simp add: open_Int)
  1.1050  apply (rule_tac x="V1 \<inter> V2" in exI)
  1.1051  apply (auto intro: P)
  1.1052 -done
  1.1053 +  done
  1.1054  
  1.1055  lemma locally_Times:
  1.1056    fixes S :: "('a::metric_space) set" and T :: "('b::metric_space) set"
  1.1057 @@ -1561,7 +1690,7 @@
  1.1058    with \<open>U \<times> V \<subseteq> W\<close> show "\<exists>u v. openin (top_of_set (S \<times> T)) u \<and> R v \<and> (x,y) \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> W"
  1.1059      apply (rule_tac x="U1 \<times> V1" in exI)
  1.1060      apply (rule_tac x="U2 \<times> V2" in exI)
  1.1061 -    apply (auto simp: openin_Times R)
  1.1062 +    apply (auto simp: openin_Times R openin_Times_eq)
  1.1063      done
  1.1064  qed
  1.1065  
  1.1066 @@ -3195,10 +3324,10 @@
  1.1067        and Qeq: "\<And>h k. (\<And>x. x \<in> u \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
  1.1068        and hom: "\<And>f g. \<lbrakk>continuous_on u f; f ` u \<subseteq> s; P f;
  1.1069                         continuous_on u g; g ` u \<subseteq> s; P g\<rbrakk>
  1.1070 -                       \<Longrightarrow> homotopic_with P u s f g"
  1.1071 +                       \<Longrightarrow> homotopic_with_canon P u s f g"
  1.1072        and contf: "continuous_on u f" and imf: "f ` u \<subseteq> t" and Qf: "Q f"
  1.1073        and contg: "continuous_on u g" and img: "g ` u \<subseteq> t" and Qg: "Q g"
  1.1074 -    shows "homotopic_with Q u t f g"
  1.1075 +    shows "homotopic_with_canon Q u t f g"
  1.1076  proof -
  1.1077    have feq: "\<And>x. x \<in> u \<Longrightarrow> (h \<circ> (k \<circ> f)) x = f x" using idhk imf by auto
  1.1078    have geq: "\<And>x. x \<in> u \<Longrightarrow> (h \<circ> (k \<circ> g)) x = g x" using idhk img by auto
  1.1079 @@ -3214,17 +3343,15 @@
  1.1080      using img imk by fastforce
  1.1081    moreover have "P (k \<circ> g)"
  1.1082      by (simp add: P Qg contg img)
  1.1083 -  ultimately have "homotopic_with P u s (k \<circ> f) (k \<circ> g)"
  1.1084 +  ultimately have "homotopic_with_canon P u s (k \<circ> f) (k \<circ> g)"
  1.1085      by (rule hom)
  1.1086 -  then have "homotopic_with Q u t (h \<circ> (k \<circ> f)) (h \<circ> (k \<circ> g))"
  1.1087 +  then have "homotopic_with_canon Q u t (h \<circ> (k \<circ> f)) (h \<circ> (k \<circ> g))"
  1.1088      apply (rule homotopic_with_compose_continuous_left [OF homotopic_with_mono])
  1.1089      using Q by (auto simp: conth imh)
  1.1090    then show ?thesis
  1.1091      apply (rule homotopic_with_eq)
  1.1092 -    apply (metis feq)
  1.1093 -    apply (metis geq)
  1.1094 -    apply (metis Qeq)
  1.1095 -    done
  1.1096 +    using feq geq apply fastforce+
  1.1097 +    using Qeq topspace_euclidean_subtopology by blast
  1.1098  qed
  1.1099  
  1.1100  lemma homotopically_trivial_retraction_null_gen:
  1.1101 @@ -3232,9 +3359,9 @@
  1.1102        and Q: "\<And>f. \<lbrakk>continuous_on u f; f ` u \<subseteq> s; P f\<rbrakk> \<Longrightarrow> Q(h \<circ> f)"
  1.1103        and Qeq: "\<And>h k. (\<And>x. x \<in> u \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
  1.1104        and hom: "\<And>f. \<lbrakk>continuous_on u f; f ` u \<subseteq> s; P f\<rbrakk>
  1.1105 -                     \<Longrightarrow> \<exists>c. homotopic_with P u s f (\<lambda>x. c)"
  1.1106 +                     \<Longrightarrow> \<exists>c. homotopic_with_canon P u s f (\<lambda>x. c)"
  1.1107        and contf: "continuous_on u f" and imf:"f ` u \<subseteq> t" and Qf: "Q f"
  1.1108 -  obtains c where "homotopic_with Q u t f (\<lambda>x. c)"
  1.1109 +  obtains c where "homotopic_with_canon Q u t f (\<lambda>x. c)"
  1.1110  proof -
  1.1111    have feq: "\<And>x. x \<in> u \<Longrightarrow> (h \<circ> (k \<circ> f)) x = f x" using idhk imf by auto
  1.1112    have "continuous_on u (k \<circ> f)"
  1.1113 @@ -3243,17 +3370,17 @@
  1.1114      using imf imk by fastforce
  1.1115    moreover have "P (k \<circ> f)"
  1.1116      by (simp add: P Qf contf imf)
  1.1117 -  ultimately obtain c where "homotopic_with P u s (k \<circ> f) (\<lambda>x. c)"
  1.1118 +  ultimately obtain c where "homotopic_with_canon P u s (k \<circ> f) (\<lambda>x. c)"
  1.1119      by (metis hom)
  1.1120 -  then have "homotopic_with Q u t (h \<circ> (k \<circ> f)) (h \<circ> (\<lambda>x. c))"
  1.1121 +  then have "homotopic_with_canon Q u t (h \<circ> (k \<circ> f)) (h \<circ> (\<lambda>x. c))"
  1.1122      apply (rule homotopic_with_compose_continuous_left [OF homotopic_with_mono])
  1.1123      using Q by (auto simp: conth imh)
  1.1124    then show ?thesis
  1.1125      apply (rule_tac c = "h c" in that)
  1.1126      apply (erule homotopic_with_eq)
  1.1127 -    apply (metis feq, simp)
  1.1128 -    apply (metis Qeq)
  1.1129 -    done
  1.1130 +    using feq apply auto[1]
  1.1131 +    apply simp
  1.1132 +    using Qeq topspace_euclidean_subtopology by blast
  1.1133  qed
  1.1134  
  1.1135  lemma cohomotopically_trivial_retraction_gen:
  1.1136 @@ -3262,10 +3389,10 @@
  1.1137        and Qeq: "\<And>h k. (\<And>x. x \<in> t \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
  1.1138        and hom: "\<And>f g. \<lbrakk>continuous_on s f; f ` s \<subseteq> u; P f;
  1.1139                         continuous_on s g; g ` s \<subseteq> u; P g\<rbrakk>
  1.1140 -                       \<Longrightarrow> homotopic_with P s u f g"
  1.1141 +                       \<Longrightarrow> homotopic_with_canon P s u f g"
  1.1142        and contf: "continuous_on t f" and imf: "f ` t \<subseteq> u" and Qf: "Q f"
  1.1143        and contg: "continuous_on t g" and img: "g ` t \<subseteq> u" and Qg: "Q g"
  1.1144 -    shows "homotopic_with Q t u f g"
  1.1145 +    shows "homotopic_with_canon Q t u f g"
  1.1146  proof -
  1.1147    have feq: "\<And>x. x \<in> t \<Longrightarrow> (f \<circ> h \<circ> k) x = f x" using idhk imf by auto
  1.1148    have geq: "\<And>x. x \<in> t \<Longrightarrow> (g \<circ> h \<circ> k) x = g x" using idhk img by auto
  1.1149 @@ -3281,17 +3408,16 @@
  1.1150      using img imh by fastforce
  1.1151    moreover have "P (g \<circ> h)"
  1.1152      by (simp add: P Qg contg img)
  1.1153 -  ultimately have "homotopic_with P s u (f \<circ> h) (g \<circ> h)"
  1.1154 +  ultimately have "homotopic_with_canon P s u (f \<circ> h) (g \<circ> h)"
  1.1155      by (rule hom)
  1.1156 -  then have "homotopic_with Q t u (f \<circ> h \<circ> k) (g \<circ> h \<circ> k)"
  1.1157 +  then have "homotopic_with_canon Q t u (f \<circ> h \<circ> k) (g \<circ> h \<circ> k)"
  1.1158      apply (rule homotopic_with_compose_continuous_right [OF homotopic_with_mono])
  1.1159      using Q by (auto simp: contk imk)
  1.1160    then show ?thesis
  1.1161      apply (rule homotopic_with_eq)
  1.1162 -    apply (metis feq)
  1.1163 -    apply (metis geq)
  1.1164 -    apply (metis Qeq)
  1.1165 -    done
  1.1166 +    using feq apply auto[1]
  1.1167 +    using geq apply auto[1]
  1.1168 +    using Qeq topspace_euclidean_subtopology by blast
  1.1169  qed
  1.1170  
  1.1171  lemma cohomotopically_trivial_retraction_null_gen:
  1.1172 @@ -3299,9 +3425,9 @@
  1.1173        and Q: "\<And>f. \<lbrakk>continuous_on s f; f ` s \<subseteq> u; P f\<rbrakk> \<Longrightarrow> Q(f \<circ> k)"
  1.1174        and Qeq: "\<And>h k. (\<And>x. x \<in> t \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
  1.1175        and hom: "\<And>f g. \<lbrakk>continuous_on s f; f ` s \<subseteq> u; P f\<rbrakk>
  1.1176 -                       \<Longrightarrow> \<exists>c. homotopic_with P s u f (\<lambda>x. c)"
  1.1177 +                       \<Longrightarrow> \<exists>c. homotopic_with_canon P s u f (\<lambda>x. c)"
  1.1178        and contf: "continuous_on t f" and imf: "f ` t \<subseteq> u" and Qf: "Q f"
  1.1179 -  obtains c where "homotopic_with Q t u f (\<lambda>x. c)"
  1.1180 +  obtains c where "homotopic_with_canon Q t u f (\<lambda>x. c)"
  1.1181  proof -
  1.1182    have feq: "\<And>x. x \<in> t \<Longrightarrow> (f \<circ> h \<circ> k) x = f x" using idhk imf by auto
  1.1183    have "continuous_on s (f \<circ> h)"
  1.1184 @@ -3310,17 +3436,17 @@
  1.1185      using imf imh by fastforce
  1.1186    moreover have "P (f \<circ> h)"
  1.1187      by (simp add: P Qf contf imf)
  1.1188 -  ultimately obtain c where "homotopic_with P s u (f \<circ> h) (\<lambda>x. c)"
  1.1189 +  ultimately obtain c where "homotopic_with_canon P s u (f \<circ> h) (\<lambda>x. c)"
  1.1190      by (metis hom)
  1.1191 -  then have "homotopic_with Q t u (f \<circ> h \<circ> k) ((\<lambda>x. c) \<circ> k)"
  1.1192 +  then have "homotopic_with_canon Q t u (f \<circ> h \<circ> k) ((\<lambda>x. c) \<circ> k)"
  1.1193      apply (rule homotopic_with_compose_continuous_right [OF homotopic_with_mono])
  1.1194      using Q by (auto simp: contk imk)
  1.1195    then show ?thesis
  1.1196      apply (rule_tac c = c in that)
  1.1197      apply (erule homotopic_with_eq)
  1.1198 -    apply (metis feq, simp)
  1.1199 -    apply (metis Qeq)
  1.1200 -    done
  1.1201 +    using feq apply auto[1]
  1.1202 +    apply simp
  1.1203 +    using Qeq topspace_euclidean_subtopology by blast
  1.1204  qed
  1.1205  
  1.1206  end
  1.1207 @@ -3346,59 +3472,64 @@
  1.1208  
  1.1209  subsection\<open>Homotopy equivalence\<close>
  1.1210  
  1.1211 -definition%important homotopy_eqv :: "'a::topological_space set \<Rightarrow> 'b::topological_space set \<Rightarrow> bool"
  1.1212 -             (infix "homotopy'_eqv" 50)
  1.1213 -  where "S homotopy_eqv T \<equiv>
  1.1214 -        \<exists>f g. continuous_on S f \<and> f ` S \<subseteq> T \<and>
  1.1215 -              continuous_on T g \<and> g ` T \<subseteq> S \<and>
  1.1216 -              homotopic_with (\<lambda>x. True) S S (g \<circ> f) id \<and>
  1.1217 -              homotopic_with (\<lambda>x. True) T T (f \<circ> g) id"
  1.1218 -
  1.1219 -lemma homeomorphic_imp_homotopy_eqv: "S homeomorphic T \<Longrightarrow> S homotopy_eqv T"
  1.1220 -  unfolding homeomorphic_def homotopy_eqv_def homeomorphism_def
  1.1221 -  by (fastforce intro!: homotopic_with_equal continuous_on_compose)
  1.1222 -
  1.1223 -lemma homotopy_eqv_refl: "S homotopy_eqv S"
  1.1224 -  by (rule homeomorphic_imp_homotopy_eqv homeomorphic_refl)+
  1.1225 -
  1.1226 -lemma homotopy_eqv_sym: "S homotopy_eqv T \<longleftrightarrow> T homotopy_eqv S"
  1.1227 -  by (auto simp: homotopy_eqv_def)
  1.1228 +subsection\<open>Homotopy equivalence of topological spaces.\<close>
  1.1229 +
  1.1230 +definition%important homotopy_equivalent_space
  1.1231 +             (infix "homotopy'_equivalent'_space" 50)
  1.1232 +  where "X homotopy_equivalent_space Y \<equiv>
  1.1233 +        (\<exists>f g. continuous_map X Y f \<and>
  1.1234 +              continuous_map Y X g \<and>
  1.1235 +              homotopic_with (\<lambda>x. True) X X (g \<circ> f) id \<and>
  1.1236 +              homotopic_with (\<lambda>x. True) Y Y (f \<circ> g) id)"
  1.1237 +
  1.1238 +lemma homeomorphic_imp_homotopy_equivalent_space:
  1.1239 +  "X homeomorphic_space Y \<Longrightarrow> X homotopy_equivalent_space Y"
  1.1240 +  unfolding homeomorphic_space_def homotopy_equivalent_space_def
  1.1241 +  apply (erule ex_forward)+
  1.1242 +  by (simp add: homotopic_with_equal homotopic_with_sym homeomorphic_maps_def)
  1.1243 +
  1.1244 +lemma homotopy_equivalent_space_refl:
  1.1245 +   "X homotopy_equivalent_space X"
  1.1246 +  by (simp add: homeomorphic_imp_homotopy_equivalent_space homeomorphic_space_refl)
  1.1247 +
  1.1248 +lemma homotopy_equivalent_space_sym:
  1.1249 +   "X homotopy_equivalent_space Y \<longleftrightarrow> Y homotopy_equivalent_space X"
  1.1250 +  by (meson homotopy_equivalent_space_def)
  1.1251  
  1.1252  lemma homotopy_eqv_trans [trans]:
  1.1253 -    fixes S :: "'a::real_normed_vector set" and U :: "'c::real_normed_vector set"
  1.1254 -  assumes ST: "S homotopy_eqv T" and TU: "T homotopy_eqv U"
  1.1255 -    shows "S homotopy_eqv U"
  1.1256 +  assumes 1: "X homotopy_equivalent_space Y" and 2: "Y homotopy_equivalent_space U"
  1.1257 +    shows "X homotopy_equivalent_space U"
  1.1258  proof -
  1.1259 -  obtain f1 g1 where f1: "continuous_on S f1" "f1 ` S \<subseteq> T"
  1.1260 -                 and g1: "continuous_on T g1" "g1 ` T \<subseteq> S"
  1.1261 -                 and hom1: "homotopic_with (\<lambda>x. True) S S (g1 \<circ> f1) id"
  1.1262 -                           "homotopic_with (\<lambda>x. True) T T (f1 \<circ> g1) id"
  1.1263 -    using ST by (auto simp: homotopy_eqv_def)
  1.1264 -  obtain f2 g2 where f2: "continuous_on T f2" "f2 ` T \<subseteq> U"
  1.1265 -                 and g2: "continuous_on U g2" "g2 ` U \<subseteq> T"
  1.1266 -                 and hom2: "homotopic_with (\<lambda>x. True) T T (g2 \<circ> f2) id"
  1.1267 +  obtain f1 g1 where f1: "continuous_map X Y f1"
  1.1268 +                 and g1: "continuous_map Y X g1"
  1.1269 +                 and hom1: "homotopic_with (\<lambda>x. True) X X (g1 \<circ> f1) id"
  1.1270 +                           "homotopic_with (\<lambda>x. True) Y Y (f1 \<circ> g1) id"
  1.1271 +    using 1 by (auto simp: homotopy_equivalent_space_def)
  1.1272 +  obtain f2 g2 where f2: "continuous_map Y U f2"
  1.1273 +                 and g2: "continuous_map U Y g2"
  1.1274 +                 and hom2: "homotopic_with (\<lambda>x. True) Y Y (g2 \<circ> f2) id"
  1.1275                             "homotopic_with (\<lambda>x. True) U U (f2 \<circ> g2) id"
  1.1276 -    using TU by (auto simp: homotopy_eqv_def)
  1.1277 -  have "homotopic_with (\<lambda>f. True) S T (g2 \<circ> f2 \<circ> f1) (id \<circ> f1)"
  1.1278 -    by (rule homotopic_with_compose_continuous_right hom2 f1)+
  1.1279 -  then have "homotopic_with (\<lambda>f. True) S T (g2 \<circ> (f2 \<circ> f1)) (id \<circ> f1)"
  1.1280 +    using 2 by (auto simp: homotopy_equivalent_space_def)
  1.1281 +  have "homotopic_with (\<lambda>f. True) X Y (g2 \<circ> f2 \<circ> f1) (id \<circ> f1)"
  1.1282 +    using f1 hom2(1) homotopic_compose_continuous_map_right by blast
  1.1283 +  then have "homotopic_with (\<lambda>f. True) X Y (g2 \<circ> (f2 \<circ> f1)) (id \<circ> f1)"
  1.1284      by (simp add: o_assoc)
  1.1285 -  then have "homotopic_with (\<lambda>x. True) S S
  1.1286 +  then have "homotopic_with (\<lambda>x. True) X X
  1.1287           (g1 \<circ> (g2 \<circ> (f2 \<circ> f1))) (g1 \<circ> (id \<circ> f1))"
  1.1288 -    by (simp add: g1 homotopic_with_compose_continuous_left)
  1.1289 -  moreover have "homotopic_with (\<lambda>x. True) S S (g1 \<circ> id \<circ> f1) id"
  1.1290 +    by (simp add: g1 homotopic_compose_continuous_map_left)
  1.1291 +  moreover have "homotopic_with (\<lambda>x. True) X X (g1 \<circ> id \<circ> f1) id"
  1.1292      using hom1 by simp
  1.1293 -  ultimately have SS: "homotopic_with (\<lambda>x. True) S S (g1 \<circ> g2 \<circ> (f2 \<circ> f1)) id"
  1.1294 +  ultimately have SS: "homotopic_with (\<lambda>x. True) X X (g1 \<circ> g2 \<circ> (f2 \<circ> f1)) id"
  1.1295      apply (simp add: o_assoc)
  1.1296      apply (blast intro: homotopic_with_trans)
  1.1297      done
  1.1298 -  have "homotopic_with (\<lambda>f. True) U T (f1 \<circ> g1 \<circ> g2) (id \<circ> g2)"
  1.1299 -    by (rule homotopic_with_compose_continuous_right hom1 g2)+
  1.1300 -  then have "homotopic_with (\<lambda>f. True) U T (f1 \<circ> (g1 \<circ> g2)) (id \<circ> g2)"
  1.1301 +  have "homotopic_with (\<lambda>f. True) U Y (f1 \<circ> g1 \<circ> g2) (id \<circ> g2)"
  1.1302 +    using g2 hom1(2) homotopic_with_compose_continuous_map_right by fastforce
  1.1303 +  then have "homotopic_with (\<lambda>f. True) U Y (f1 \<circ> (g1 \<circ> g2)) (id \<circ> g2)"
  1.1304      by (simp add: o_assoc)
  1.1305    then have "homotopic_with (\<lambda>x. True) U U
  1.1306           (f2 \<circ> (f1 \<circ> (g1 \<circ> g2))) (f2 \<circ> (id \<circ> g2))"
  1.1307 -    by (simp add: f2 homotopic_with_compose_continuous_left)
  1.1308 +    by (simp add: f2 homotopic_with_compose_continuous_map_left)
  1.1309    moreover have "homotopic_with (\<lambda>x. True) U U (f2 \<circ> id \<circ> g2) id"
  1.1310      using hom2 by simp
  1.1311    ultimately have UU: "homotopic_with (\<lambda>x. True) U U (f2 \<circ> f1 \<circ> (g1 \<circ> g2)) id"
  1.1312 @@ -3406,14 +3537,382 @@
  1.1313      apply (blast intro: homotopic_with_trans)
  1.1314      done
  1.1315    show ?thesis
  1.1316 -    unfolding homotopy_eqv_def
  1.1317 -    apply (rule_tac x = "f2 \<circ> f1" in exI)
  1.1318 -    apply (rule_tac x = "g1 \<circ> g2" in exI)
  1.1319 -    apply (intro conjI continuous_on_compose SS UU)
  1.1320 -    using f1 f2 g1 g2  apply (force simp: elim!: continuous_on_subset)+
  1.1321 -    done
  1.1322 +    unfolding homotopy_equivalent_space_def
  1.1323 +    by (blast intro: f1 f2 g1 g2 continuous_map_compose SS UU)
  1.1324 +qed
  1.1325 +
  1.1326 +lemma deformation_retraction_imp_homotopy_equivalent_space:
  1.1327 +  "\<lbrakk>homotopic_with (\<lambda>x. True) X X (s \<circ> r) id; retraction_maps X Y r s\<rbrakk>
  1.1328 +    \<Longrightarrow> X homotopy_equivalent_space Y"
  1.1329 +  unfolding homotopy_equivalent_space_def retraction_maps_def
  1.1330 +  apply (rule_tac x=r in exI)
  1.1331 +  apply (rule_tac x=s in exI)
  1.1332 +  apply (auto simp: homotopic_with_equal continuous_map_compose)
  1.1333 +  done
  1.1334 +
  1.1335 +lemma deformation_retract_imp_homotopy_equivalent_space:
  1.1336 +   "\<lbrakk>homotopic_with (\<lambda>x. True) X X r id; retraction_maps X Y r id\<rbrakk>
  1.1337 +    \<Longrightarrow> X homotopy_equivalent_space Y"
  1.1338 +  using deformation_retraction_imp_homotopy_equivalent_space by force
  1.1339 +
  1.1340 +lemma deformation_retract_of_space:
  1.1341 +  "S \<subseteq> topspace X \<and>
  1.1342 +   (\<exists>r. homotopic_with (\<lambda>x. True) X X id r \<and> retraction_maps X (subtopology X S) r id) \<longleftrightarrow>
  1.1343 +   S retract_of_space X \<and> (\<exists>f. homotopic_with (\<lambda>x. True) X X id f \<and> f ` (topspace X) \<subseteq> S)"
  1.1344 +proof (cases "S \<subseteq> topspace X")
  1.1345 +  case True
  1.1346 +  moreover have "(\<exists>r. homotopic_with (\<lambda>x. True) X X id r \<and> retraction_maps X (subtopology X S) r id)
  1.1347 +             \<longleftrightarrow> (S retract_of_space X \<and> (\<exists>f. homotopic_with (\<lambda>x. True) X X id f \<and> f ` topspace X \<subseteq> S))"
  1.1348 +    unfolding retract_of_space_def
  1.1349 +  proof safe
  1.1350 +    fix f r
  1.1351 +    assume f: "homotopic_with (\<lambda>x. True) X X id f"
  1.1352 +      and fS: "f ` topspace X \<subseteq> S"
  1.1353 +      and r: "continuous_map X (subtopology X S) r"
  1.1354 +      and req: "\<forall>x\<in>S. r x = x"
  1.1355 +    show "\<exists>r. homotopic_with (\<lambda>x. True) X X id r \<and> retraction_maps X (subtopology X S) r id"
  1.1356 +    proof (intro exI conjI)
  1.1357 +      have "homotopic_with (\<lambda>x. True) X X f r"
  1.1358 +        proof (rule homotopic_with_eq)
  1.1359 +          show "homotopic_with (\<lambda>x. True) X X (r \<circ> f) (r \<circ> id)"
  1.1360 +            using homotopic_with_symD continuous_map_into_fulltopology f homotopic_compose_continuous_map_left r by blast
  1.1361 +          show "f x = (r \<circ> f) x" if "x \<in> topspace X" for x
  1.1362 +            using that fS req by auto
  1.1363 +        qed auto
  1.1364 +      then show "homotopic_with (\<lambda>x. True) X X id r"
  1.1365 +        by (rule homotopic_with_trans [OF f])
  1.1366 +    next
  1.1367 +      show "retraction_maps X (subtopology X S) r id"
  1.1368 +        by (simp add: r req retraction_maps_def topspace_subtopology)
  1.1369 +    qed
  1.1370 +  qed (use True in \<open>auto simp: retraction_maps_def topspace_subtopology_subset continuous_map_in_subtopology\<close>)
  1.1371 +  ultimately show ?thesis by simp
  1.1372 +qed (auto simp: retract_of_space_def retraction_maps_def)
  1.1373 +
  1.1374 +
  1.1375 +
  1.1376 +subsection\<open>Contractible spaces\<close>
  1.1377 +
  1.1378 +text\<open>The definition (which agrees with "contractible" on subsets of Euclidean space)
  1.1379 +is a little cryptic because we don't in fact assume that the constant "a" is in the space.
  1.1380 +This forces the convention that the empty space / set is contractible, avoiding some special cases. \<close>
  1.1381 +
  1.1382 +definition contractible_space where
  1.1383 +  "contractible_space X \<equiv> \<exists>a. homotopic_with (\<lambda>x. True) X X id (\<lambda>x. a)"
  1.1384 +
  1.1385 +lemma contractible_space_top_of_set [simp]:"contractible_space (top_of_set S) \<longleftrightarrow> contractible S"
  1.1386 +  by (auto simp: contractible_space_def contractible_def)
  1.1387 +
  1.1388 +lemma contractible_space_empty:
  1.1389 +   "topspace X = {} \<Longrightarrow> contractible_space X"
  1.1390 +  apply (simp add: contractible_space_def homotopic_with_def)
  1.1391 +  apply (rule_tac x=undefined in exI)
  1.1392 +  apply (rule_tac x="\<lambda>(t,x). if t = 0 then x else undefined" in exI)
  1.1393 +  apply (auto simp: continuous_map_on_empty)
  1.1394 +  done
  1.1395 +
  1.1396 +lemma contractible_space_singleton:
  1.1397 +  "topspace X = {a} \<Longrightarrow> contractible_space X"
  1.1398 +  apply (simp add: contractible_space_def homotopic_with_def)
  1.1399 +  apply (rule_tac x=a in exI)
  1.1400 +  apply (rule_tac x="\<lambda>(t,x). if t = 0 then x else a" in exI)
  1.1401 +  apply (auto intro: continuous_map_eq [where f = "\<lambda>z. a"])
  1.1402 +  done
  1.1403 +
  1.1404 +lemma contractible_space_subset_singleton:
  1.1405 +   "topspace X \<subseteq> {a} \<Longrightarrow> contractible_space X"
  1.1406 +  by (meson contractible_space_empty contractible_space_singleton subset_singletonD)
  1.1407 +
  1.1408 +lemma contractible_space_subtopology_singleton:
  1.1409 +   "contractible_space(subtopology X {a})"
  1.1410 +  by (meson contractible_space_subset_singleton insert_subset path_connectedin_singleton path_connectedin_subtopology subsetI)
  1.1411 +
  1.1412 +lemma contractible_space:
  1.1413 +   "contractible_space X \<longleftrightarrow>
  1.1414 +        topspace X = {} \<or>
  1.1415 +        (\<exists>a \<in> topspace X. homotopic_with (\<lambda>x. True) X X id (\<lambda>x. a))"
  1.1416 +proof (cases "topspace X = {}")
  1.1417 +  case False
  1.1418 +  then show ?thesis
  1.1419 +    apply (auto simp: contractible_space_def)
  1.1420 +    using homotopic_with_imp_continuous_maps by fastforce
  1.1421 +qed (simp add: contractible_space_empty)
  1.1422 +
  1.1423 +lemma contractible_imp_path_connected_space:
  1.1424 +  assumes "contractible_space X" shows "path_connected_space X"
  1.1425 +proof (cases "topspace X = {}")
  1.1426 +  case False
  1.1427 +  have *: "path_connected_space X"
  1.1428 +    if "a \<in> topspace X" and conth: "continuous_map (prod_topology (top_of_set {0..1}) X) X h"
  1.1429 +      and h: "\<forall>x. h (0, x) = x" "\<forall>x. h (1, x) = a"
  1.1430 +    for a and h :: "real \<times> 'a \<Rightarrow> 'a"
  1.1431 +  proof -
  1.1432 +    have "path_component_of X b a" if "b \<in> topspace X" for b
  1.1433 +      using that unfolding path_component_of_def
  1.1434 +      apply (rule_tac x="h \<circ> (\<lambda>x. (x,b))" in exI)
  1.1435 +      apply (simp add: h pathin_def)
  1.1436 +      apply (rule continuous_map_compose [OF _ conth])
  1.1437 +      apply (auto simp: continuous_map_pairwise intro!: continuous_intros continuous_map_compose continuous_map_id [unfolded id_def])
  1.1438 +      done
  1.1439 +  then show ?thesis
  1.1440 +    by (metis path_component_of_equiv path_connected_space_iff_path_component)
  1.1441 +  qed
  1.1442 +  show ?thesis
  1.1443 +    using assms False by (auto simp: contractible_space homotopic_with_def *)
  1.1444 +qed (simp add: path_connected_space_topspace_empty)
  1.1445 +
  1.1446 +lemma contractible_imp_connected_space:
  1.1447 +   "contractible_space X \<Longrightarrow> connected_space X"
  1.1448 +  by (simp add: contractible_imp_path_connected_space path_connected_imp_connected_space)
  1.1449 +
  1.1450 +lemma contractible_space_alt:
  1.1451 +   "contractible_space X \<longleftrightarrow> (\<forall>a \<in> topspace X. homotopic_with (\<lambda>x. True) X X id (\<lambda>x. a))" (is "?lhs = ?rhs")
  1.1452 +proof
  1.1453 +  assume X: ?lhs
  1.1454 +  then obtain a where a: "homotopic_with (\<lambda>x. True) X X id (\<lambda>x. a)"
  1.1455 +    by (auto simp: contractible_space_def)
  1.1456 +  show ?rhs
  1.1457 +  proof
  1.1458 +    show "homotopic_with (\<lambda>x. True) X X id (\<lambda>x. b)" if "b \<in> topspace X" for b
  1.1459 +      apply (rule homotopic_with_trans [OF a])
  1.1460 +      using homotopic_constant_maps path_connected_space_imp_path_component_of
  1.1461 +      by (metis (full_types) X a continuous_map_const contractible_imp_path_connected_space homotopic_with_imp_continuous_maps that)
  1.1462 +  qed
  1.1463 +next
  1.1464 +  assume R: ?rhs
  1.1465 +  then show ?lhs
  1.1466 +    apply (simp add: contractible_space_def)
  1.1467 +    by (metis equals0I homotopic_on_emptyI)
  1.1468 +qed
  1.1469 +
  1.1470 +
  1.1471 +lemma compose_const [simp]: "f \<circ> (\<lambda>x. a) = (\<lambda>x. f a)" "(\<lambda>x. a) \<circ> g = (\<lambda>x. a)"
  1.1472 +  by (simp_all add: o_def)
  1.1473 +
  1.1474 +lemma nullhomotopic_through_contractible_space:
  1.1475 +  assumes f: "continuous_map X Y f" and g: "continuous_map Y Z g" and Y: "contractible_space Y"
  1.1476 +  obtains c where "homotopic_with (\<lambda>h. True) X Z (g \<circ> f) (\<lambda>x. c)"
  1.1477 +proof -
  1.1478 +  obtain b where b: "homotopic_with (\<lambda>x. True) Y Y id (\<lambda>x. b)"
  1.1479 +    using Y by (auto simp: contractible_space_def)
  1.1480 +  show thesis
  1.1481 +    using homotopic_compose_continuous_map_right
  1.1482 +           [OF homotopic_compose_continuous_map_left [OF b g] f]
  1.1483 +    by (simp add: that)
  1.1484  qed
  1.1485  
  1.1486 +lemma nullhomotopic_into_contractible_space:
  1.1487 +  assumes f: "continuous_map X Y f" and Y: "contractible_space Y"
  1.1488 +  obtains c where "homotopic_with (\<lambda>h. True) X Y f (\<lambda>x. c)"
  1.1489 +  using nullhomotopic_through_contractible_space [OF f _ Y]
  1.1490 +  by (metis continuous_map_id id_comp)
  1.1491 +
  1.1492 +lemma nullhomotopic_from_contractible_space:
  1.1493 +  assumes f: "continuous_map X Y f" and X: "contractible_space X"
  1.1494 +  obtains c where "homotopic_with (\<lambda>h. True) X Y f (\<lambda>x. c)"
  1.1495 +  using nullhomotopic_through_contractible_space [OF _ f X]
  1.1496 +  by (metis comp_id continuous_map_id)
  1.1497 +
  1.1498 +lemma homotopy_dominated_contractibility:
  1.1499 +  assumes f: "continuous_map X Y f" and g: "continuous_map Y X g"
  1.1500 +    and hom: "homotopic_with (\<lambda>x. True) Y Y (f \<circ> g) id" and X: "contractible_space X"
  1.1501 +  shows "contractible_space Y"
  1.1502 +proof -
  1.1503 +  obtain c where c: "homotopic_with (\<lambda>h. True) X Y f (\<lambda>x. c)"
  1.1504 +    using nullhomotopic_from_contractible_space [OF f X] .
  1.1505 +  have "homotopic_with (\<lambda>x. True) Y Y (f \<circ> g) (\<lambda>x. c)"
  1.1506 +    using homotopic_compose_continuous_map_right [OF c g] by fastforce
  1.1507 +  then have "homotopic_with (\<lambda>x. True) Y Y id (\<lambda>x. c)"
  1.1508 +    using homotopic_with_trans [OF _ hom] homotopic_with_symD by blast
  1.1509 +  then show ?thesis
  1.1510 +    unfolding contractible_space_def ..
  1.1511 +qed
  1.1512 +
  1.1513 +lemma homotopy_equivalent_space_contractibility:
  1.1514 +   "X homotopy_equivalent_space Y \<Longrightarrow> (contractible_space X \<longleftrightarrow> contractible_space Y)"
  1.1515 +  unfolding homotopy_equivalent_space_def
  1.1516 +  by (blast intro: homotopy_dominated_contractibility)
  1.1517 +
  1.1518 +lemma homeomorphic_space_contractibility:
  1.1519 +   "X homeomorphic_space Y
  1.1520 +        \<Longrightarrow> (contractible_space X \<longleftrightarrow> contractible_space Y)"
  1.1521 +  by (simp add: homeomorphic_imp_homotopy_equivalent_space homotopy_equivalent_space_contractibility)
  1.1522 +
  1.1523 +lemma contractible_eq_homotopy_equivalent_singleton_subtopology:
  1.1524 +   "contractible_space X \<longleftrightarrow>
  1.1525 +        topspace X = {} \<or> (\<exists>a \<in> topspace X. X homotopy_equivalent_space (subtopology X {a}))"(is "?lhs = ?rhs")
  1.1526 +proof (cases "topspace X = {}")
  1.1527 +  case False
  1.1528 +  show ?thesis
  1.1529 +  proof
  1.1530 +    assume ?lhs
  1.1531 +    then obtain a where a: "homotopic_with (\<lambda>x. True) X X id (\<lambda>x. a)"
  1.1532 +      by (auto simp: contractible_space_def)
  1.1533 +    then have "a \<in> topspace X"
  1.1534 +      by (metis False continuous_map_const homotopic_with_imp_continuous_maps)
  1.1535 +    then have "X homotopy_equivalent_space subtopology X {a}"
  1.1536 +      unfolding homotopy_equivalent_space_def
  1.1537 +      apply (rule_tac x="\<lambda>x. a" in exI)
  1.1538 +      apply (rule_tac x=id in exI)
  1.1539 +      apply (auto simp: homotopic_with_sym topspace_subtopology_subset a)
  1.1540 +      using connectedin_absolute connectedin_sing contractible_space_alt contractible_space_subtopology_singleton by fastforce
  1.1541 +    with \<open>a \<in> topspace X\<close> show ?rhs
  1.1542 +      by blast
  1.1543 +  next
  1.1544 +    assume ?rhs
  1.1545 +    then show ?lhs
  1.1546 +      by (meson False contractible_space_subtopology_singleton homotopy_equivalent_space_contractibility)
  1.1547 +  qed
  1.1548 +qed (simp add: contractible_space_empty)
  1.1549 +
  1.1550 +lemma contractible_space_retraction_map_image:
  1.1551 +  assumes "retraction_map X Y f" and X: "contractible_space X"
  1.1552 +  shows "contractible_space Y"
  1.1553 +proof -
  1.1554 +  obtain g where f: "continuous_map X Y f" and g: "continuous_map Y X g" and fg: "\<forall>y \<in> topspace Y. f(g y) = y"
  1.1555 +    using assms by (auto simp: retraction_map_def retraction_maps_def)
  1.1556 +  obtain a where a: "homotopic_with (\<lambda>x. True) X X id (\<lambda>x. a)"
  1.1557 +    using X by (auto simp: contractible_space_def)
  1.1558 +  have "homotopic_with (\<lambda>x. True) Y Y id (\<lambda>x. f a)"
  1.1559 +  proof (rule homotopic_with_eq)
  1.1560 +    show "homotopic_with (\<lambda>x. True) Y Y (f \<circ> id \<circ> g) (f \<circ> (\<lambda>x. a) \<circ> g)"
  1.1561 +      using f g a homotopic_compose_continuous_map_left homotopic_compose_continuous_map_right by metis
  1.1562 +  qed (use fg in auto)
  1.1563 +  then show ?thesis
  1.1564 +    unfolding contractible_space_def by blast
  1.1565 +qed
  1.1566 +
  1.1567 +lemma contractible_space_prod_topology:
  1.1568 +   "contractible_space(prod_topology X Y) \<longleftrightarrow>
  1.1569 +    topspace X = {} \<or> topspace Y = {} \<or> contractible_space X \<and> contractible_space Y"
  1.1570 +proof (cases "topspace X = {} \<or> topspace Y = {}")
  1.1571 +  case True
  1.1572 +  then have "topspace (prod_topology X Y) = {}"
  1.1573 +    by simp
  1.1574 +  then show ?thesis
  1.1575 +    by (auto simp: contractible_space_empty)
  1.1576 +next
  1.1577 +  case False
  1.1578 +  have "contractible_space(prod_topology X Y) \<longleftrightarrow> contractible_space X \<and> contractible_space Y"
  1.1579 +  proof safe
  1.1580 +    assume XY: "contractible_space (prod_topology X Y)"
  1.1581 +    with False have "retraction_map (prod_topology X Y) X fst"
  1.1582 +      by (auto simp: contractible_space False retraction_map_fst)
  1.1583 +    then show "contractible_space X"
  1.1584 +      by (rule contractible_space_retraction_map_image [OF _ XY])
  1.1585 +    have "retraction_map (prod_topology X Y) Y snd"
  1.1586 +      using False XY  by (auto simp: contractible_space False retraction_map_snd)
  1.1587 +    then show "contractible_space Y"
  1.1588 +      by (rule contractible_space_retraction_map_image [OF _ XY])
  1.1589 +  next
  1.1590 +    assume "contractible_space X" and "contractible_space Y"
  1.1591 +    with False obtain a b
  1.1592 +      where "a \<in> topspace X" and a: "homotopic_with (\<lambda>x. True) X X id (\<lambda>x. a)"
  1.1593 +        and "b \<in> topspace Y" and b: "homotopic_with (\<lambda>x. True) Y Y id (\<lambda>x. b)"
  1.1594 +      by (auto simp: contractible_space)
  1.1595 +    with False show "contractible_space (prod_topology X Y)"
  1.1596 +      apply (simp add: contractible_space)
  1.1597 +      apply (rule_tac x=a in bexI)
  1.1598 +       apply (rule_tac x=b in bexI)
  1.1599 +      using homotopic_with_prod_topology [OF a b]
  1.1600 +    	  apply (metis (no_types, lifting) case_prod_Pair case_prod_beta' eq_id_iff)
  1.1601 +    	 apply auto
  1.1602 +    	done
  1.1603 +  qed
  1.1604 +  with False show ?thesis
  1.1605 +    by auto
  1.1606 +qed
  1.1607 +
  1.1608 +
  1.1609 +
  1.1610 +
  1.1611 +lemma contractible_space_product_topology:
  1.1612 +  "contractible_space(product_topology X I) \<longleftrightarrow>
  1.1613 +    topspace (product_topology X I) = {} \<or> (\<forall>i \<in> I. contractible_space(X i))"
  1.1614 +proof (cases "topspace (product_topology X I) = {}")
  1.1615 +  case False
  1.1616 +  have 1: "contractible_space (X i)"
  1.1617 +    if XI: "contractible_space (product_topology X I)" and "i \<in> I"
  1.1618 +    for i
  1.1619 +  proof (rule contractible_space_retraction_map_image [OF _ XI])
  1.1620 +    show "retraction_map (product_topology X I) (X i) (\<lambda>x. x i)"
  1.1621 +      using False by (simp add: retraction_map_product_projection \<open>i \<in> I\<close>)
  1.1622 +  qed
  1.1623 +  have 2: "contractible_space (product_topology X I)"
  1.1624 +    if "x \<in> topspace (product_topology X I)" and cs: "\<forall>i\<in>I. contractible_space (X i)"
  1.1625 +    for x :: "'a \<Rightarrow> 'b"
  1.1626 +  proof -
  1.1627 +    obtain f where f: "\<And>i. i\<in>I \<Longrightarrow> homotopic_with (\<lambda>x. True) (X i) (X i) id (\<lambda>x. f i)"
  1.1628 +      using cs unfolding contractible_space_def by metis
  1.1629 +    have "homotopic_with (\<lambda>x. True)
  1.1630 +                         (product_topology X I) (product_topology X I) id (\<lambda>x. restrict f I)"
  1.1631 +      by (rule homotopic_with_eq [OF homotopic_with_product_topology [OF f]]) (auto simp: topspace_product_topology)
  1.1632 +    then show ?thesis
  1.1633 +      by (auto simp: contractible_space_def)
  1.1634 +  qed
  1.1635 +  show ?thesis
  1.1636 +    using False 1 2 by blast
  1.1637 +qed (simp add: contractible_space_empty)
  1.1638 +
  1.1639 +
  1.1640 +lemma contractible_space_subtopology_euclideanreal [simp]:
  1.1641 +  "contractible_space(subtopology euclideanreal S) \<longleftrightarrow> is_interval S"
  1.1642 +  (is "?lhs = ?rhs")
  1.1643 +proof
  1.1644 +  assume ?lhs
  1.1645 +  then have "path_connectedin (subtopology euclideanreal S) S"
  1.1646 +    using contractible_imp_path_connected_space path_connectedin_topspace path_connectedin_absolute
  1.1647 +    by (simp add: contractible_imp_path_connected) 
  1.1648 +  then show ?rhs
  1.1649 +    by (simp add: is_interval_path_connected_1)
  1.1650 +next
  1.1651 +  assume ?rhs
  1.1652 +  then have "convex S"
  1.1653 +    by (simp add: is_interval_convex_1)
  1.1654 +  show ?lhs
  1.1655 +  proof (cases "S = {}")
  1.1656 +    case False
  1.1657 +    then obtain z where "z \<in> S"
  1.1658 +      by blast
  1.1659 +    show ?thesis
  1.1660 +      unfolding contractible_space_def homotopic_with_def
  1.1661 +    proof (intro exI conjI allI)
  1.1662 +      show "continuous_map (prod_topology (top_of_set {0..1}) (top_of_set S)) (top_of_set S)
  1.1663 +                           (\<lambda>(t,x). (1 - t) * x + t * z)"
  1.1664 +        apply (auto simp: case_prod_unfold)
  1.1665 +         apply (intro continuous_intros)
  1.1666 +        using  \<open>z \<in> S\<close> apply (auto intro: convexD [OF \<open>convex S\<close>, simplified])
  1.1667 +        done
  1.1668 +    qed auto
  1.1669 +  qed (simp add: contractible_space_empty)
  1.1670 +qed
  1.1671 +
  1.1672 +
  1.1673 +corollary contractible_space_euclideanreal: "contractible_space euclideanreal"
  1.1674 +proof -
  1.1675 +  have "contractible_space (subtopology euclideanreal UNIV)"
  1.1676 +    using contractible_space_subtopology_euclideanreal by blast
  1.1677 +  then show ?thesis
  1.1678 +    by simp
  1.1679 +qed
  1.1680 +
  1.1681 +
  1.1682 +abbreviation%important homotopy_eqv :: "'a::topological_space set \<Rightarrow> 'b::topological_space set \<Rightarrow> bool"
  1.1683 +             (infix "homotopy'_eqv" 50)
  1.1684 +  where "S homotopy_eqv T \<equiv> top_of_set S homotopy_equivalent_space top_of_set T"
  1.1685 +
  1.1686 +
  1.1687 +
  1.1688 +
  1.1689 +
  1.1690 +lemma homeomorphic_imp_homotopy_eqv: "S homeomorphic T \<Longrightarrow> S homotopy_eqv T"
  1.1691 +  unfolding homeomorphic_def homeomorphism_def homotopy_equivalent_space_def
  1.1692 +  apply (erule ex_forward)+
  1.1693 +  apply auto
  1.1694 +   apply (metis homotopic_with_id2 topspace_euclidean_subtopology)
  1.1695 +  by (metis (full_types) homotopic_with_id2 imageE topspace_euclidean_subtopology)
  1.1696 +
  1.1697 +
  1.1698  lemma homotopy_eqv_inj_linear_image:
  1.1699    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
  1.1700    assumes "linear f" "inj f"
  1.1701 @@ -3436,33 +3935,33 @@
  1.1702        and g: "continuous_on U g" "g ` U \<subseteq> T"
  1.1703        and homUS: "\<And>f g. \<lbrakk>continuous_on U f; f ` U \<subseteq> S;
  1.1704                           continuous_on U g; g ` U \<subseteq> S\<rbrakk>
  1.1705 -                         \<Longrightarrow> homotopic_with (\<lambda>x. True) U S f g"
  1.1706 -    shows "homotopic_with (\<lambda>x. True) U T f g"
  1.1707 +                         \<Longrightarrow> homotopic_with_canon (\<lambda>x. True) U S f g"
  1.1708 +    shows "homotopic_with_canon (\<lambda>x. True) U T f g"
  1.1709  proof -
  1.1710    obtain h k where h: "continuous_on S h" "h ` S \<subseteq> T"
  1.1711                 and k: "continuous_on T k" "k ` T \<subseteq> S"
  1.1712 -               and hom: "homotopic_with (\<lambda>x. True) S S (k \<circ> h) id"
  1.1713 -                        "homotopic_with (\<lambda>x. True) T T (h \<circ> k) id"
  1.1714 -    using assms by (auto simp: homotopy_eqv_def)
  1.1715 -  have "homotopic_with (\<lambda>f. True) U S (k \<circ> f) (k \<circ> g)"
  1.1716 +               and hom: "homotopic_with_canon (\<lambda>x. True) S S (k \<circ> h) id"
  1.1717 +                        "homotopic_with_canon (\<lambda>x. True) T T (h \<circ> k) id"
  1.1718 +    using assms by (auto simp: homotopy_equivalent_space_def)
  1.1719 +  have "homotopic_with_canon (\<lambda>f. True) U S (k \<circ> f) (k \<circ> g)"
  1.1720      apply (rule homUS)
  1.1721      using f g k
  1.1722      apply (safe intro!: continuous_on_compose h k f elim!: continuous_on_subset)
  1.1723      apply (force simp: o_def)+
  1.1724      done
  1.1725 -  then have "homotopic_with (\<lambda>x. True) U T (h \<circ> (k \<circ> f)) (h \<circ> (k \<circ> g))"
  1.1726 +  then have "homotopic_with_canon (\<lambda>x. True) U T (h \<circ> (k \<circ> f)) (h \<circ> (k \<circ> g))"
  1.1727      apply (rule homotopic_with_compose_continuous_left)
  1.1728      apply (simp_all add: h)
  1.1729      done
  1.1730 -  moreover have "homotopic_with (\<lambda>x. True) U T (h \<circ> k \<circ> f) (id \<circ> f)"
  1.1731 +  moreover have "homotopic_with_canon (\<lambda>x. True) U T (h \<circ> k \<circ> f) (id \<circ> f)"
  1.1732      apply (rule homotopic_with_compose_continuous_right [where X=T and Y=T])
  1.1733      apply (auto simp: hom f)
  1.1734      done
  1.1735 -  moreover have "homotopic_with (\<lambda>x. True) U T (h \<circ> k \<circ> g) (id \<circ> g)"
  1.1736 +  moreover have "homotopic_with_canon (\<lambda>x. True) U T (h \<circ> k \<circ> g) (id \<circ> g)"
  1.1737      apply (rule homotopic_with_compose_continuous_right [where X=T and Y=T])
  1.1738      apply (auto simp: hom g)
  1.1739      done
  1.1740 -  ultimately show "homotopic_with (\<lambda>x. True) U T f g"
  1.1741 +  ultimately show "homotopic_with_canon (\<lambda>x. True) U T f g"
  1.1742      apply (simp add: o_assoc)
  1.1743      using homotopic_with_trans homotopic_with_sym by blast
  1.1744  qed
  1.1745 @@ -3474,13 +3973,24 @@
  1.1746    assumes "S homotopy_eqv T"
  1.1747      shows "(\<forall>f g. continuous_on U f \<and> f ` U \<subseteq> S \<and>
  1.1748                     continuous_on U g \<and> g ` U \<subseteq> S
  1.1749 -                   \<longrightarrow> homotopic_with (\<lambda>x. True) U S f g) \<longleftrightarrow>
  1.1750 +                   \<longrightarrow> homotopic_with_canon (\<lambda>x. True) U S f g) \<longleftrightarrow>
  1.1751             (\<forall>f g. continuous_on U f \<and> f ` U \<subseteq> T \<and>
  1.1752                    continuous_on U g \<and> g ` U \<subseteq> T
  1.1753 -                  \<longrightarrow> homotopic_with (\<lambda>x. True) U T f g)"
  1.1754 -apply (rule iffI)
  1.1755 -apply (metis assms homotopy_eqv_homotopic_triviality_imp)
  1.1756 -by (metis (no_types) assms homotopy_eqv_homotopic_triviality_imp homotopy_eqv_sym)
  1.1757 +                  \<longrightarrow> homotopic_with_canon (\<lambda>x. True) U T f g)"
  1.1758 +      (is "?lhs = ?rhs")
  1.1759 +proof
  1.1760 +  assume ?lhs
  1.1761 +  then show ?rhs
  1.1762 +    by (metis assms homotopy_eqv_homotopic_triviality_imp)
  1.1763 +next
  1.1764 +  assume ?rhs
  1.1765 +  moreover
  1.1766 +  have "T homotopy_eqv S"
  1.1767 +    using assms homotopy_equivalent_space_sym by blast
  1.1768 +  ultimately show ?lhs
  1.1769 +    by (blast intro: homotopy_eqv_homotopic_triviality_imp)
  1.1770 +qed
  1.1771 +
  1.1772  
  1.1773  lemma homotopy_eqv_cohomotopic_triviality_null_imp:
  1.1774    fixes S :: "'a::real_normed_vector set"
  1.1775 @@ -3489,23 +3999,23 @@
  1.1776    assumes "S homotopy_eqv T"
  1.1777        and f: "continuous_on T f" "f ` T \<subseteq> U"
  1.1778        and homSU: "\<And>f. \<lbrakk>continuous_on S f; f ` S \<subseteq> U\<rbrakk>
  1.1779 -                      \<Longrightarrow> \<exists>c. homotopic_with (\<lambda>x. True) S U f (\<lambda>x. c)"
  1.1780 -  obtains c where "homotopic_with (\<lambda>x. True) T U f (\<lambda>x. c)"
  1.1781 +                      \<Longrightarrow> \<exists>c. homotopic_with_canon (\<lambda>x. True) S U f (\<lambda>x. c)"
  1.1782 +  obtains c where "homotopic_with_canon (\<lambda>x. True) T U f (\<lambda>x. c)"
  1.1783  proof -
  1.1784    obtain h k where h: "continuous_on S h" "h ` S \<subseteq> T"
  1.1785                 and k: "continuous_on T k" "k ` T \<subseteq> S"
  1.1786 -               and hom: "homotopic_with (\<lambda>x. True) S S (k \<circ> h) id"
  1.1787 -                        "homotopic_with (\<lambda>x. True) T T (h \<circ> k) id"
  1.1788 -    using assms by (auto simp: homotopy_eqv_def)
  1.1789 -  obtain c where "homotopic_with (\<lambda>x. True) S U (f \<circ> h) (\<lambda>x. c)"
  1.1790 +               and hom: "homotopic_with_canon (\<lambda>x. True) S S (k \<circ> h) id"
  1.1791 +                        "homotopic_with_canon (\<lambda>x. True) T T (h \<circ> k) id"
  1.1792 +    using assms by (auto simp: homotopy_equivalent_space_def)
  1.1793 +  obtain c where "homotopic_with_canon (\<lambda>x. True) S U (f \<circ> h) (\<lambda>x. c)"
  1.1794      apply (rule exE [OF homSU [of "f \<circ> h"]])
  1.1795      apply (intro continuous_on_compose h)
  1.1796      using h f  apply (force elim!: continuous_on_subset)+
  1.1797      done
  1.1798 -  then have "homotopic_with (\<lambda>x. True) T U ((f \<circ> h) \<circ> k) ((\<lambda>x. c) \<circ> k)"
  1.1799 +  then have "homotopic_with_canon (\<lambda>x. True) T U ((f \<circ> h) \<circ> k) ((\<lambda>x. c) \<circ> k)"
  1.1800      apply (rule homotopic_with_compose_continuous_right [where X=S])
  1.1801      using k by auto
  1.1802 -  moreover have "homotopic_with (\<lambda>x. True) T U (f \<circ> id) (f \<circ> (h \<circ> k))"
  1.1803 +  moreover have "homotopic_with_canon (\<lambda>x. True) T U (f \<circ> id) (f \<circ> (h \<circ> k))"
  1.1804      apply (rule homotopic_with_compose_continuous_left [where Y=T])
  1.1805        apply (simp add: hom homotopic_with_symD)
  1.1806       using f apply auto
  1.1807 @@ -3522,12 +4032,12 @@
  1.1808      and U :: "'c::real_normed_vector set"
  1.1809    assumes "S homotopy_eqv T"
  1.1810      shows "(\<forall>f. continuous_on S f \<and> f ` S \<subseteq> U
  1.1811 -                \<longrightarrow> (\<exists>c. homotopic_with (\<lambda>x. True) S U f (\<lambda>x. c))) \<longleftrightarrow>
  1.1812 +                \<longrightarrow> (\<exists>c. homotopic_with_canon (\<lambda>x. True) S U f (\<lambda>x. c))) \<longleftrightarrow>
  1.1813             (\<forall>f. continuous_on T f \<and> f ` T \<subseteq> U
  1.1814 -                \<longrightarrow> (\<exists>c. homotopic_with (\<lambda>x. True) T U f (\<lambda>x. c)))"
  1.1815 +                \<longrightarrow> (\<exists>c. homotopic_with_canon (\<lambda>x. True) T U f (\<lambda>x. c)))"
  1.1816  apply (rule iffI)
  1.1817  apply (metis assms homotopy_eqv_cohomotopic_triviality_null_imp)
  1.1818 -by (metis assms homotopy_eqv_cohomotopic_triviality_null_imp homotopy_eqv_sym)
  1.1819 +by (metis assms homotopy_eqv_cohomotopic_triviality_null_imp homotopy_equivalent_space_sym)
  1.1820  
  1.1821  lemma homotopy_eqv_homotopic_triviality_null_imp:
  1.1822    fixes S :: "'a::real_normed_vector set"
  1.1823 @@ -3536,23 +4046,23 @@
  1.1824    assumes "S homotopy_eqv T"
  1.1825        and f: "continuous_on U f" "f ` U \<subseteq> T"
  1.1826        and homSU: "\<And>f. \<lbrakk>continuous_on U f; f ` U \<subseteq> S\<rbrakk>
  1.1827 -                      \<Longrightarrow> \<exists>c. homotopic_with (\<lambda>x. True) U S f (\<lambda>x. c)"
  1.1828 -    shows "\<exists>c. homotopic_with (\<lambda>x. True) U T f (\<lambda>x. c)"
  1.1829 +                      \<Longrightarrow> \<exists>c. homotopic_with_canon (\<lambda>x. True) U S f (\<lambda>x. c)"
  1.1830 +    shows "\<exists>c. homotopic_with_canon (\<lambda>x. True) U T f (\<lambda>x. c)"
  1.1831  proof -
  1.1832    obtain h k where h: "continuous_on S h" "h ` S \<subseteq> T"
  1.1833                 and k: "continuous_on T k" "k ` T \<subseteq> S"
  1.1834 -               and hom: "homotopic_with (\<lambda>x. True) S S (k \<circ> h) id"
  1.1835 -                        "homotopic_with (\<lambda>x. True) T T (h \<circ> k) id"
  1.1836 -    using assms by (auto simp: homotopy_eqv_def)
  1.1837 -  obtain c::'a where "homotopic_with (\<lambda>x. True) U S (k \<circ> f) (\<lambda>x. c)"
  1.1838 +               and hom: "homotopic_with_canon (\<lambda>x. True) S S (k \<circ> h) id"
  1.1839 +                        "homotopic_with_canon (\<lambda>x. True) T T (h \<circ> k) id"
  1.1840 +    using assms by (auto simp: homotopy_equivalent_space_def)
  1.1841 +  obtain c::'a where "homotopic_with_canon (\<lambda>x. True) U S (k \<circ> f) (\<lambda>x. c)"
  1.1842      apply (rule exE [OF homSU [of "k \<circ> f"]])
  1.1843      apply (intro continuous_on_compose h)
  1.1844      using k f  apply (force elim!: continuous_on_subset)+
  1.1845      done
  1.1846 -  then have "homotopic_with (\<lambda>x. True) U T (h \<circ> (k \<circ> f)) (h \<circ> (\<lambda>x. c))"
  1.1847 +  then have "homotopic_with_canon (\<lambda>x. True) U T (h \<circ> (k \<circ> f)) (h \<circ> (\<lambda>x. c))"
  1.1848      apply (rule homotopic_with_compose_continuous_left [where Y=S])
  1.1849      using h by auto
  1.1850 -  moreover have "homotopic_with (\<lambda>x. True) U T (id \<circ> f) ((h \<circ> k) \<circ> f)"
  1.1851 +  moreover have "homotopic_with_canon (\<lambda>x. True) U T (id \<circ> f) ((h \<circ> k) \<circ> f)"
  1.1852      apply (rule homotopic_with_compose_continuous_right [where X=T])
  1.1853        apply (simp add: hom homotopic_with_symD)
  1.1854       using f apply auto
  1.1855 @@ -3567,12 +4077,12 @@
  1.1856      and U :: "'c::real_normed_vector set"
  1.1857    assumes "S homotopy_eqv T"
  1.1858      shows "(\<forall>f. continuous_on U f \<and> f ` U \<subseteq> S
  1.1859 -                  \<longrightarrow> (\<exists>c. homotopic_with (\<lambda>x. True) U S f (\<lambda>x. c))) \<longleftrightarrow>
  1.1860 +                  \<longrightarrow> (\<exists>c. homotopic_with_canon (\<lambda>x. True) U S f (\<lambda>x. c))) \<longleftrightarrow>
  1.1861             (\<forall>f. continuous_on U f \<and> f ` U \<subseteq> T
  1.1862 -                  \<longrightarrow> (\<exists>c. homotopic_with (\<lambda>x. True) U T f (\<lambda>x. c)))"
  1.1863 +                  \<longrightarrow> (\<exists>c. homotopic_with_canon (\<lambda>x. True) U T f (\<lambda>x. c)))"
  1.1864  apply (rule iffI)
  1.1865  apply (metis assms homotopy_eqv_homotopic_triviality_null_imp)
  1.1866 -by (metis assms homotopy_eqv_homotopic_triviality_null_imp homotopy_eqv_sym)
  1.1867 +by (metis assms homotopy_eqv_homotopic_triviality_null_imp homotopy_equivalent_space_sym)
  1.1868  
  1.1869  lemma homotopy_eqv_contractible_sets:
  1.1870    fixes S :: "'a::real_normed_vector set"
  1.1871 @@ -3587,7 +4097,7 @@
  1.1872    with assms obtain a b where "a \<in> S" "b \<in> T"
  1.1873      by auto
  1.1874    then show ?thesis
  1.1875 -    unfolding homotopy_eqv_def
  1.1876 +    unfolding homotopy_equivalent_space_def
  1.1877      apply (rule_tac x="\<lambda>x. b" in exI)
  1.1878      apply (rule_tac x="\<lambda>x. a" in exI)
  1.1879      apply (intro assms conjI continuous_on_id' homotopic_into_contractible)
  1.1880 @@ -3598,20 +4108,19 @@
  1.1881  lemma homotopy_eqv_empty1 [simp]:
  1.1882    fixes S :: "'a::real_normed_vector set"
  1.1883    shows "S homotopy_eqv ({}::'b::real_normed_vector set) \<longleftrightarrow> S = {}"
  1.1884 -apply (rule iffI)
  1.1885 -using homotopy_eqv_def apply fastforce
  1.1886 -by (simp add: homotopy_eqv_contractible_sets)
  1.1887 +  apply (rule iffI)
  1.1888 +   apply (metis Abstract_Topology.continuous_map_subtopology_eu emptyE equals0I homotopy_equivalent_space_def image_subset_iff)
  1.1889 +  by (simp add: homotopy_eqv_contractible_sets)
  1.1890  
  1.1891  lemma homotopy_eqv_empty2 [simp]:
  1.1892    fixes S :: "'a::real_normed_vector set"
  1.1893    shows "({}::'b::real_normed_vector set) homotopy_eqv S \<longleftrightarrow> S = {}"
  1.1894 -by (metis homotopy_eqv_empty1 homotopy_eqv_sym)
  1.1895 +  using homotopy_equivalent_space_sym homotopy_eqv_empty1 by blast
  1.1896  
  1.1897  lemma homotopy_eqv_contractibility:
  1.1898    fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set"
  1.1899    shows "S homotopy_eqv T \<Longrightarrow> (contractible S \<longleftrightarrow> contractible T)"
  1.1900 -unfolding homotopy_eqv_def
  1.1901 -by (blast intro: homotopy_dominated_contractibility)
  1.1902 +  by (meson contractible_space_top_of_set homotopy_equivalent_space_contractibility)
  1.1903  
  1.1904  lemma homotopy_eqv_sing:
  1.1905    fixes S :: "'a::real_normed_vector set" and a :: "'b::real_normed_vector"
  1.1906 @@ -5034,11 +5543,15 @@
  1.1907  
  1.1908  proposition nullhomotopic_from_sphere_extension:
  1.1909    fixes f :: "'M::euclidean_space \<Rightarrow> 'a::real_normed_vector"
  1.1910 -  shows  "(\<exists>c. homotopic_with (\<lambda>x. True) (sphere a r) S f (\<lambda>x. c)) \<longleftrightarrow>
  1.1911 +  shows  "(\<exists>c. homotopic_with_canon (\<lambda>x. True) (sphere a r) S f (\<lambda>x. c)) \<longleftrightarrow>
  1.1912            (\<exists>g. continuous_on (cball a r) g \<and> g ` (cball a r) \<subseteq> S \<and>
  1.1913                 (\<forall>x \<in> sphere a r. g x = f x))"
  1.1914           (is "?lhs = ?rhs")
  1.1915  proof (cases r "0::real" rule: linorder_cases)
  1.1916 +  case less
  1.1917 +  then show ?thesis
  1.1918 +    by (simp add: homotopic_on_emptyI)
  1.1919 +next
  1.1920    case equal
  1.1921    then show ?thesis
  1.1922      apply (auto simp: homotopic_with)
  1.1923 @@ -5051,9 +5564,11 @@
  1.1924    have ?P if ?lhs using that
  1.1925    proof
  1.1926      fix c
  1.1927 -    assume c: "homotopic_with (\<lambda>x. True) (sphere a r) S f (\<lambda>x. c)"
  1.1928 -    then have contf: "continuous_on (sphere a r) f" and fim: "f ` sphere a r \<subseteq> S"
  1.1929 -      by (auto simp: homotopic_with_imp_subset1 homotopic_with_imp_continuous)
  1.1930 +    assume c: "homotopic_with_canon (\<lambda>x. True) (sphere a r) S f (\<lambda>x. c)"
  1.1931 +    then have contf: "continuous_on (sphere a r) f" 
  1.1932 +      by (metis homotopic_with_imp_continuous)
  1.1933 +    moreover have fim: "f ` sphere a r \<subseteq> S"
  1.1934 +      by (meson continuous_map_subtopology_eu c homotopic_with_imp_continuous_maps)
  1.1935      show ?P
  1.1936        using contf fim by (auto simp: sphere_def dist_norm norm_minus_commute)
  1.1937    qed
  1.1938 @@ -5070,7 +5585,7 @@
  1.1939    moreover have ?thesis if ?P
  1.1940    proof
  1.1941      assume ?lhs
  1.1942 -    then obtain c where "homotopic_with (\<lambda>x. True) (sphere a r) S (\<lambda>x. c) f"
  1.1943 +    then obtain c where "homotopic_with_canon (\<lambda>x. True) (sphere a r) S (\<lambda>x. c) f"
  1.1944        using homotopic_with_sym by blast
  1.1945      then obtain h where conth: "continuous_on ({0..1::real} \<times> sphere a r) h"
  1.1946                      and him: "h ` ({0..1} \<times> sphere a r) \<subseteq> S"
  1.1947 @@ -5159,6 +5674,6 @@
  1.1948    qed
  1.1949    ultimately
  1.1950    show ?thesis by meson
  1.1951 -qed simp
  1.1952 +qed 
  1.1953  
  1.1954  end
  1.1955 \ No newline at end of file