# HG changeset patch
# User paulson
# Date 1553619715 0
# Node ID e7648f104d6bc6feda259ae0b165fd15b59a130f
# Parent  8e916ed23d17fcdeb6f002eb5ee2b851e7b4e56f# Parent  f2d327275065081bd4038080c17ae921de3066fd
merged

diff -r 8e916ed23d17 -r e7648f104d6b src/HOL/Analysis/Abstract_Topology.thy
--- a/src/HOL/Analysis/Abstract_Topology.thy	Tue Mar 26 16:27:29 2019 +0100
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Tue Mar 26 17:01:55 2019 +0000
@@ -1609,6 +1609,8 @@
   qed
 qed (auto simp: continuous_map_on_empty)
 
+declare continuous_map_const [THEN iffD2, continuous_intros]
+
 lemma continuous_map_compose:
   assumes f: "continuous_map X X' f" and g: "continuous_map X' X'' g"
   shows "continuous_map X X'' (g \<circ> f)"
@@ -3773,6 +3775,13 @@
   shows "closedin (top_of_set S) (S \<inter> f -` T)"
   using assms continuous_on_closed by blast
 
+lemma continuous_map_subtopology_eu [simp]:
+  "continuous_map (subtopology euclidean S) (subtopology euclidean T) h \<longleftrightarrow> continuous_on S h \<and> h ` S \<subseteq> T"
+  apply safe
+  apply (metis continuous_map_closedin_preimage_eq continuous_map_in_subtopology continuous_on_closed order_refl topspace_euclidean_subtopology)
+  apply (simp add: continuous_map_closedin_preimage_eq image_subset_iff)
+  by (metis (no_types, hide_lams) continuous_map_closedin_preimage_eq continuous_map_in_subtopology continuous_on_closed order_refl topspace_euclidean_subtopology)
+
 subsection%unimportant \<open>Half-global and completely global cases\<close>
 
 lemma continuous_openin_preimage_gen:
diff -r 8e916ed23d17 -r e7648f104d6b src/HOL/Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Tue Mar 26 16:27:29 2019 +0100
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Tue Mar 26 17:01:55 2019 +0000
@@ -49,10 +49,10 @@
   assumes ts: "T retract_of S"
       and hom: "\<And>f g. \<lbrakk>continuous_on U f; f ` U \<subseteq> S;
                        continuous_on U g; g ` U \<subseteq> S\<rbrakk>
-                       \<Longrightarrow> homotopic_with (\<lambda>x. True) U S f g"
+                       \<Longrightarrow> homotopic_with_canon (\<lambda>x. True) U S f g"
       and "continuous_on U f" "f ` U \<subseteq> T"
       and "continuous_on U g" "g ` U \<subseteq> T"
-    shows "homotopic_with (\<lambda>x. True) U T f g"
+    shows "homotopic_with_canon (\<lambda>x. True) U T f g"
 proof -
   obtain r where "r ` S \<subseteq> S" "continuous_on S r" "\<forall>x\<in>S. r (r x) = r x" "T = r ` S"
     using ts by (auto simp: retract_of_def retraction)
@@ -69,9 +69,9 @@
 lemma retract_of_homotopically_trivial_null:
   assumes ts: "T retract_of S"
       and hom: "\<And>f. \<lbrakk>continuous_on U f; f ` U \<subseteq> S\<rbrakk>
-                     \<Longrightarrow> \<exists>c. homotopic_with (\<lambda>x. True) U S f (\<lambda>x. c)"
+                     \<Longrightarrow> \<exists>c. homotopic_with_canon (\<lambda>x. True) U S f (\<lambda>x. c)"
       and "continuous_on U f" "f ` U \<subseteq> T"
-  obtains c where "homotopic_with (\<lambda>x. True) U T f (\<lambda>x. c)"
+  obtains c where "homotopic_with_canon (\<lambda>x. True) U T f (\<lambda>x. c)"
 proof -
   obtain r where "r ` S \<subseteq> S" "continuous_on S r" "\<forall>x\<in>S. r (r x) = r x" "T = r ` S"
     using ts by (auto simp: retract_of_def retraction)
@@ -98,8 +98,8 @@
   by (metis locally_compact_closedin closedin_retract)
 
 lemma homotopic_into_retract:
-   "\<lbrakk>f ` S \<subseteq> T; g ` S \<subseteq> T; T retract_of U; homotopic_with (\<lambda>x. True) S U f g\<rbrakk>
-        \<Longrightarrow> homotopic_with (\<lambda>x. True) S T f g"
+   "\<lbrakk>f ` S \<subseteq> T; g ` S \<subseteq> T; T retract_of U; homotopic_with_canon (\<lambda>x. True) S U f g\<rbrakk>
+        \<Longrightarrow> homotopic_with_canon (\<lambda>x. True) S T f g"
 apply (subst (asm) homotopic_with_def)
 apply (simp add: homotopic_with retract_of_def retraction_def, clarify)
 apply (rule_tac x="r \<circ> h" in exI)
@@ -122,24 +122,24 @@
 
 lemma deformation_retract_imp_homotopy_eqv:
   fixes S :: "'a::euclidean_space set"
-  assumes "homotopic_with (\<lambda>x. True) S S id r" and r: "retraction S T r"
+  assumes "homotopic_with_canon (\<lambda>x. True) S S id r" and r: "retraction S T r"
   shows "S homotopy_eqv T"
 proof -
-  have "homotopic_with (\<lambda>x. True) S S (id \<circ> r) id"
+  have "homotopic_with_canon (\<lambda>x. True) S S (id \<circ> r) id"
     by (simp add: assms(1) homotopic_with_symD)
-  moreover have "homotopic_with (\<lambda>x. True) T T (r \<circ> id) id"
+  moreover have "homotopic_with_canon (\<lambda>x. True) T T (r \<circ> id) id"
     using r unfolding retraction_def
-    by (metis (no_types, lifting) comp_id continuous_on_id' homotopic_with_equal homotopic_with_symD id_def image_id order_refl)
+    by (metis eq_id_iff homotopic_with_id2 topspace_euclidean_subtopology)
   ultimately
   show ?thesis
-    unfolding homotopy_eqv_def
-    by (metis continuous_on_id' id_def image_id r retraction_def)
+    unfolding homotopy_equivalent_space_def 
+    by (metis (no_types, lifting) continuous_map_subtopology_eu continuous_on_id' id_def image_id r retraction_def)
 qed
 
 lemma deformation_retract:
   fixes S :: "'a::euclidean_space set"
-    shows "(\<exists>r. homotopic_with (\<lambda>x. True) S S id r \<and> retraction S T r) \<longleftrightarrow>
-           T retract_of S \<and> (\<exists>f. homotopic_with (\<lambda>x. True) S S id f \<and> f ` S \<subseteq> T)"
+    shows "(\<exists>r. homotopic_with_canon (\<lambda>x. True) S S id r \<and> retraction S T r) \<longleftrightarrow>
+           T retract_of S \<and> (\<exists>f. homotopic_with_canon (\<lambda>x. True) S S id f \<and> f ` S \<subseteq> T)"
     (is "?lhs = ?rhs")
 proof
   assume ?lhs
@@ -160,11 +160,11 @@
 lemma deformation_retract_of_contractible_sing:
   fixes S :: "'a::euclidean_space set"
   assumes "contractible S" "a \<in> S"
-  obtains r where "homotopic_with (\<lambda>x. True) S S id r" "retraction S {a} r"
+  obtains r where "homotopic_with_canon (\<lambda>x. True) S S id r" "retraction S {a} r"
 proof -
   have "{a} retract_of S"
     by (simp add: \<open>a \<in> S\<close>)
-  moreover have "homotopic_with (\<lambda>x. True) S S id (\<lambda>x. a)"
+  moreover have "homotopic_with_canon (\<lambda>x. True) S S id (\<lambda>x. a)"
       using assms
       by (auto simp: contractible_def homotopic_into_contractible image_subset_iff)
   moreover have "(\<lambda>x. a) ` S \<subseteq> {a}"
@@ -3392,7 +3392,7 @@
       and arelS: "a \<in> rel_interior S"
       and relS: "rel_frontier S \<subseteq> T"
       and affS: "T \<subseteq> affine hull S"
-  obtains r where "homotopic_with (\<lambda>x. True) (T - {a}) (T - {a}) id r"
+  obtains r where "homotopic_with_canon (\<lambda>x. True) (T - {a}) (T - {a}) id r"
                   "retraction (T - {a}) (rel_frontier S) r"
 proof -
   have "\<exists>d. 0 < d \<and> (a + d *\<^sub>R l) \<in> rel_frontier S \<and>
@@ -3466,7 +3466,7 @@
     by (blast intro: continuous_on_subset)
   show ?thesis
   proof
-    show "homotopic_with (\<lambda>x. True) (T - {a}) (T - {a}) id (\<lambda>x. a + dd (x - a) *\<^sub>R (x - a))"
+    show "homotopic_with_canon (\<lambda>x. True) (T - {a}) (T - {a}) id (\<lambda>x. a + dd (x - a) *\<^sub>R (x - a))"
     proof (rule homotopic_with_linear)
       show "continuous_on (T - {a}) id"
         by (intro continuous_intros continuous_on_compose)
@@ -3560,8 +3560,7 @@
   apply (rule rel_frontier_deformation_retract_of_punctured_convex [of S T])
   using assms
   apply auto
-  apply (subst homotopy_eqv_sym)
-  using deformation_retract_imp_homotopy_eqv by blast
+  using deformation_retract_imp_homotopy_eqv homotopy_equivalent_space_sym by blast
 
 lemma homotopy_eqv_rel_frontier_punctured_affine_hull:
   fixes S :: "'a::euclidean_space set"
@@ -3600,7 +3599,7 @@
 
 lemma Borsuk_maps_homotopic_in_path_component:
   assumes "path_component (- s) a b"
-    shows "homotopic_with (\<lambda>x. True) s (sphere 0 1)
+    shows "homotopic_with_canon (\<lambda>x. True) s (sphere 0 1)
                    (\<lambda>x. inverse(norm(x - a)) *\<^sub>R (x - a))
                    (\<lambda>x. inverse(norm(x - b)) *\<^sub>R (x - b))"
 proof -
@@ -4128,8 +4127,8 @@
       and anr: "(ANR S \<and> ANR T) \<or> ANR U"
       and contf: "continuous_on T f"
       and "f ` T \<subseteq> U"
-      and "homotopic_with (\<lambda>x. True) S U f g"
-   obtains g' where "homotopic_with (\<lambda>x. True) T U f g'"
+      and "homotopic_with_canon (\<lambda>x. True) S U f g"
+   obtains g' where "homotopic_with_canon (\<lambda>x. True) T U f g'"
                     "continuous_on T g'" "image g' T \<subseteq> U"
                     "\<And>x. x \<in> S \<Longrightarrow> g' x = g x"
 proof -
@@ -4141,9 +4140,9 @@
   define h' where "h' \<equiv>  \<lambda>z. if snd z \<in> S then h z else (f \<circ> snd) z"
   define B where "B \<equiv> {0::real} \<times> T \<union> {0..1} \<times> S"
   have clo0T: "closedin (top_of_set ({0..1} \<times> T)) ({0::real} \<times> T)"
-    by (simp add: closedin_subtopology_refl closedin_Times)
+    by (simp add: Abstract_Topology.closedin_Times)
   moreover have cloT1S: "closedin (top_of_set ({0..1} \<times> T)) ({0..1} \<times> S)"
-    by (simp add: closedin_subtopology_refl closedin_Times assms)
+    by (simp add: Abstract_Topology.closedin_Times assms)
   ultimately have clo0TB:"closedin (top_of_set ({0..1} \<times> T)) B"
     by (auto simp: B_def)
   have cloBS: "closedin (top_of_set B) ({0..1} \<times> S)"
@@ -4225,7 +4224,7 @@
   qed
   show ?thesis
   proof
-    show hom: "homotopic_with (\<lambda>x. True) T U f (\<lambda>x. k (a x, x))"
+    show hom: "homotopic_with_canon (\<lambda>x. True) T U f (\<lambda>x. k (a x, x))"
     proof (simp add: homotopic_with, intro exI conjI)
       show "continuous_on ({0..1} \<times> T) (k \<circ> (\<lambda>z. (fst z *\<^sub>R (a \<circ> snd) z, snd z)))"
         apply (intro continuous_on_compose continuous_intros)
@@ -4241,7 +4240,7 @@
         by auto
     qed
   show "continuous_on T (\<lambda>x. k (a x, x))"
-    using hom homotopic_with_imp_continuous by blast
+    using homotopic_with_imp_continuous_maps [OF hom] by auto
   show "(\<lambda>x. k (a x, x)) ` T \<subseteq> U"
   proof clarify
     fix t
@@ -4262,12 +4261,12 @@
       and "ANR T"
       and fim: "f ` S \<subseteq> T"
       and "S \<noteq> {}"
-   shows "(\<exists>c. homotopic_with (\<lambda>x. True) S T f (\<lambda>x. c)) \<longleftrightarrow>
+   shows "(\<exists>c. homotopic_with_canon (\<lambda>x. True) S T f (\<lambda>x. c)) \<longleftrightarrow>
           (\<exists>g. continuous_on UNIV g \<and> range g \<subseteq> T \<and> (\<forall>x \<in> S. g x = f x))"
        (is "?lhs = ?rhs")
 proof
   assume ?lhs
-  then obtain c where c: "homotopic_with (\<lambda>x. True) S T (\<lambda>x. c) f"
+  then obtain c where c: "homotopic_with_canon (\<lambda>x. True) S T (\<lambda>x. c) f"
     by (blast intro: homotopic_with_symD)
   have "closedin (top_of_set UNIV) S"
     using \<open>closed S\<close> closed_closedin by fastforce
@@ -4281,14 +4280,12 @@
   assume ?rhs
   then obtain g where "continuous_on UNIV g" "range g \<subseteq> T" "\<And>x. x\<in>S \<Longrightarrow> g x = f x"
     by blast
-  then obtain c where "homotopic_with (\<lambda>h. True) UNIV T g (\<lambda>x. c)"
+  then obtain c where "homotopic_with_canon (\<lambda>h. True) UNIV T g (\<lambda>x. c)"
     using nullhomotopic_from_contractible [of UNIV g T] contractible_UNIV by blast
+  then have "homotopic_with_canon (\<lambda>x. True) S T g (\<lambda>x. c)"
+    by (simp add: homotopic_from_subtopology)
   then show ?lhs
-    apply (rule_tac x=c in exI)
-    apply (rule homotopic_with_eq [of _ _ _ g "\<lambda>x. c"])
-    apply (rule homotopic_with_subset_left)
-    apply (auto simp: \<open>\<And>x. x \<in> S \<Longrightarrow> g x = f x\<close>)
-    done
+    by (force elim: homotopic_with_eq [of _ _ _ g "\<lambda>x. c"] simp: \<open>\<And>x. x \<in> S \<Longrightarrow> g x = f x\<close>)
 qed
 
 corollary%unimportant nullhomotopic_into_rel_frontier_extension:
@@ -4298,7 +4295,7 @@
       and "convex T" "bounded T"
       and fim: "f ` S \<subseteq> rel_frontier T"
       and "S \<noteq> {}"
-   shows "(\<exists>c. homotopic_with (\<lambda>x. True) S (rel_frontier T) f (\<lambda>x. c)) \<longleftrightarrow>
+   shows "(\<exists>c. homotopic_with_canon (\<lambda>x. True) S (rel_frontier T) f (\<lambda>x. c)) \<longleftrightarrow>
           (\<exists>g. continuous_on UNIV g \<and> range g \<subseteq> rel_frontier T \<and> (\<forall>x \<in> S. g x = f x))"
 by (simp add: nullhomotopic_into_ANR_extension assms ANR_rel_frontier_convex)
 
@@ -4306,7 +4303,7 @@
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b :: euclidean_space"
   assumes "closed S" and contf: "continuous_on S f"
       and "S \<noteq> {}" and fim: "f ` S \<subseteq> sphere a r"
-    shows "((\<exists>c. homotopic_with (\<lambda>x. True) S (sphere a r) f (\<lambda>x. c)) \<longleftrightarrow>
+    shows "((\<exists>c. homotopic_with_canon (\<lambda>x. True) S (sphere a r) f (\<lambda>x. c)) \<longleftrightarrow>
            (\<exists>g. continuous_on UNIV g \<and> range g \<subseteq> sphere a r \<and> (\<forall>x \<in> S. g x = f x)))"
            (is "?lhs = ?rhs")
 proof (cases "r = 0")
@@ -4328,7 +4325,7 @@
   fixes a :: "'a :: euclidean_space"
   assumes "compact S" and "a \<notin> S"
    shows "bounded (connected_component_set (- S) a) \<longleftrightarrow>
-          \<not>(\<exists>c. homotopic_with (\<lambda>x. True) S (sphere 0 1)
+          \<not>(\<exists>c. homotopic_with_canon (\<lambda>x. True) S (sphere 0 1)
                                (\<lambda>x. inverse(norm(x - a)) *\<^sub>R (x - a)) (\<lambda>x. c))"
    (is "?lhs = ?rhs")
 proof (cases "S = {}")
@@ -4368,13 +4365,13 @@
       using bounded_iff linear by blast
     then have bnot: "b \<notin> ball 0 r"
       by simp
-    have "homotopic_with (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. (x - a) /\<^sub>R norm (x - a))
+    have "homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. (x - a) /\<^sub>R norm (x - a))
                                                    (\<lambda>x. (x - b) /\<^sub>R norm (x - b))"
       apply (rule Borsuk_maps_homotopic_in_path_component)
       using \<open>closed S\<close> b open_Compl open_path_connected_component apply fastforce
       done
     moreover
-    obtain c where "homotopic_with (\<lambda>x. True) (ball 0 r) (sphere 0 1)
+    obtain c where "homotopic_with_canon (\<lambda>x. True) (ball 0 r) (sphere 0 1)
                                    (\<lambda>x. inverse (norm (x - b)) *\<^sub>R (x - b)) (\<lambda>x. c)"
     proof (rule nullhomotopic_from_contractible)
       show "contractible (ball (0::'a) r)"
@@ -4384,8 +4381,7 @@
       show "(\<lambda>x. (x - b) /\<^sub>R norm (x - b)) ` ball 0 r \<subseteq> sphere 0 1"
         using bnot Borsuk_map_into_sphere by blast
     qed blast
-    ultimately have "homotopic_with (\<lambda>x. True) S (sphere 0 1)
-                         (\<lambda>x. (x - a) /\<^sub>R norm (x - a)) (\<lambda>x. c)"
+    ultimately have "homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. (x - a) /\<^sub>R norm (x - a)) (\<lambda>x. c)"
       by (meson homotopic_with_subset_left homotopic_with_trans r)
     then show "\<not> ?rhs"
       by blast
@@ -4397,7 +4393,7 @@
   fixes a :: "'a :: euclidean_space"
   assumes "compact S" and "a \<notin> S"and "b \<notin> S"
       and boc: "bounded (connected_component_set (- S) a)"
-      and hom: "homotopic_with (\<lambda>x. True) S (sphere 0 1)
+      and hom: "homotopic_with_canon (\<lambda>x. True) S (sphere 0 1)
                                (\<lambda>x. (x - a) /\<^sub>R norm (x - a))
                                (\<lambda>x. (x - b) /\<^sub>R norm (x - b))"
    shows "connected_component (- S) a b"
@@ -4418,7 +4414,7 @@
       by (simp add: \<open>b \<notin> S\<close> notcc continuous_on_Borsuk_map)
     show "(\<lambda>x. (x - b) /\<^sub>R norm (x - b)) ` ?T \<subseteq> sphere 0 1"
       by (simp add: \<open>b \<notin> S\<close> notcc Borsuk_map_into_sphere)
-    show "homotopic_with (\<lambda>x. True) S (sphere 0 1)
+    show "homotopic_with_canon (\<lambda>x. True) S (sphere 0 1)
              (\<lambda>x. (x - b) /\<^sub>R norm (x - b)) (\<lambda>x. (x - a) /\<^sub>R norm (x - a))"
       by (simp add: hom homotopic_with_symD)
     qed (auto simp: ANR_sphere intro: that)
@@ -4429,7 +4425,7 @@
 lemma Borsuk_maps_homotopic_in_connected_component_eq:
   fixes a :: "'a :: euclidean_space"
   assumes S: "compact S" "a \<notin> S" "b \<notin> S" and 2: "2 \<le> DIM('a)"
-    shows "(homotopic_with (\<lambda>x. True) S (sphere 0 1)
+    shows "(homotopic_with_canon (\<lambda>x. True) S (sphere 0 1)
                    (\<lambda>x. (x - a) /\<^sub>R norm (x - a))
                    (\<lambda>x. (x - b) /\<^sub>R norm (x - b)) \<longleftrightarrow>
            connected_component (- S) a b)"
@@ -4587,9 +4583,9 @@
   assumes contf: "continuous_on S f" and fim: "f ` S \<subseteq> U"
       and contg: "continuous_on S g" and gim: "g ` S \<subseteq> U"
       and clo: "closedin (top_of_set S) T"
-      and "ANR U" and hom: "homotopic_with (\<lambda>x. True) T U f g"
+      and "ANR U" and hom: "homotopic_with_canon (\<lambda>x. True) T U f g"
     obtains V where "T \<subseteq> V" "openin (top_of_set S) V"
-                    "homotopic_with (\<lambda>x. True) V U f g"
+                    "homotopic_with_canon (\<lambda>x. True) V U f g"
 proof -
   have "T \<subseteq> S"
     using clo closedin_imp_subset by blast
@@ -4631,7 +4627,7 @@
   obtain T' where opeT': "openin (top_of_set S) T'" 
               and "T \<subseteq> T'" and TW: "{0..1} \<times> T' \<subseteq> W"
     using tube_lemma_gen [of "{0..1::real}" T S W] W \<open>T \<subseteq> S\<close> opeW by auto
-  moreover have "homotopic_with (\<lambda>x. True) T' U f g"
+  moreover have "homotopic_with_canon (\<lambda>x. True) T' U f g"
   proof (simp add: homotopic_with, intro exI conjI)
     show "continuous_on ({0..1} \<times> T') k"
       using TW continuous_on_subset contk by auto
@@ -4651,8 +4647,8 @@
   fixes \<F> :: "'a::euclidean_space set set"
   assumes "\<And>S. S \<in> \<F> \<Longrightarrow> closedin (top_of_set (\<Union>\<F>)) S"
       and "\<And>S. S \<in> \<F> \<Longrightarrow> openin (top_of_set (\<Union>\<F>)) S"
-      and "\<And>S. S \<in> \<F> \<Longrightarrow> homotopic_with (\<lambda>x. True) S T f g"
-  shows "homotopic_with (\<lambda>x. True) (\<Union>\<F>) T f g"
+      and "\<And>S. S \<in> \<F> \<Longrightarrow> homotopic_with_canon (\<lambda>x. True) S T f g"
+  shows "homotopic_with_canon (\<lambda>x. True) (\<Union>\<F>) T f g"
 proof -
   obtain \<V> where "\<V> \<subseteq> \<F>" "countable \<V>" and eqU: "\<Union>\<V> = \<Union>\<F>"
     using Lindelof_openin assms by blast
@@ -4660,14 +4656,14 @@
   proof (cases "\<V> = {}")
     case True
     then show ?thesis
-      by (metis Union_empty eqU homotopic_on_empty)
+      by (metis Union_empty eqU homotopic_with_canon_on_empty)
   next
     case False
     then obtain V :: "nat \<Rightarrow> 'a set" where V: "range V = \<V>"
       using range_from_nat_into \<open>countable \<V>\<close> by metis
     with \<open>\<V> \<subseteq> \<F>\<close> have clo: "\<And>n. closedin (top_of_set (\<Union>\<F>)) (V n)"
                   and ope: "\<And>n. openin (top_of_set (\<Union>\<F>)) (V n)"
-                  and hom: "\<And>n. homotopic_with (\<lambda>x. True) (V n) T f g"
+                  and hom: "\<And>n. homotopic_with_canon (\<lambda>x. True) (V n) T f g"
       using assms by auto 
     then obtain h where conth: "\<And>n. continuous_on ({0..1::real} \<times> V n) (h n)"
                   and him: "\<And>n. h n ` ({0..1} \<times> V n) \<subseteq> T" 
@@ -4723,9 +4719,9 @@
 lemma homotopic_on_components_eq:
   fixes S :: "'a :: euclidean_space set" and T :: "'b :: euclidean_space set"
   assumes S: "locally connected S \<or> compact S" and "ANR T"
-  shows "homotopic_with (\<lambda>x. True) S T f g \<longleftrightarrow>
+  shows "homotopic_with_canon (\<lambda>x. True) S T f g \<longleftrightarrow>
          (continuous_on S f \<and> f ` S \<subseteq> T \<and> continuous_on S g \<and> g ` S \<subseteq> T) \<and>
-         (\<forall>C \<in> components S. homotopic_with (\<lambda>x. True) C T f g)"
+         (\<forall>C \<in> components S. homotopic_with_canon (\<lambda>x. True) C T f g)"
     (is "?lhs \<longleftrightarrow> ?C \<and> ?rhs")
 proof -
   have "continuous_on S f" "f ` S \<subseteq> T" "continuous_on S g" "g ` S \<subseteq> T" if ?lhs
@@ -4740,7 +4736,7 @@
     assume R: ?rhs
     have "\<exists>U. C \<subseteq> U \<and> closedin (top_of_set S) U \<and>
               openin (top_of_set S) U \<and>
-              homotopic_with (\<lambda>x. True) U T f g" if C: "C \<in> components S" for C
+              homotopic_with_canon (\<lambda>x. True) U T f g" if C: "C \<in> components S" for C
     proof -
       have "C \<subseteq> S"
         by (simp add: in_components_subset that)
@@ -4754,15 +4750,15 @@
             by (simp add: closedin_component that)
           show "openin (top_of_set S) C"
             by (simp add: \<open>locally connected S\<close> openin_components_locally_connected that)
-          show "homotopic_with (\<lambda>x. True) C T f g"
+          show "homotopic_with_canon (\<lambda>x. True) C T f g"
             by (simp add: R that)
         qed auto
       next
         assume "compact S"
-        have hom: "homotopic_with (\<lambda>x. True) C T f g"
+        have hom: "homotopic_with_canon (\<lambda>x. True) C T f g"
           using R that by blast
         obtain U where "C \<subseteq> U" and opeU: "openin (top_of_set S) U"
-                  and hom: "homotopic_with (\<lambda>x. True) U T f g"
+                  and hom: "homotopic_with_canon (\<lambda>x. True) U T f g"
           using homotopic_neighbourhood_extension [OF contf fim contg gim _ \<open>ANR T\<close> hom]
             \<open>C \<in> components S\<close> closedin_component by blast
         then obtain V where "open V" and V: "U = S \<inter> V"
@@ -4775,7 +4771,7 @@
         proof (intro exI conjI)
           show "closedin (top_of_set S) K"
             by (meson \<open>compact K\<close> \<open>compact S\<close> closedin_compact_eq opeK openin_imp_subset)
-          show "homotopic_with (\<lambda>x. True) K T f g"
+          show "homotopic_with_canon (\<lambda>x. True) K T f g"
             using V \<open>K \<subseteq> V\<close> hom homotopic_with_subset_left opeK openin_imp_subset by fastforce
         qed (use opeK \<open>C \<subseteq> K\<close> in auto)
       qed
@@ -4783,7 +4779,7 @@
     then obtain \<phi> where \<phi>: "\<And>C. C \<in> components S \<Longrightarrow> C \<subseteq> \<phi> C"
                   and clo\<phi>: "\<And>C. C \<in> components S \<Longrightarrow> closedin (top_of_set S) (\<phi> C)"
                   and ope\<phi>: "\<And>C. C \<in> components S \<Longrightarrow> openin (top_of_set S) (\<phi> C)"
-                  and hom\<phi>: "\<And>C. C \<in> components S \<Longrightarrow> homotopic_with (\<lambda>x. True) (\<phi> C) T f g"
+                  and hom\<phi>: "\<And>C. C \<in> components S \<Longrightarrow> homotopic_with_canon (\<lambda>x. True) (\<phi> C) T f g"
       by metis
     have Seq: "S = \<Union> (\<phi> ` components S)"
     proof
@@ -4806,11 +4802,11 @@
   assumes S: "locally connected S \<or> compact S" and "ANR T"
   shows
    "(\<forall>f g. continuous_on S f \<longrightarrow> f ` S \<subseteq> T \<longrightarrow> continuous_on S g \<longrightarrow> g ` S \<subseteq> T \<longrightarrow>
-           homotopic_with (\<lambda>x. True) S T f g)
+           homotopic_with_canon (\<lambda>x. True) S T f g)
     \<longleftrightarrow>
     (\<forall>C\<in>components S.
         \<forall>f g. continuous_on C f \<longrightarrow> f ` C \<subseteq> T \<longrightarrow> continuous_on C g \<longrightarrow> g ` C \<subseteq> T \<longrightarrow>
-              homotopic_with (\<lambda>x. True) C T f g)"
+              homotopic_with_canon (\<lambda>x. True) C T f g)"
      (is "?lhs = ?rhs")
 proof
   assume L[rule_format]: ?lhs
@@ -4823,9 +4819,9 @@
       using extension_from_component [OF S \<open>ANR T\<close> C contf fim] by metis
     obtain g' where contg': "continuous_on S g'" and g'im: "g' ` S \<subseteq> T" and g'g: "\<And>x. x \<in> C \<Longrightarrow> g' x = g x"
       using extension_from_component [OF S \<open>ANR T\<close> C contg gim] by metis
-    have "homotopic_with (\<lambda>x. True) C T f' g'"
+    have "homotopic_with_canon (\<lambda>x. True) C T f' g'"
       using L [OF contf' f'im contg' g'im] homotopic_with_subset_left C in_components_subset by fastforce
-    then show "homotopic_with (\<lambda>x. True) C T f g"
+    then show "homotopic_with_canon (\<lambda>x. True) C T f g"
       using f'f g'g homotopic_with_eq by force
   qed
 next
@@ -4835,10 +4831,10 @@
     fix f g
     assume contf: "continuous_on S f" and fim: "f ` S \<subseteq> T"
       and contg: "continuous_on S g" and gim: "g ` S \<subseteq> T"
-    moreover have "homotopic_with (\<lambda>x. True) C T f g" if "C \<in> components S" for C
+    moreover have "homotopic_with_canon (\<lambda>x. True) C T f g" if "C \<in> components S" for C
       using R [OF that]
       by (meson contf contg continuous_on_subset fim gim image_mono in_components_subset order.trans that)
-    ultimately show "homotopic_with (\<lambda>x. True) S T f g"
+    ultimately show "homotopic_with_canon (\<lambda>x. True) S T f g"
       by (subst homotopic_on_components_eq [OF S \<open>ANR T\<close>]) auto
   qed
 qed
diff -r 8e916ed23d17 -r e7648f104d6b src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Tue Mar 26 16:27:29 2019 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Tue Mar 26 17:01:55 2019 +0000
@@ -4036,11 +4036,11 @@
 subsection\<open>Formulation of loop homotopy in terms of maps out of type complex\<close>
 
 lemma homotopic_circlemaps_imp_homotopic_loops:
-  assumes "homotopic_with (\<lambda>h. True) (sphere 0 1) S f g"
+  assumes "homotopic_with_canon (\<lambda>h. True) (sphere 0 1) S f g"
    shows "homotopic_loops S (f \<circ> exp \<circ> (\<lambda>t. 2 * of_real pi * of_real t * \<i>))
                             (g \<circ> exp \<circ> (\<lambda>t. 2 * of_real pi * of_real t * \<i>))"
 proof -
-  have "homotopic_with (\<lambda>f. True) {z. cmod z = 1} S f g"
+  have "homotopic_with_canon (\<lambda>f. True) {z. cmod z = 1} S f g"
     using assms by (auto simp: sphere_def)
   moreover have "continuous_on {0..1} (exp \<circ> (\<lambda>t. 2 * of_real pi * of_real t * \<i>))"
      by (intro continuous_intros)
@@ -4056,7 +4056,7 @@
 
 lemma homotopic_loops_imp_homotopic_circlemaps:
   assumes "homotopic_loops S p q"
-    shows "homotopic_with (\<lambda>h. True) (sphere 0 1) S
+    shows "homotopic_with_canon (\<lambda>h. True) (sphere 0 1) S
                           (p \<circ> (\<lambda>z. (Arg2pi z / (2 * pi))))
                           (q \<circ> (\<lambda>z. (Arg2pi z / (2 * pi))))"
 proof -
@@ -4117,7 +4117,7 @@
   assumes S: "simply_connected S"
       and contf: "continuous_on (sphere 0 1) f" and fim: "f ` (sphere 0 1) \<subseteq> S"
       and contg: "continuous_on (sphere 0 1) g" and gim: "g ` (sphere 0 1) \<subseteq> S"
-    shows "homotopic_with (\<lambda>h. True) (sphere 0 1) S f g"
+    shows "homotopic_with_canon (\<lambda>h. True) (sphere 0 1) S f g"
 proof -
   have "homotopic_loops S (f \<circ> exp \<circ> (\<lambda>t. of_real(2 * pi * t) * \<i>)) (g \<circ> exp \<circ> (\<lambda>t. of_real(2 * pi *  t) * \<i>))"
     apply (rule S [unfolded simply_connected_homotopic_loops, rule_format])
@@ -4135,8 +4135,8 @@
       and hom: "\<And>f g::complex \<Rightarrow> 'a.
                 \<lbrakk>continuous_on (sphere 0 1) f; f ` (sphere 0 1) \<subseteq> S;
                 continuous_on (sphere 0 1) g; g ` (sphere 0 1) \<subseteq> S\<rbrakk>
-                \<Longrightarrow> homotopic_with (\<lambda>h. True) (sphere 0 1) S f g"
-            shows "\<exists>a. homotopic_with (\<lambda>h. True) (sphere 0 1) S h (\<lambda>x. a)"
+                \<Longrightarrow> homotopic_with_canon (\<lambda>h. True) (sphere 0 1) S f g"
+            shows "\<exists>a. homotopic_with_canon (\<lambda>h. True) (sphere 0 1) S h (\<lambda>x. a)"
     apply (rule_tac x="h 1" in exI)
     apply (rule hom)
     using assms
@@ -4147,7 +4147,7 @@
   assumes "\<And>f g::complex \<Rightarrow> 'a.
                 \<lbrakk>continuous_on (sphere 0 1) f; f ` (sphere 0 1) \<subseteq> S;
                 continuous_on (sphere 0 1) g; g ` (sphere 0 1) \<subseteq> S\<rbrakk>
-                \<Longrightarrow> homotopic_with (\<lambda>h. True) (sphere 0 1) S f g"
+                \<Longrightarrow> homotopic_with_canon (\<lambda>h. True) (sphere 0 1) S f g"
   shows "path_connected S"
 proof (clarsimp simp add: path_connected_eq_homotopic_points)
   fix a b
@@ -4162,14 +4162,14 @@
   assumes "path_connected S"
       and hom: "\<And>f::complex \<Rightarrow> 'a.
                   \<lbrakk>continuous_on (sphere 0 1) f; f `(sphere 0 1) \<subseteq> S\<rbrakk>
-                  \<Longrightarrow> \<exists>a. homotopic_with (\<lambda>h. True) (sphere 0 1) S f (\<lambda>x. a)"
+                  \<Longrightarrow> \<exists>a. homotopic_with_canon (\<lambda>h. True) (sphere 0 1) S f (\<lambda>x. a)"
     shows "simply_connected S"
 proof (clarsimp simp add: simply_connected_eq_contractible_loop_some assms)
   fix p
   assume p: "path p" "path_image p \<subseteq> S" "pathfinish p = pathstart p"
   then have "homotopic_loops S p p"
     by (simp add: homotopic_loops_refl)
-  then obtain a where homp: "homotopic_with (\<lambda>h. True) (sphere 0 1) S (p \<circ> (\<lambda>z. Arg2pi z / (2 * pi))) (\<lambda>x. a)"
+  then obtain a where homp: "homotopic_with_canon (\<lambda>h. True) (sphere 0 1) S (p \<circ> (\<lambda>z. Arg2pi z / (2 * pi))) (\<lambda>x. a)"
     by (metis homotopic_with_imp_subset2 homotopic_loops_imp_homotopic_circlemaps homotopic_with_imp_continuous hom)
   show "\<exists>a. a \<in> S \<and> homotopic_loops S p (linepath a a)"
   proof (intro exI conjI)
@@ -4198,7 +4198,7 @@
          (\<forall>f g::complex \<Rightarrow> 'a.
               continuous_on (sphere 0 1) f \<and> f ` (sphere 0 1) \<subseteq> S \<and>
               continuous_on (sphere 0 1) g \<and> g ` (sphere 0 1) \<subseteq> S
-              \<longrightarrow> homotopic_with (\<lambda>h. True) (sphere 0 1) S f g)"
+              \<longrightarrow> homotopic_with_canon (\<lambda>h. True) (sphere 0 1) S f g)"
   apply (rule iffI)
    apply (blast elim: dest: simply_connected_eq_homotopic_circlemaps1)
   by (simp add: simply_connected_eq_homotopic_circlemaps2a simply_connected_eq_homotopic_circlemaps2b simply_connected_eq_homotopic_circlemaps3)
@@ -4209,7 +4209,7 @@
          path_connected S \<and>
          (\<forall>f::complex \<Rightarrow> 'a.
               continuous_on (sphere 0 1) f \<and> f `(sphere 0 1) \<subseteq> S
-              \<longrightarrow> (\<exists>a. homotopic_with (\<lambda>h. True) (sphere 0 1) S f (\<lambda>x. a)))"
+              \<longrightarrow> (\<exists>a. homotopic_with_canon (\<lambda>h. True) (sphere 0 1) S f (\<lambda>x. a)))"
   apply (rule iffI)
    apply (simp add: simply_connected_eq_homotopic_circlemaps1 simply_connected_eq_homotopic_circlemaps2a simply_connected_eq_homotopic_circlemaps2b)
   using simply_connected_eq_homotopic_circlemaps3 by blast
@@ -4229,7 +4229,7 @@
 proof -
   have "homotopic_loops (path_image \<gamma>) \<gamma> \<gamma>"
     by (simp add: assms homotopic_loops_refl simple_path_imp_path)
-  then have hom: "homotopic_with (\<lambda>h. True) (sphere 0 1) (path_image \<gamma>)
+  then have hom: "homotopic_with_canon (\<lambda>h. True) (sphere 0 1) (path_image \<gamma>)
                (\<gamma> \<circ> (\<lambda>z. Arg2pi z / (2*pi))) (\<gamma> \<circ> (\<lambda>z. Arg2pi z / (2*pi)))"
     by (rule homotopic_loops_imp_homotopic_circlemaps)
   have "\<exists>g. homeomorphism (sphere 0 1) (path_image \<gamma>) (\<gamma> \<circ> (\<lambda>z. Arg2pi z / (2*pi))) g"
diff -r 8e916ed23d17 -r e7648f104d6b src/HOL/Analysis/Further_Topology.thy
--- a/src/HOL/Analysis/Further_Topology.thy	Tue Mar 26 16:27:29 2019 +0100
+++ b/src/HOL/Analysis/Further_Topology.thy	Tue Mar 26 17:01:55 2019 +0000
@@ -164,7 +164,7 @@
       and "S \<subseteq> T"
       and contf: "continuous_on (sphere 0 1 \<inter> S) f"
       and fim: "f ` (sphere 0 1 \<inter> S) \<subseteq> sphere 0 1 \<inter> T"
-    shows "\<exists>c. homotopic_with (\<lambda>x. True) (sphere 0 1 \<inter> S) (sphere 0 1 \<inter> T) f (\<lambda>x. c)"
+    shows "\<exists>c. homotopic_with_canon (\<lambda>x. True) (sphere 0 1 \<inter> S) (sphere 0 1 \<inter> T) f (\<lambda>x. c)"
 proof -
   have [simp]: "\<And>x. \<lbrakk>norm x = 1; x \<in> S\<rbrakk> \<Longrightarrow> norm (f x) = 1"
     using fim by (simp add: image_subset_iff)
@@ -194,7 +194,7 @@
     apply (intro derivative_intros diffg differentiable_on_compose [OF diffg])
     using gnz apply auto
     done
-  have homfg: "homotopic_with (\<lambda>z. True) (sphere 0 1 \<inter> S) (T - {0}) f g"
+  have homfg: "homotopic_with_canon (\<lambda>z. True) (sphere 0 1 \<inter> S) (T - {0}) f g"
   proof (rule homotopic_with_linear [OF contf])
     show "continuous_on (sphere 0 1 \<inter> S) g"
       using pfg by (simp add: differentiable_imp_continuous_on diffg)
@@ -224,7 +224,7 @@
     by (auto simp: between_mem_segment midpoint_def)
   have conth: "continuous_on (sphere 0 1 \<inter> S) h"
     using differentiable_imp_continuous_on diffh by blast
-  have hom_hd: "homotopic_with (\<lambda>z. True) (sphere 0 1 \<inter> S) (T - {0}) h (\<lambda>x. -d)"
+  have hom_hd: "homotopic_with_canon (\<lambda>z. True) (sphere 0 1 \<inter> S) (T - {0}) h (\<lambda>x. -d)"
     apply (rule homotopic_with_linear [OF conth continuous_on_const])
     apply (simp add: subset_Diff_insert non0hd)
     apply (simp add: segment_convex_hull)
@@ -236,7 +236,7 @@
     by (intro continuous_intros) auto
   have sub0T: "(\<lambda>y. y /\<^sub>R norm y) ` (T - {0}) \<subseteq> sphere 0 1 \<inter> T"
     by (fastforce simp: assms(2) subspace_mul)
-  obtain c where homhc: "homotopic_with (\<lambda>z. True) (sphere 0 1 \<inter> S) (sphere 0 1 \<inter> T) h (\<lambda>x. c)"
+  obtain c where homhc: "homotopic_with_canon (\<lambda>z. True) (sphere 0 1 \<inter> S) (sphere 0 1 \<inter> T) h (\<lambda>x. c)"
     apply (rule_tac c="-d" in that)
     apply (rule homotopic_with_eq)
        apply (rule homotopic_compose_continuous_left [OF hom_hd conT0 sub0T])
@@ -306,7 +306,7 @@
       and affST: "aff_dim S < aff_dim T"
       and contf: "continuous_on (rel_frontier S) f"
       and fim: "f ` (rel_frontier S) \<subseteq> rel_frontier T"
-  obtains c where "homotopic_with (\<lambda>z. True) (rel_frontier S) (rel_frontier T) f (\<lambda>x. c)"
+  obtains c where "homotopic_with_canon (\<lambda>z. True) (rel_frontier S) (rel_frontier T) f (\<lambda>x. c)"
 proof (cases "S = {}")
   case True
   then show ?thesis
@@ -328,7 +328,7 @@
       using \<open>T \<noteq> {}\<close> by blast
     with homeomorphic_imp_homotopy_eqv
     have relT: "sphere 0 1 \<inter> T'  homotopy_eqv rel_frontier T"
-      using homotopy_eqv_sym by blast
+      using homotopy_equivalent_space_sym by blast
     have "aff_dim S \<le> int (dim T')"
       using affT' \<open>subspace T'\<close> affST aff_dim_subspace by force
     with spheremap_lemma3 [OF \<open>bounded S\<close> \<open>convex S\<close> \<open>subspace T'\<close>] \<open>S \<noteq> {}\<close>
@@ -338,10 +338,10 @@
         by metis
     with homeomorphic_imp_homotopy_eqv
     have relS: "sphere 0 1 \<inter> S'  homotopy_eqv rel_frontier S"
-      using homotopy_eqv_sym by blast
+      using homotopy_equivalent_space_sym by blast
     have dimST': "dim S' < dim T'"
       by (metis \<open>S' \<subseteq> T'\<close> \<open>subspace S'\<close> \<open>subspace T'\<close> affS' affST affT' less_irrefl not_le subspace_dim_equal)
-    have "\<exists>c. homotopic_with (\<lambda>z. True) (rel_frontier S) (rel_frontier T) f (\<lambda>x. c)"
+    have "\<exists>c. homotopic_with_canon (\<lambda>z. True) (rel_frontier S) (rel_frontier T) f (\<lambda>x. c)"
       apply (rule homotopy_eqv_homotopic_triviality_null_imp [OF relT contf fim])
       apply (rule homotopy_eqv_cohomotopic_triviality_null[OF relS, THEN iffD1, rule_format])
        apply (metis dimST' \<open>subspace S'\<close>  \<open>subspace T'\<close>  \<open>S' \<subseteq> T'\<close> spheremap_lemma2, blast)
@@ -354,7 +354,7 @@
   fixes f :: "'M::euclidean_space \<Rightarrow> 'a::euclidean_space"
   assumes
    "DIM('M) < DIM('a)" and f: "continuous_on (sphere a r) f" "f ` (sphere a r) \<subseteq> (sphere b s)"
-   obtains c where "homotopic_with (\<lambda>z. True) (sphere a r) (sphere b s) f (\<lambda>x. c)"
+   obtains c where "homotopic_with_canon (\<lambda>z. True) (sphere a r) (sphere b s) f (\<lambda>x. c)"
 proof (cases "s \<le> 0")
   case True then show ?thesis
     by (meson nullhomotopic_into_contractible f contractible_sphere that)
@@ -522,13 +522,13 @@
           using Suc.prems affD by linarith
         have contDh: "continuous_on (rel_frontier D) h"
           using \<open>C \<in> \<F>\<close> relf_sub by (blast intro: continuous_on_subset [OF conth])
-        then have *: "(\<exists>c. homotopic_with (\<lambda>x. True) (rel_frontier D) (rel_frontier T) h (\<lambda>x. c)) =
+        then have *: "(\<exists>c. homotopic_with_canon (\<lambda>x. True) (rel_frontier D) (rel_frontier T) h (\<lambda>x. c)) =
                       (\<exists>g. continuous_on UNIV g \<and>  range g \<subseteq> rel_frontier T \<and>
                            (\<forall>x\<in>rel_frontier D. g x = h x))"
           apply (rule nullhomotopic_into_rel_frontier_extension [OF closed_rel_frontier])
           apply (simp_all add: assms rel_frontier_eq_empty him_relf)
           done
-        have "(\<exists>c. homotopic_with (\<lambda>x. True) (rel_frontier D)
+        have "(\<exists>c. homotopic_with_canon (\<lambda>x. True) (rel_frontier D)
               (rel_frontier T) h (\<lambda>x. c))"
           by (metis inessential_spheremap_lowdim_gen
                  [OF \<open>convex D\<close> \<open>bounded D\<close> \<open>convex T\<close> \<open>bounded T\<close> affD_lessT contDh him_relf])
@@ -1706,7 +1706,7 @@
   assumes "compact S"
     shows "(\<forall>c \<in> components(- S). \<not>bounded c) \<longleftrightarrow>
            (\<forall>f. continuous_on S f \<and> f ` S \<subseteq> sphere (0::'a) 1
-                \<longrightarrow> (\<exists>c. homotopic_with (\<lambda>x. True) S (sphere 0 1) f (\<lambda>x. c)))"
+                \<longrightarrow> (\<exists>c. homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) f (\<lambda>x. c)))"
        (is "?lhs = ?rhs")
 proof
   assume L [rule_format]: ?lhs
@@ -1717,9 +1717,10 @@
     obtain g where contg: "continuous_on UNIV g" and gim: "range g \<subseteq> sphere 0 1"
                and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
       by (rule extend_map_UNIV_to_sphere_no_bounded_component [OF _ _ \<open>compact S\<close> contf fim L]) auto
-    then show "\<exists>c. homotopic_with (\<lambda>x. True) S (sphere 0 1) f (\<lambda>x. c)"
-      using nullhomotopic_from_contractible [OF contg gim]
-      by (metis assms compact_imp_closed contf empty_iff fim homotopic_with_equal nullhomotopic_into_sphere_extension)
+    then obtain c where c: "homotopic_with_canon (\<lambda>h. True) UNIV (sphere 0 1) g (\<lambda>x. c)"
+      using contractible_UNIV nullhomotopic_from_contractible by blast
+    then show "\<exists>c. homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) f (\<lambda>x. c)"
+      by (metis assms compact_imp_closed contf contg contractible_empty fim gf gim nullhomotopic_from_contractible nullhomotopic_into_sphere_extension)
   qed
 next
   assume R [rule_format]: ?rhs
@@ -1744,7 +1745,7 @@
   assumes "compact S" and 2: "2 \<le> DIM('a)"
     shows "connected(- S) \<longleftrightarrow>
            (\<forall>f. continuous_on S f \<and> f ` S \<subseteq> sphere (0::'a) 1
-                \<longrightarrow> (\<exists>c. homotopic_with (\<lambda>x. True) S (sphere 0 1) f (\<lambda>x. c)))"
+                \<longrightarrow> (\<exists>c. homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) f (\<lambda>x. c)))"
        (is "?lhs = ?rhs")
 proof
   assume L: ?lhs
@@ -2814,12 +2815,12 @@
       by simp
     have "convex (cball (0::complex) 1)"
       by (rule convex_cball)
-    then obtain c where "homotopic_with (\<lambda>z. True) (sphere (0::complex) 1) (rel_frontier S) f (\<lambda>x. c)"
+    then obtain c where "homotopic_with_canon (\<lambda>z. True) (sphere (0::complex) 1) (rel_frontier S) f (\<lambda>x. c)"
       apply (rule inessential_spheremap_lowdim_gen [OF _ bounded_cball \<open>convex S\<close> \<open>bounded S\<close>, where f=f])
       using f 3
          apply (auto simp: aff_dim_cball)
       done
-    then show "\<exists>a. homotopic_with (\<lambda>h. True) (sphere 0 1) (rel_frontier S) f (\<lambda>x. a)"
+    then show "\<exists>a. homotopic_with_canon (\<lambda>h. True) (sphere 0 1) (rel_frontier S) f (\<lambda>x. a)"
       by blast
   qed
 qed
@@ -3018,7 +3019,7 @@
         by (metis DIM_complex False homeomorphic_spheres_gen not_less zero_less_one)
       then have "simply_connected(sphere (0::complex) 1)"
         using L homeomorphic_simply_connected_eq by blast
-      then obtain a::complex where "homotopic_with (\<lambda>h. True) (sphere 0 1) (sphere 0 1) id (\<lambda>x. a)"
+      then obtain a::complex where "homotopic_with_canon (\<lambda>h. True) (sphere 0 1) (sphere 0 1) id (\<lambda>x. a)"
         apply (simp add: simply_connected_eq_contractible_circlemap)
         by (metis continuous_on_id' id_apply image_id subset_refl)
       then show False
@@ -3496,7 +3497,7 @@
 
 lemma inessential_eq_continuous_logarithm:
   fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
-  shows "(\<exists>a. homotopic_with (\<lambda>h. True) S (-{0}) f (\<lambda>t. a)) \<longleftrightarrow>
+  shows "(\<exists>a. homotopic_with_canon (\<lambda>h. True) S (-{0}) f (\<lambda>t. a)) \<longleftrightarrow>
          (\<exists>g. continuous_on S g \<and> (\<forall>x \<in> S. f x = exp(g x)))"
   (is "?lhs \<longleftrightarrow> ?rhs")
 proof
@@ -3506,24 +3507,24 @@
   assume ?rhs
   then obtain g where contg: "continuous_on S g" and f: "\<And>x. x \<in> S \<Longrightarrow> f x = exp(g x)"
     by metis
-  obtain a where "homotopic_with (\<lambda>h. True) S (- {of_real 0}) (exp \<circ> g) (\<lambda>x. a)"
+  obtain a where "homotopic_with_canon (\<lambda>h. True) S (- {of_real 0}) (exp \<circ> g) (\<lambda>x. a)"
   proof (rule nullhomotopic_through_contractible [OF contg subset_UNIV _ _ contractible_UNIV])
     show "continuous_on (UNIV::complex set) exp"
       by (intro continuous_intros)
     show "range exp \<subseteq> - {0}"
       by auto
   qed force
-  thus ?lhs
-    apply (rule_tac x=a in exI)
-    by (simp add: f homotopic_with_eq)
+  then have "homotopic_with_canon (\<lambda>h. True) S (- {0}) f (\<lambda>t. a)"
+    using f homotopic_with_eq by fastforce
+  then show ?lhs ..
 qed
 
 corollary inessential_imp_continuous_logarithm_circle:
   fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
-  assumes "homotopic_with (\<lambda>h. True) S (sphere 0 1) f (\<lambda>t. a)"
+  assumes "homotopic_with_canon (\<lambda>h. True) S (sphere 0 1) f (\<lambda>t. a)"
   obtains g where "continuous_on S g" and "\<And>x. x \<in> S \<Longrightarrow> f x = exp(g x)"
 proof -
-  have "homotopic_with (\<lambda>h. True) S (- {0}) f (\<lambda>t. a)"
+  have "homotopic_with_canon (\<lambda>h. True) S (- {0}) f (\<lambda>t. a)"
     using assms homotopic_with_subset_right by fastforce
   then show ?thesis
     by (metis inessential_eq_continuous_logarithm that)
@@ -3532,7 +3533,7 @@
 
 lemma inessential_eq_continuous_logarithm_circle:
   fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
-  shows "(\<exists>a. homotopic_with (\<lambda>h. True) S (sphere 0 1) f (\<lambda>t. a)) \<longleftrightarrow>
+  shows "(\<exists>a. homotopic_with_canon (\<lambda>h. True) S (sphere 0 1) f (\<lambda>t. a)) \<longleftrightarrow>
          (\<exists>g. continuous_on S g \<and> (\<forall>x \<in> S. f x = exp(\<i> * of_real(g x))))"
   (is "?lhs \<longleftrightarrow> ?rhs")
 proof
@@ -3552,7 +3553,7 @@
   assume ?rhs
   then obtain g where contg: "continuous_on S g" and g: "\<And>x. x \<in> S \<Longrightarrow> f x = exp(\<i>* of_real(g x))"
     by metis
-  obtain a where "homotopic_with (\<lambda>h. True) S (sphere 0 1) ((exp \<circ> (\<lambda>z. \<i>*z)) \<circ> (of_real \<circ> g)) (\<lambda>x. a)"
+  obtain a where "homotopic_with_canon (\<lambda>h. True) S (sphere 0 1) ((exp \<circ> (\<lambda>z. \<i>*z)) \<circ> (of_real \<circ> g)) (\<lambda>x. a)"
   proof (rule nullhomotopic_through_contractible)
     show "continuous_on S (complex_of_real \<circ> g)"
       by (intro conjI contg continuous_intros)
@@ -3565,16 +3566,16 @@
   qed (auto simp: convex_Reals convex_imp_contractible)
   moreover have "\<And>x. x \<in> S \<Longrightarrow> (exp \<circ> (*)\<i> \<circ> (complex_of_real \<circ> g)) x = f x"
     by (simp add: g)
-  ultimately show ?lhs
-    apply (rule_tac x=a in exI)
-    by (simp add: homotopic_with_eq)
+  ultimately have "homotopic_with_canon (\<lambda>h. True) S (sphere 0 1) f (\<lambda>t. a)"
+    using homotopic_with_eq by force
+  then show ?lhs ..
 qed
 
 proposition homotopic_with_sphere_times:
   fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
-  assumes hom: "homotopic_with (\<lambda>x. True) S (sphere 0 1) f g" and conth: "continuous_on S h"
+  assumes hom: "homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) f g" and conth: "continuous_on S h"
       and hin: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> sphere 0 1"
-    shows "homotopic_with (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x * h x) (\<lambda>x. g x * h x)"
+    shows "homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x * h x) (\<lambda>x. g x * h x)"
 proof -
   obtain k where contk: "continuous_on ({0..1::real} \<times> S) k"
              and kim: "k ` ({0..1} \<times> S) \<subseteq> sphere 0 1"
@@ -3592,29 +3593,29 @@
 
 proposition homotopic_circlemaps_divide:
   fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
-    shows "homotopic_with (\<lambda>x. True) S (sphere 0 1) f g \<longleftrightarrow>
+    shows "homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) f g \<longleftrightarrow>
            continuous_on S f \<and> f ` S \<subseteq> sphere 0 1 \<and>
            continuous_on S g \<and> g ` S \<subseteq> sphere 0 1 \<and>
-           (\<exists>c. homotopic_with (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. c))"
+           (\<exists>c. homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. c))"
 proof -
-  have "homotopic_with (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. 1)"
-       if "homotopic_with (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. c)" for c
+  have "homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. 1)"
+       if "homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. c)" for c
   proof -
     have "S = {} \<or> path_component (sphere 0 1) 1 c"
       using homotopic_with_imp_subset2 [OF that] path_connected_sphere [of "0::complex" 1]
       by (auto simp: path_connected_component)
-    then have "homotopic_with (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. 1) (\<lambda>x. c)"
-      by (metis homotopic_constant_maps)
+    then have "homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. 1) (\<lambda>x. c)"
+      by (simp add: homotopic_constant_maps)
     then show ?thesis
       using homotopic_with_symD homotopic_with_trans that by blast
   qed
-  then have *: "(\<exists>c. homotopic_with (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. c)) \<longleftrightarrow>
-                homotopic_with (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. 1)"
+  then have *: "(\<exists>c. homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. c)) \<longleftrightarrow>
+                homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. 1)"
     by auto
-  have "homotopic_with (\<lambda>x. True) S (sphere 0 1) f g \<longleftrightarrow>
+  have "homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) f g \<longleftrightarrow>
            continuous_on S f \<and> f ` S \<subseteq> sphere 0 1 \<and>
            continuous_on S g \<and> g ` S \<subseteq> sphere 0 1 \<and>
-           homotopic_with (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. 1)"
+           homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. 1)"
         (is "?lhs \<longleftrightarrow> ?rhs")
   proof
     assume L: ?lhs
@@ -3627,7 +3628,7 @@
       apply (rule continuous_on_subset [of "sphere 0 1", OF continuous_on_inverse])
         apply (auto simp: continuous_on_id)
       done
-    have "homotopic_with (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. 1)"
+    have "homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. 1)"
       using homotopic_with_sphere_times [OF L cont]
       apply (rule homotopic_with_eq)
          apply (auto simp: division_ring_class.divide_inverse norm_inverse)
@@ -3852,7 +3853,7 @@
   assumes "continuous_on S f" "contractible S" "\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0"
   obtains g where "continuous_on S g" "\<And>x. x \<in> S \<Longrightarrow> f x = exp(g x)"
 proof -
-  obtain c where hom: "homotopic_with (\<lambda>h. True) S (-{0}) f (\<lambda>x. c)"
+  obtain c where hom: "homotopic_with_canon (\<lambda>h. True) S (-{0}) f (\<lambda>x. c)"
     using nullhomotopic_from_contractible assms
     by (metis imageE subset_Compl_singleton)
   then show ?thesis
@@ -3920,7 +3921,7 @@
   fixes f :: "'a::euclidean_space \<Rightarrow> complex"
   assumes 2: "2 < DIM('a)" and contf: "continuous_on (sphere a r) f" 
       and fim: "f `(sphere a r) \<subseteq> (sphere 0 1)" 
-  obtains c where "homotopic_with (\<lambda>z. True) (sphere a r) (sphere 0 1) f (\<lambda>x. c)"
+  obtains c where "homotopic_with_canon (\<lambda>z. True) (sphere a r) (sphere 0 1) f (\<lambda>x. c)"
 proof -
   obtain g where contg: "continuous_on (sphere a r) g" 
              and feq: "\<And>x. x \<in> sphere a r \<Longrightarrow> f x = exp(g x)"
@@ -3947,7 +3948,7 @@
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes a2: "2 < DIM('a)" and b2: "DIM('b) = 2" 
       and contf: "continuous_on (sphere a r) f" and fim: "f `(sphere a r) \<subseteq> (sphere b s)"
-  obtains c where "homotopic_with (\<lambda>z. True) (sphere a r) (sphere b s) f (\<lambda>x. c)"
+  obtains c where "homotopic_with_canon (\<lambda>z. True) (sphere a r) (sphere b s) f (\<lambda>x. c)"
 proof (cases "s \<le> 0")
   case True
   then show ?thesis
@@ -3963,16 +3964,16 @@
        and  him: "h ` sphere b s \<subseteq> sphere 0 1"
        and  kim: "k ` sphere 0 1 \<subseteq> sphere b s"
     by (simp_all add: homeomorphism_def)
-  obtain c where "homotopic_with (\<lambda>z. True) (sphere a r) (sphere 0 1) (h \<circ> f) (\<lambda>x. c)"
+  obtain c where "homotopic_with_canon (\<lambda>z. True) (sphere a r) (sphere 0 1) (h \<circ> f) (\<lambda>x. c)"
   proof (rule inessential_spheremap_2_aux [OF a2])
     show "continuous_on (sphere a r) (h \<circ> f)"
       by (meson continuous_on_compose [OF contf] conth continuous_on_subset fim)
     show "(h \<circ> f) ` sphere a r \<subseteq> sphere 0 1"
       using fim him by force
   qed auto
-  then have "homotopic_with (\<lambda>f. True) (sphere a r) (sphere b s) (k \<circ> (h \<circ> f)) (k \<circ> (\<lambda>x. c))"
+  then have "homotopic_with_canon (\<lambda>f. True) (sphere a r) (sphere b s) (k \<circ> (h \<circ> f)) (k \<circ> (\<lambda>x. c))"
     by (rule homotopic_compose_continuous_left [OF _ contk kim])
-  then have "homotopic_with (\<lambda>z. True) (sphere a r) (sphere b s) f (\<lambda>x. k c)"
+  then have "homotopic_with_canon (\<lambda>z. True) (sphere a r) (sphere b s) f (\<lambda>x. k c)"
     apply (rule homotopic_with_eq, auto)
     by (metis fim hk homeomorphism_def image_subset_iff mem_sphere)
   then show ?thesis
@@ -4202,7 +4203,7 @@
 definition%important Borsukian where
     "Borsukian S \<equiv>
         \<forall>f. continuous_on S f \<and> f ` S \<subseteq> (- {0::complex})
-            \<longrightarrow> (\<exists>a. homotopic_with (\<lambda>h. True) S (- {0}) f (\<lambda>x. a))"
+            \<longrightarrow> (\<exists>a. homotopic_with_canon (\<lambda>h. True) S (- {0}) f (\<lambda>x. a))"
 
 lemma Borsukian_retraction_gen:
   assumes "Borsukian S" "continuous_on S h" "h ` S = T"
@@ -4259,7 +4260,7 @@
    "Borsukian S \<longleftrightarrow>
         (\<forall>f g. continuous_on S f \<and> f ` S \<subseteq> -{0} \<and>
                continuous_on S g \<and> g ` S \<subseteq> -{0}
-               \<longrightarrow> homotopic_with (\<lambda>h. True) S (- {0::complex}) f g)"
+               \<longrightarrow> homotopic_with_canon (\<lambda>h. True) S (- {0::complex}) f g)"
   unfolding Borsukian_def homotopic_triviality
   by (simp add: path_connected_punctured_universe)
 
@@ -4343,7 +4344,7 @@
   fixes S :: "'a::real_normed_vector set"
   shows "Borsukian S \<longleftrightarrow>
          (\<forall>f. continuous_on S f \<and> f ` S \<subseteq> sphere (0::complex) 1
-              \<longrightarrow> (\<exists>a. homotopic_with (\<lambda>h. True) S (sphere (0::complex) 1) f (\<lambda>x. a)))"
+              \<longrightarrow> (\<exists>a. homotopic_with_canon (\<lambda>h. True) S (sphere (0::complex) 1) f (\<lambda>x. a)))"
 by (simp add: inessential_eq_continuous_logarithm_circle Borsukian_continuous_logarithm_circle_real)
 
 lemma contractible_imp_Borsukian: "contractible S \<Longrightarrow> Borsukian S"
@@ -5335,12 +5336,12 @@
 proposition inessential_eq_extensible:
   fixes f :: "'a::euclidean_space \<Rightarrow> complex"
   assumes "closed S"
-  shows "(\<exists>a. homotopic_with (\<lambda>h. True) S (-{0}) f (\<lambda>t. a)) \<longleftrightarrow>
+  shows "(\<exists>a. homotopic_with_canon (\<lambda>h. True) S (-{0}) f (\<lambda>t. a)) \<longleftrightarrow>
          (\<exists>g. continuous_on UNIV g \<and> (\<forall>x \<in> S. g x = f x) \<and> (\<forall>x. g x \<noteq> 0))"
      (is "?lhs = ?rhs")
 proof
   assume ?lhs
-  then obtain a where a: "homotopic_with (\<lambda>h. True) S (-{0}) f (\<lambda>t. a)" ..
+  then obtain a where a: "homotopic_with_canon (\<lambda>h. True) S (-{0}) f (\<lambda>t. a)" ..
   show ?rhs
   proof (cases "S = {}")
     case True
@@ -5403,8 +5404,8 @@
   assumes T: "path_connected T"
       and "\<And>S. S \<in> \<F> \<Longrightarrow> closedin (top_of_set (\<Union>\<F>)) S"
       and "\<And>S. S \<in> \<F> \<Longrightarrow> openin (top_of_set (\<Union>\<F>)) S"
-      and hom: "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>a. homotopic_with (\<lambda>x. True) S T f (\<lambda>x. a)"
-  obtains a where "homotopic_with (\<lambda>x. True) (\<Union>\<F>) T f (\<lambda>x. a)"
+      and hom: "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>a. homotopic_with_canon (\<lambda>x. True) S T f (\<lambda>x. a)"
+  obtains a where "homotopic_with_canon (\<lambda>x. True) (\<Union>\<F>) T f (\<lambda>x. a)"
 proof (cases "\<Union>\<F> = {}")
   case True
   with that show ?thesis
@@ -5415,16 +5416,16 @@
     by blast
   then obtain a where clo: "closedin (top_of_set (\<Union>\<F>)) C"
     and ope: "openin (top_of_set (\<Union>\<F>)) C"
-    and "homotopic_with (\<lambda>x. True) C T f (\<lambda>x. a)"
+    and "homotopic_with_canon (\<lambda>x. True) C T f (\<lambda>x. a)"
     using assms by blast
   with \<open>C \<noteq> {}\<close> have "f ` C \<subseteq> T" "a \<in> T"
     using homotopic_with_imp_subset1 homotopic_with_imp_subset2 by blast+
-  have "homotopic_with (\<lambda>x. True) (\<Union>\<F>) T f (\<lambda>x. a)"
+  have "homotopic_with_canon (\<lambda>x. True) (\<Union>\<F>) T f (\<lambda>x. a)"
   proof (rule homotopic_on_clopen_Union)
     show "\<And>S. S \<in> \<F> \<Longrightarrow> closedin (top_of_set (\<Union>\<F>)) S"
          "\<And>S. S \<in> \<F> \<Longrightarrow> openin (top_of_set (\<Union>\<F>)) S"
       by (simp_all add: assms)
-    show "homotopic_with (\<lambda>x. True) S T f (\<lambda>x. a)" if "S \<in> \<F>" for S
+    show "homotopic_with_canon (\<lambda>x. True) S T f (\<lambda>x. a)" if "S \<in> \<F>" for S
     proof (cases "S = {}")
       case True
       then show ?thesis
@@ -5433,12 +5434,13 @@
       case False
       then obtain b where "b \<in> S"
         by blast
-      obtain c where c: "homotopic_with (\<lambda>x. True) S T f (\<lambda>x. c)"
+      obtain c where c: "homotopic_with_canon (\<lambda>x. True) S T f (\<lambda>x. c)"
         using \<open>S \<in> \<F>\<close> hom by blast
       then have "c \<in> T"
         using \<open>b \<in> S\<close> homotopic_with_imp_subset2 by blast
-      then have "homotopic_with (\<lambda>x. True) S T (\<lambda>x. a) (\<lambda>x. c)"
-        using T \<open>a \<in> T\<close> homotopic_constant_maps path_connected_component by blast
+      then have "homotopic_with_canon (\<lambda>x. True) S T (\<lambda>x. a) (\<lambda>x. c)"
+        using T \<open>a \<in> T\<close> homotopic_constant_maps path_connected_component
+        by (simp add: homotopic_constant_maps path_connected_component)
       then show ?thesis
         using c homotopic_with_symD homotopic_with_trans by blast
     qed
diff -r 8e916ed23d17 -r e7648f104d6b src/HOL/Analysis/Homeomorphism.thy
--- a/src/HOL/Analysis/Homeomorphism.thy	Tue Mar 26 16:27:29 2019 +0100
+++ b/src/HOL/Analysis/Homeomorphism.thy	Tue Mar 26 17:01:55 2019 +0000
@@ -1861,7 +1861,7 @@
     show "topspace ?X \<subseteq> (\<Union>i\<in>U. {0..1} \<times> V i)"
       using V by force
     show "\<And>i. i \<in> U \<Longrightarrow> openin (top_of_set ({0..1} \<times> U)) ({0..1} \<times> V i)"
-      by (simp add: opeV openin_Times)
+      by (simp add: Abstract_Topology.openin_Times opeV)
     show "\<And>i. i \<in> U \<Longrightarrow> continuous_map
               (subtopology (top_of_set ({0..1} \<times> U)) ({0..1} \<times> V i)) euclidean (fs i)"
       using contfs
@@ -1949,7 +1949,7 @@
       and contg: "continuous_on U g"
       and gim: "g ` U \<subseteq> C"
       and pgeq: "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
-      and hom: "homotopic_with (\<lambda>x. True) U S f f'"
+      and hom: "homotopic_with_canon (\<lambda>x. True) U S f f'"
     obtains g' where "continuous_on U g'" "image g' U \<subseteq> C" "\<And>y. y \<in> U \<Longrightarrow> p(g' y) = f' y"
 proof -
   obtain h where conth: "continuous_on ({0..1::real} \<times> U) h"
@@ -1978,7 +1978,7 @@
 corollary covering_space_lift_inessential_function:
   fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" and U :: "'c::real_normed_vector set"
   assumes cov: "covering_space C p S"
-      and hom: "homotopic_with (\<lambda>x. True) U S f (\<lambda>x. a)"
+      and hom: "homotopic_with_canon (\<lambda>x. True) U S f (\<lambda>x. a)"
   obtains g where "continuous_on U g" "g ` U \<subseteq> C" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
 proof (cases "U = {}")
   case True
diff -r 8e916ed23d17 -r e7648f104d6b src/HOL/Analysis/Homotopy.thy
--- a/src/HOL/Analysis/Homotopy.thy	Tue Mar 26 16:27:29 2019 +0100
+++ b/src/HOL/Analysis/Homotopy.thy	Tue Mar 26 17:01:55 2019 +0000
@@ -5,172 +5,299 @@
 section \<open>Homotopy of Maps\<close>
 
 theory Homotopy
-  imports Path_Connected Continuum_Not_Denumerable
+  imports Path_Connected Continuum_Not_Denumerable Product_Topology
 begin
 
-definition%important homotopic_with ::
-  "[('a::topological_space \<Rightarrow> 'b::topological_space) \<Rightarrow> bool, 'a set, 'b set, 'a \<Rightarrow> 'b, 'a \<Rightarrow> 'b] \<Rightarrow> bool"
+definition%important homotopic_with
 where
- "homotopic_with P X Y p q \<equiv>
-   (\<exists>h:: real \<times> 'a \<Rightarrow> 'b.
-       continuous_on ({0..1} \<times> X) h \<and>
-       h ` ({0..1} \<times> X) \<subseteq> Y \<and>
-       (\<forall>x. h(0, x) = p x) \<and>
-       (\<forall>x. h(1, x) = q x) \<and>
-       (\<forall>t \<in> {0..1}. P(\<lambda>x. h(t, x))))"
+ "homotopic_with P X Y f g \<equiv>
+   (\<exists>h. continuous_map (prod_topology (subtopology euclideanreal {0..1}) X) Y h \<and>
+       (\<forall>x. h(0, x) = f x) \<and>
+       (\<forall>x. h(1, x) = g x) \<and>
+       (\<forall>t \<in> {0..1}. P(\<lambda>x. h(t,x))))"
 
 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.
 We often just want to require that \<open>P\<close> fixes some subset, but to include the case of a loop homotopy,
 it is convenient to have a general property \<open>P\<close>.\<close>
 
+abbreviation homotopic_with_canon ::
+  "[('a::topological_space \<Rightarrow> 'b::topological_space) \<Rightarrow> bool, 'a set, 'b set, 'a \<Rightarrow> 'b, 'a \<Rightarrow> 'b] \<Rightarrow> bool"
+where
+ "homotopic_with_canon P S T p q \<equiv> homotopic_with P (top_of_set S) (top_of_set T) p q"
+
+lemma split_01: "{0..1::real} = {0..1/2} \<union> {1/2..1}"
+  by force
+
+lemma split_01_prod: "{0..1::real} \<times> X = ({0..1/2} \<times> X) \<union> ({1/2..1} \<times> X)"
+  by force
+
+lemma image_Pair_const: "(\<lambda>x. (x, c)) ` A = A \<times> {c}"
+  by auto
+
+lemma fst_o_paired [simp]: "fst \<circ> (\<lambda>(x,y). (f x y, g x y)) = (\<lambda>(x,y). f x y)"
+  by auto
+
+lemma snd_o_paired [simp]: "snd \<circ> (\<lambda>(x,y). (f x y, g x y)) = (\<lambda>(x,y). g x y)"
+  by auto
+
+lemma continuous_on_o_Pair: "\<lbrakk>continuous_on (T \<times> X) h; t \<in> T\<rbrakk> \<Longrightarrow> continuous_on X (h \<circ> Pair t)"
+  by (fast intro: continuous_intros elim!: continuous_on_subset)
+
+lemma continuous_map_o_Pair: 
+  assumes h: "continuous_map (prod_topology X Y) Z h" and t: "t \<in> topspace X"
+  shows "continuous_map Y Z (h \<circ> Pair t)"
+  apply (intro continuous_map_compose [OF _ h] continuous_map_id [unfolded id_def] continuous_intros)
+  apply (simp add: t)
+  done
+
+subsection%unimportant\<open>Trivial properties\<close>
+
 text \<open>We often want to just localize the ending function equality or whatever.\<close>
 text%important \<open>%whitespace\<close>
 proposition homotopic_with:
-  fixes X :: "'a::topological_space set" and Y :: "'b::topological_space set"
-  assumes "\<And>h k. (\<And>x. x \<in> X \<Longrightarrow> h x = k x) \<Longrightarrow> (P h \<longleftrightarrow> P k)"
+  assumes "\<And>h k. (\<And>x. x \<in> topspace X \<Longrightarrow> h x = k x) \<Longrightarrow> (P h \<longleftrightarrow> P k)"
   shows "homotopic_with P X Y p q \<longleftrightarrow>
-           (\<exists>h :: real \<times> 'a \<Rightarrow> 'b.
-              continuous_on ({0..1} \<times> X) h \<and>
-              h ` ({0..1} \<times> X) \<subseteq> Y \<and>
-              (\<forall>x \<in> X. h(0,x) = p x) \<and>
-              (\<forall>x \<in> X. h(1,x) = q x) \<and>
+           (\<exists>h. continuous_map (prod_topology (subtopology euclideanreal {0..1}) X) Y h \<and>
+              (\<forall>x \<in> topspace X. h(0,x) = p x) \<and>
+              (\<forall>x \<in> topspace X. h(1,x) = q x) \<and>
               (\<forall>t \<in> {0..1}. P(\<lambda>x. h(t, x))))"
   unfolding homotopic_with_def
   apply (rule iffI, blast, clarify)
-  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)
+  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)
   apply auto
-  apply (force elim: continuous_on_eq)
+  using continuous_map_eq apply fastforce
   apply (drule_tac x=t in bspec, force)
   apply (subst assms; simp)
   done
 
-proposition homotopic_with_eq:
-   assumes h: "homotopic_with P X Y f g"
-       and f': "\<And>x. x \<in> X \<Longrightarrow> f' x = f x"
-       and g': "\<And>x. x \<in> X \<Longrightarrow> g' x = g x"
-       and P:  "(\<And>h k. (\<And>x. x \<in> X \<Longrightarrow> h x = k x) \<Longrightarrow> (P h \<longleftrightarrow> P k))"
-   shows "homotopic_with P X Y f' g'"
-  using h unfolding homotopic_with_def
-  apply safe
-  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)
-  apply (simp add: f' g', safe)
-  apply (fastforce intro: continuous_on_eq, fastforce)
-  apply (subst P; fastforce)
+lemma homotopic_with_mono:
+  assumes hom: "homotopic_with P X Y f g"
+    and Q: "\<And>h. \<lbrakk>continuous_map X Y h; P h\<rbrakk> \<Longrightarrow> Q h"
+  shows "homotopic_with Q X Y f g"
+  using hom
+  apply (simp add: homotopic_with_def)
+  apply (erule ex_forward)
+  apply (force simp: o_def dest: continuous_map_o_Pair intro: Q)
   done
 
-proposition homotopic_with_equal:
-   assumes contf: "continuous_on X f" and fXY: "f ` X \<subseteq> Y"
-       and gf: "\<And>x. x \<in> X \<Longrightarrow> g x = f x"
-       and P:  "P f" "P g"
-   shows "homotopic_with P X Y f g"
+lemma homotopic_with_imp_continuous_maps:
+    assumes "homotopic_with P X Y f g"
+    shows "continuous_map X Y f \<and> continuous_map X Y g"
+proof -
+  obtain h
+    where conth: "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X) Y h"
+      and h: "\<forall>x. h (0, x) = f x" "\<forall>x. h (1, x) = g x"
+    using assms by (auto simp: homotopic_with_def)
+  have *: "t \<in> {0..1} \<Longrightarrow> continuous_map X Y (h \<circ> (\<lambda>x. (t,x)))" for t
+    by (rule continuous_map_compose [OF _ conth]) (simp add: o_def continuous_map_pairwise)
+  show ?thesis
+    using h *[of 0] *[of 1] by (simp add: continuous_map_eq)
+qed
+
+lemma homotopic_with_imp_continuous:
+    assumes "homotopic_with_canon P X Y f g"
+    shows "continuous_on X f \<and> continuous_on X g"
+  by (meson assms continuous_map_subtopology_eu homotopic_with_imp_continuous_maps)
+
+lemma homotopic_with_imp_property:
+  assumes "homotopic_with P X Y f g"
+  shows "P f \<and> P g"
+proof
+  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))"
+    using assms by (force simp: homotopic_with_def)
+  show "P f" "P g"
+    using P [of 0] P [of 1] by (force simp: h)+
+qed
+
+lemma homotopic_with_equal:
+  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"
+  shows "homotopic_with P X Y f g"
   unfolding homotopic_with_def
-  apply (rule_tac x="\<lambda>(u,v). if u = 1 then g v else f v" in exI)
-  using assms
-  apply (intro conjI)
-  apply (rule continuous_on_eq [where f = "f \<circ> snd"])
-  apply (rule continuous_intros | force)+
-  apply clarify
-  apply (case_tac "t=1"; force)
+proof (intro exI conjI allI ballI)
+  let ?h = "\<lambda>(t::real,x). if t = 1 then g x else f x"
+  show "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X) Y ?h"
+  proof (rule continuous_map_eq)
+    show "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X) Y (f \<circ> snd)"
+      by (simp add: contf continuous_map_of_snd)
+  qed (auto simp: fg)
+  show "P (\<lambda>x. ?h (t, x))" if "t \<in> {0..1}" for t
+    by (cases "t = 1") (simp_all add: assms)
+qed auto
+
+lemma homotopic_with_imp_subset1:
+     "homotopic_with_canon P X Y f g \<Longrightarrow> f ` X \<subseteq> Y"
+  by (simp add: homotopic_with_def image_subset_iff) (metis atLeastAtMost_iff order_refl zero_le_one)
+
+lemma homotopic_with_imp_subset2:
+     "homotopic_with_canon P X Y f g \<Longrightarrow> g ` X \<subseteq> Y"
+  by (simp add: homotopic_with_def image_subset_iff) (metis atLeastAtMost_iff order_refl zero_le_one)
+
+lemma homotopic_with_subset_left:
+     "\<lbrakk>homotopic_with_canon P X Y f g; Z \<subseteq> X\<rbrakk> \<Longrightarrow> homotopic_with_canon P Z Y f g"
+  apply (simp add: homotopic_with_def)
+  apply (fast elim!: continuous_on_subset ex_forward)
+  done
+
+lemma homotopic_with_subset_right:
+     "\<lbrakk>homotopic_with_canon P X Y f g; Y \<subseteq> Z\<rbrakk> \<Longrightarrow> homotopic_with_canon P X Z f g"
+  apply (simp add: homotopic_with_def)
+  apply (fast elim!: continuous_on_subset ex_forward)
   done
 
-
-lemma image_Pair_const: "(\<lambda>x. (x, c)) ` A = A \<times> {c}"
-  by auto
-
-lemma homotopic_constant_maps:
-   "homotopic_with (\<lambda>x. True) s t (\<lambda>x. a) (\<lambda>x. b) \<longleftrightarrow> s = {} \<or> path_component t a b"
-proof (cases "s = {} \<or> t = {}")
-  case True with continuous_on_const show ?thesis
-    by (auto simp: homotopic_with path_component_def)
-next
-  case False
-  then obtain c where "c \<in> s" by blast
+subsection\<open>Homotopy with P is an equivalence relation\<close>
+
+text \<open>(on continuous functions mapping X into Y that satisfy P, though this only affects reflexivity)\<close>
+
+lemma homotopic_with_refl [simp]: "homotopic_with P X Y f f \<longleftrightarrow> continuous_map X Y f \<and> P f"
+  by (auto simp: homotopic_with_imp_continuous_maps intro: homotopic_with_equal dest: homotopic_with_imp_property)
+
+lemma homotopic_with_symD:
+    assumes "homotopic_with P X Y f g"
+      shows "homotopic_with P X Y g f"
+proof -
+  let ?I01 = "subtopology euclideanreal {0..1}"
+  let ?j = "\<lambda>y. (1 - fst y, snd y)"
+  have 1: "continuous_map (prod_topology ?I01 X) (prod_topology euclideanreal X) ?j"
+    apply (intro continuous_intros)
+    apply (simp_all add: prod_topology_subtopology continuous_map_from_subtopology [OF continuous_map_fst])
+    done
+  have *: "continuous_map (prod_topology ?I01 X) (prod_topology ?I01 X) ?j"
+  proof -
+    have "continuous_map (prod_topology ?I01 X) (subtopology (prod_topology euclideanreal X) ({0..1} \<times> topspace X)) ?j"
+      by (simp add: continuous_map_into_subtopology [OF 1] image_subset_iff)
+    then show ?thesis
+      by (simp add: prod_topology_subtopology(1))
+  qed
   show ?thesis
-  proof
-    assume "homotopic_with (\<lambda>x. True) s t (\<lambda>x. a) (\<lambda>x. b)"
-    then obtain h :: "real \<times> 'a \<Rightarrow> 'b"
-        where conth: "continuous_on ({0..1} \<times> s) h"
-          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)"
-      by (auto simp: homotopic_with)
-    have "continuous_on {0..1} (h \<circ> (\<lambda>t. (t, c)))"
-      apply (rule continuous_intros conth | simp add: image_Pair_const)+
-      apply (blast intro:  \<open>c \<in> s\<close> continuous_on_subset [OF conth])
-      done
-    with \<open>c \<in> s\<close> h show "s = {} \<or> path_component t a b"
-      apply (simp_all add: homotopic_with path_component_def, auto)
-      apply (drule_tac x="h \<circ> (\<lambda>t. (t, c))" in spec)
-      apply (auto simp: pathstart_def pathfinish_def path_image_def path_def)
-      done
-  next
-    assume "s = {} \<or> path_component t a b"
-    with False show "homotopic_with (\<lambda>x. True) s t (\<lambda>x. a) (\<lambda>x. b)"
-      apply (clarsimp simp: homotopic_with path_component_def pathstart_def pathfinish_def path_image_def path_def)
-      apply (rule_tac x="g \<circ> fst" in exI)
-      apply (rule conjI continuous_intros | force)+
+    using assms
+    apply (clarsimp simp add: homotopic_with_def)
+    apply (rename_tac h)
+    apply (rule_tac x="h \<circ> (\<lambda>y. (1 - fst y, snd y))" in exI)
+    apply (simp add: continuous_map_compose [OF *])
+    done
+qed
+
+lemma homotopic_with_sym:
+   "homotopic_with P X Y f g \<longleftrightarrow> homotopic_with P X Y g f"
+  by (metis homotopic_with_symD)
+
+proposition homotopic_with_trans:
+    assumes "homotopic_with P X Y f g"  "homotopic_with P X Y g h"
+    shows "homotopic_with P X Y f h"
+proof -
+  let ?X01 = "prod_topology (subtopology euclideanreal {0..1}) X"
+  obtain k1 k2
+    where contk1: "continuous_map ?X01 Y k1" and contk2: "continuous_map ?X01 Y k2"
+      and k12: "\<forall>x. k1 (1, x) = g x" "\<forall>x. k2 (0, x) = g x"
+      "\<forall>x. k1 (0, x) = f x" "\<forall>x. k2 (1, x) = h x"
+      and P:   "\<forall>t\<in>{0..1}. P (\<lambda>x. k1 (t, x))" "\<forall>t\<in>{0..1}. P (\<lambda>x. k2 (t, x))"
+    using assms by (auto simp: homotopic_with_def)
+  define k where "k \<equiv> \<lambda>y. if fst y \<le> 1/2
+                             then (k1 \<circ> (\<lambda>x. (2 *\<^sub>R fst x, snd x))) y
+                             else (k2 \<circ> (\<lambda>x. (2 *\<^sub>R fst x -1, snd x))) y"
+  have keq: "k1 (2 * u, v) = k2 (2 * u -1, v)" if "u = 1/2"  for u v
+    by (simp add: k12 that)
+  show ?thesis
+    unfolding homotopic_with_def
+  proof (intro exI conjI)
+    show "continuous_map ?X01 Y k"
+      unfolding k_def
+    proof (rule continuous_map_cases_le)
+      show fst: "continuous_map ?X01 euclideanreal fst"
+        using continuous_map_fst continuous_map_in_subtopology by blast
+      show "continuous_map ?X01 euclideanreal (\<lambda>x. 1/2)"
+        by simp
+      show "continuous_map (subtopology ?X01 {y \<in> topspace ?X01. fst y \<le> 1/2}) Y
+               (k1 \<circ> (\<lambda>x. (2 *\<^sub>R fst x, snd x)))"
+        apply (rule fst continuous_map_compose [OF _ contk1] continuous_intros continuous_map_into_subtopology | simp)+
+          apply (intro continuous_intros fst continuous_map_from_subtopology)
+         apply (force simp: prod_topology_subtopology)
+        using continuous_map_snd continuous_map_from_subtopology by blast
+      show "continuous_map (subtopology ?X01 {y \<in> topspace ?X01. 1/2 \<le> fst y}) Y
+               (k2 \<circ> (\<lambda>x. (2 *\<^sub>R fst x -1, snd x)))"
+        apply (rule fst continuous_map_compose [OF _ contk2] continuous_intros continuous_map_into_subtopology | simp)+
+          apply (rule continuous_intros fst continuous_map_from_subtopology | simp)+
+         apply (force simp: topspace_subtopology prod_topology_subtopology)
+        using continuous_map_snd  continuous_map_from_subtopology by blast
+      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"
+        if "y \<in> topspace ?X01" and "fst y = 1/2" for y
+        using that by (simp add: keq)
+    qed
+    show "\<forall>x. k (0, x) = f x"
+      by (simp add: k12 k_def)
+    show "\<forall>x. k (1, x) = h x"
+      by (simp add: k12 k_def)
+    show "\<forall>t\<in>{0..1}. P (\<lambda>x. k (t, x))"
+      using P
+      apply (clarsimp simp add: k_def)
+      apply (case_tac "t \<le> 1/2", auto)
       done
   qed
 qed
 
-
-subsection%unimportant\<open>Trivial properties\<close>
-
-lemma homotopic_with_imp_property: "homotopic_with P X Y f g \<Longrightarrow> P f \<and> P g"
-  unfolding homotopic_with_def Ball_def
+lemma homotopic_with_id2: 
+  "(\<And>x. x \<in> topspace X \<Longrightarrow> g (f x) = x) \<Longrightarrow> homotopic_with (\<lambda>x. True) X X (g \<circ> f) id"
+  by (metis comp_apply continuous_map_id eq_id_iff homotopic_with_equal homotopic_with_symD)
+
+subsection\<open>Continuity lemmas\<close>
+
+lemma homotopic_with_compose_continuous_map_left:
+  "\<lbrakk>homotopic_with p X1 X2 f g; continuous_map X2 X3 h; \<And>j. p j \<Longrightarrow> q(h \<circ> j)\<rbrakk>
+   \<Longrightarrow> homotopic_with q X1 X3 (h \<circ> f) (h \<circ> g)"
+  unfolding homotopic_with_def
   apply clarify
-  apply (frule_tac x=0 in spec)
-  apply (drule_tac x=1 in spec, auto)
+  apply (rename_tac k)
+  apply (rule_tac x="h \<circ> k" in exI)
+  apply (rule conjI continuous_map_compose | simp add: o_def)+
   done
 
-lemma continuous_on_o_Pair: "\<lbrakk>continuous_on (T \<times> X) h; t \<in> T\<rbrakk> \<Longrightarrow> continuous_on X (h \<circ> Pair t)"
-  by (fast intro: continuous_intros elim!: continuous_on_subset)
-
-lemma homotopic_with_imp_continuous:
-    assumes "homotopic_with P X Y f g"
-    shows "continuous_on X f \<and> continuous_on X g"
+lemma homotopic_compose_continuous_map_left:
+   "\<lbrakk>homotopic_with (\<lambda>k. True) X1 X2 f g; continuous_map X2 X3 h\<rbrakk>
+        \<Longrightarrow> homotopic_with (\<lambda>k. True) X1 X3 (h \<circ> f) (h \<circ> g)"
+  by (simp add: homotopic_with_compose_continuous_map_left)
+
+lemma homotopic_with_compose_continuous_map_right:
+  assumes hom: "homotopic_with p X2 X3 f g" and conth: "continuous_map X1 X2 h"
+    and q: "\<And>j. p j \<Longrightarrow> q(j \<circ> h)"
+  shows "homotopic_with q X1 X3 (f \<circ> h) (g \<circ> h)"
 proof -
-  obtain h :: "real \<times> 'a \<Rightarrow> 'b"
-    where conth: "continuous_on ({0..1} \<times> X) h"
-      and h: "\<forall>x. h (0, x) = f x" "\<forall>x. h (1, x) = g x"
-    using assms by (auto simp: homotopic_with_def)
-  have *: "t \<in> {0..1} \<Longrightarrow> continuous_on X (h \<circ> (\<lambda>x. (t,x)))" for t
-    by (rule continuous_intros continuous_on_subset [OF conth] | force)+
+  obtain k
+    where contk: "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X2) X3 k"
+      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))"
+    using hom unfolding homotopic_with_def by blast
+  have hsnd: "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X1) X2 (h \<circ> snd)"
+    by (rule continuous_map_compose [OF continuous_map_snd conth])
+  let ?h = "k \<circ> (\<lambda>(t,x). (t,h x))"
   show ?thesis
-    using h *[of 0] *[of 1] by auto
+    unfolding homotopic_with_def
+  proof (intro exI conjI allI ballI)
+    have "continuous_map (prod_topology (top_of_set {0..1}) X1)
+     (prod_topology (top_of_set {0..1::real}) X2) (\<lambda>(t, x). (t, h x))"
+      by (metis (mono_tags, lifting) case_prod_beta' comp_def continuous_map_eq continuous_map_fst continuous_map_pairedI hsnd)
+    then show "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X1) X3 ?h"
+      by (intro conjI continuous_map_compose [OF _ contk])
+    show "q (\<lambda>x. ?h (t, x))" if "t \<in> {0..1}" for t
+      using q [OF p [OF that]] by (simp add: o_def)
+  qed (auto simp: k)
 qed
 
-proposition homotopic_with_imp_subset1:
-     "homotopic_with P X Y f g \<Longrightarrow> f ` X \<subseteq> Y"
-  by (simp add: homotopic_with_def image_subset_iff) (metis atLeastAtMost_iff order_refl zero_le_one)
-
-proposition homotopic_with_imp_subset2:
-     "homotopic_with P X Y f g \<Longrightarrow> g ` X \<subseteq> Y"
-  by (simp add: homotopic_with_def image_subset_iff) (metis atLeastAtMost_iff order_refl zero_le_one)
-
-proposition homotopic_with_mono:
-    assumes hom: "homotopic_with P X Y f g"
-        and Q: "\<And>h. \<lbrakk>continuous_on X h; image h X \<subseteq> Y \<and> P h\<rbrakk> \<Longrightarrow> Q h"
-      shows "homotopic_with Q X Y f g"
-  using hom
-  apply (simp add: homotopic_with_def)
-  apply (erule ex_forward)
-  apply (force simp: intro!: Q dest: continuous_on_o_Pair)
-  done
-
-proposition homotopic_with_subset_left:
-     "\<lbrakk>homotopic_with P X Y f g; Z \<subseteq> X\<rbrakk> \<Longrightarrow> homotopic_with P Z Y f g"
-  apply (simp add: homotopic_with_def)
-  apply (fast elim!: continuous_on_subset ex_forward)
-  done
-
-proposition homotopic_with_subset_right:
-     "\<lbrakk>homotopic_with P X Y f g; Y \<subseteq> Z\<rbrakk> \<Longrightarrow> homotopic_with P X Z f g"
-  apply (simp add: homotopic_with_def)
-  apply (fast elim!: continuous_on_subset ex_forward)
-  done
+lemma homotopic_compose_continuous_map_right:
+   "\<lbrakk>homotopic_with (\<lambda>k. True) X2 X3 f g; continuous_map X1 X2 h\<rbrakk>
+        \<Longrightarrow> homotopic_with (\<lambda>k. True) X1 X3 (f \<circ> h) (g \<circ> h)"
+  by (meson homotopic_with_compose_continuous_map_right)
+
+corollary homotopic_compose:
+      shows "\<lbrakk>homotopic_with (\<lambda>x. True) X Y f f'; homotopic_with (\<lambda>x. True) Y Z g g'\<rbrakk>
+             \<Longrightarrow> homotopic_with (\<lambda>x. True) X Z (g \<circ> f) (g' \<circ> f')"
+  apply (rule homotopic_with_trans [where g = "g \<circ> f'"])
+  apply (simp add: homotopic_compose_continuous_map_left homotopic_with_imp_continuous_maps)
+  by (simp add: homotopic_compose_continuous_map_right homotopic_with_imp_continuous_maps)
+
+
 
 proposition homotopic_with_compose_continuous_right:
-    "\<lbrakk>homotopic_with (\<lambda>f. p (f \<circ> h)) X Y f g; continuous_on W h; h ` W \<subseteq> X\<rbrakk>
-     \<Longrightarrow> homotopic_with p W Y (f \<circ> h) (g \<circ> h)"
+    "\<lbrakk>homotopic_with_canon (\<lambda>f. p (f \<circ> h)) X Y f g; continuous_on W h; h ` W \<subseteq> X\<rbrakk>
+     \<Longrightarrow> homotopic_with_canon p W Y (f \<circ> h) (g \<circ> h)"
   apply (clarsimp simp add: homotopic_with_def)
   apply (rename_tac k)
   apply (rule_tac x="k \<circ> (\<lambda>y. (fst y, h (snd y)))" in exI)
@@ -180,13 +307,13 @@
   done
 
 proposition homotopic_compose_continuous_right:
-     "\<lbrakk>homotopic_with (\<lambda>f. True) X Y f g; continuous_on W h; h ` W \<subseteq> X\<rbrakk>
-      \<Longrightarrow> homotopic_with (\<lambda>f. True) W Y (f \<circ> h) (g \<circ> h)"
+     "\<lbrakk>homotopic_with_canon (\<lambda>f. True) X Y f g; continuous_on W h; h ` W \<subseteq> X\<rbrakk>
+      \<Longrightarrow> homotopic_with_canon (\<lambda>f. True) W Y (f \<circ> h) (g \<circ> h)"
   using homotopic_with_compose_continuous_right by fastforce
 
 proposition homotopic_with_compose_continuous_left:
-     "\<lbrakk>homotopic_with (\<lambda>f. p (h \<circ> f)) X Y f g; continuous_on Y h; h ` Y \<subseteq> Z\<rbrakk>
-      \<Longrightarrow> homotopic_with p X Z (h \<circ> f) (h \<circ> g)"
+     "\<lbrakk>homotopic_with_canon (\<lambda>f. p (h \<circ> f)) X Y f g; continuous_on Y h; h ` Y \<subseteq> Z\<rbrakk>
+      \<Longrightarrow> homotopic_with_canon p X Z (h \<circ> f) (h \<circ> g)"
   apply (clarsimp simp add: homotopic_with_def)
   apply (rename_tac k)
   apply (rule_tac x="h \<circ> k" in exI)
@@ -196,150 +323,171 @@
   done
 
 proposition homotopic_compose_continuous_left:
-   "\<lbrakk>homotopic_with (\<lambda>_. True) X Y f g;
+   "\<lbrakk>homotopic_with_canon (\<lambda>_. True) X Y f g;
      continuous_on Y h; h ` Y \<subseteq> Z\<rbrakk>
-    \<Longrightarrow> homotopic_with (\<lambda>f. True) X Z (h \<circ> f) (h \<circ> g)"
+    \<Longrightarrow> homotopic_with_canon (\<lambda>f. True) X Z (h \<circ> f) (h \<circ> g)"
   using homotopic_with_compose_continuous_left by fastforce
 
-proposition homotopic_with_Pair:
-   assumes hom: "homotopic_with p s t f g" "homotopic_with p' s' t' f' g'"
-       and q: "\<And>f g. \<lbrakk>p f; p' g\<rbrakk> \<Longrightarrow> q(\<lambda>(x,y). (f x, g y))"
-     shows "homotopic_with q (s \<times> s') (t \<times> t')
-                  (\<lambda>(x,y). (f x, f' y)) (\<lambda>(x,y). (g x, g' y))"
-  using hom
-  apply (clarsimp simp add: homotopic_with_def)
-  apply (rename_tac k k')
-  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)
-  apply (rule conjI continuous_intros | erule continuous_on_subset | clarsimp)+
-  apply (auto intro!: q [unfolded case_prod_unfold])
-  done
-
-lemma homotopic_on_empty [simp]: "homotopic_with (\<lambda>x. True) {} t f g"
-  by (metis continuous_on_def empty_iff homotopic_with_equal image_subset_iff)
-
-
-text\<open>Homotopy with P is an equivalence relation (on continuous functions mapping X into Y that satisfy P,
-     though this only affects reflexivity.\<close>
-
-
-proposition homotopic_with_refl:
-   "homotopic_with P X Y f f \<longleftrightarrow> continuous_on X f \<and> image f X \<subseteq> Y \<and> P f"
-  apply (rule iffI)
-  using homotopic_with_imp_continuous homotopic_with_imp_property homotopic_with_imp_subset2 apply blast
-  apply (simp add: homotopic_with_def)
-  apply (rule_tac x="f \<circ> snd" in exI)
-  apply (rule conjI continuous_intros | force)+
-  done
-
-lemma homotopic_with_symD:
-  fixes X :: "'a::real_normed_vector set"
-    assumes "homotopic_with P X Y f g"
-      shows "homotopic_with P X Y g f"
-  using assms
-  apply (clarsimp simp add: homotopic_with_def)
-  apply (rename_tac h)
-  apply (rule_tac x="h \<circ> (\<lambda>y. (1 - fst y, snd y))" in exI)
-  apply (rule conjI continuous_intros | erule continuous_on_subset | force simp: image_subset_iff)+
+lemma homotopic_from_subtopology:
+   "homotopic_with P X X' f g \<Longrightarrow> homotopic_with P (subtopology X s) X' f g"
+  unfolding homotopic_with_def
+  apply (erule ex_forward)
+  by (simp add: continuous_map_from_subtopology prod_topology_subtopology(2))
+
+lemma homotopic_on_emptyI:
+    assumes "topspace X = {}" "P f" "P g"
+    shows "homotopic_with P X X' f g"
+  unfolding homotopic_with_def
+proof (intro exI conjI ballI)
+  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
+    by (cases "t = 0", auto simp: assms)
+qed (auto simp: continuous_map_atin assms)
+
+lemma homotopic_on_empty:
+   "topspace X = {} \<Longrightarrow> (homotopic_with P X X' f g \<longleftrightarrow> P f \<and> P g)"
+  using homotopic_on_emptyI homotopic_with_imp_property by metis
+
+lemma homotopic_with_canon_on_empty [simp]: "homotopic_with_canon (\<lambda>x. True) {} t f g"
+  by (auto intro: homotopic_with_equal)
+
+lemma homotopic_constant_maps:
+   "homotopic_with (\<lambda>x. True) X X' (\<lambda>x. a) (\<lambda>x. b) \<longleftrightarrow>
+    topspace X = {} \<or> path_component_of X' a b" (is "?lhs = ?rhs")
+proof (cases "topspace X = {}")
+  case False
+  then obtain c where c: "c \<in> topspace X"
+    by blast
+  have "\<exists>g. continuous_map (top_of_set {0..1::real}) X' g \<and> g 0 = a \<and> g 1 = b"
+    if "x \<in> topspace X" and hom: "homotopic_with (\<lambda>x. True) X X' (\<lambda>x. a) (\<lambda>x. b)" for x
+  proof -
+    obtain h :: "real \<times> 'a \<Rightarrow> 'b"
+      where conth: "continuous_map (prod_topology (top_of_set {0..1}) X) X' h"
+        and h: "\<And>x. h (0, x) = a" "\<And>x. h (1, x) = b"
+      using hom by (auto simp: homotopic_with_def)
+    have cont: "continuous_map (top_of_set {0..1}) X' (h \<circ> (\<lambda>t. (t, c)))"
+      apply (rule continuous_map_compose [OF _ conth])
+      apply (rule continuous_intros c | simp)+
+      done
+    then show ?thesis
+      by (force simp: h)
+  qed
+  moreover have "homotopic_with (\<lambda>x. True) X X' (\<lambda>x. g 0) (\<lambda>x. g 1)"
+    if "x \<in> topspace X" "a = g 0" "b = g 1" "continuous_map (top_of_set {0..1}) X' g"
+    for x and g :: "real \<Rightarrow> 'b"
+    unfolding homotopic_with_def
+    by (force intro!: continuous_map_compose continuous_intros c that)
+  ultimately show ?thesis
+    using False by (auto simp: path_component_of_def pathin_def)
+qed (simp add: homotopic_on_empty)
+
+proposition homotopic_with_eq:
+   assumes h: "homotopic_with P X Y f g"
+       and f': "\<And>x. x \<in> topspace X \<Longrightarrow> f' x = f x"
+       and g': "\<And>x. x \<in> topspace X \<Longrightarrow> g' x = g x"
+       and P:  "(\<And>h k. (\<And>x. x \<in> topspace X \<Longrightarrow> h x = k x) \<Longrightarrow> P h \<longleftrightarrow> P k)"
+   shows "homotopic_with P X Y f' g'"
+  using h unfolding homotopic_with_def
+  apply safe
+  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)
+  apply (simp add: f' g', safe)
+  apply (fastforce intro: continuous_map_eq)
+  apply (subst P; fastforce)
   done
 
-proposition homotopic_with_sym:
-    fixes X :: "'a::real_normed_vector set"
-    shows "homotopic_with P X Y f g \<longleftrightarrow> homotopic_with P X Y g f"
-  using homotopic_with_symD by blast
-
-lemma split_01: "{0..1::real} = {0..1/2} \<union> {1/2..1}"
-  by force
-
-lemma split_01_prod: "{0..1::real} \<times> X = ({0..1/2} \<times> X) \<union> ({1/2..1} \<times> X)"
-  by force
-
-proposition homotopic_with_trans:
-    fixes X :: "'a::real_normed_vector set"
-    assumes "homotopic_with P X Y f g" and "homotopic_with P X Y g h"
-      shows "homotopic_with P X Y f h"
+lemma homotopic_with_prod_topology:
+  assumes "homotopic_with p X1 Y1 f f'" and "homotopic_with q X2 Y2 g g'"
+    and r: "\<And>i j. \<lbrakk>p i; q j\<rbrakk> \<Longrightarrow> r(\<lambda>(x,y). (i x, j y))"
+  shows "homotopic_with r (prod_topology X1 X2) (prod_topology Y1 Y2)
+                          (\<lambda>z. (f(fst z),g(snd z))) (\<lambda>z. (f'(fst z), g'(snd z)))"
 proof -
-  have clo1: "closedin (top_of_set ({0..1/2} \<times> X \<union> {1/2..1} \<times> X)) ({0..1/2::real} \<times> X)"
-    apply (simp add: closedin_closed split_01_prod [symmetric])
-    apply (rule_tac x="{0..1/2} \<times> UNIV" in exI)
-    apply (force simp: closed_Times)
-    done
-  have clo2: "closedin (top_of_set ({0..1/2} \<times> X \<union> {1/2..1} \<times> X)) ({1/2..1::real} \<times> X)"
-    apply (simp add: closedin_closed split_01_prod [symmetric])
-    apply (rule_tac x="{1/2..1} \<times> UNIV" in exI)
-    apply (force simp: closed_Times)
-    done
-  { fix k1 k2:: "real \<times> 'a \<Rightarrow> 'b"
-    assume cont: "continuous_on ({0..1} \<times> X) k1" "continuous_on ({0..1} \<times> X) k2"
-       and Y: "k1 ` ({0..1} \<times> X) \<subseteq> Y" "k2 ` ({0..1} \<times> X) \<subseteq> Y"
-       and geq: "\<forall>x. k1 (1, x) = g x" "\<forall>x. k2 (0, x) = g x"
-       and k12: "\<forall>x. k1 (0, x) = f x" "\<forall>x. k2 (1, x) = h x"
-       and P:   "\<forall>t\<in>{0..1}. P (\<lambda>x. k1 (t, x))" "\<forall>t\<in>{0..1}. P (\<lambda>x. k2 (t, x))"
-    define k where "k y =
-      (if fst y \<le> 1 / 2
-       then (k1 \<circ> (\<lambda>x. (2 *\<^sub>R fst x, snd x))) y
-       else (k2 \<circ> (\<lambda>x. (2 *\<^sub>R fst x -1, snd x))) y)" for y
-    have keq: "k1 (2 * u, v) = k2 (2 * u - 1, v)" if "u = 1/2"  for u v
-      by (simp add: geq that)
-    have "continuous_on ({0..1} \<times> X) k"
-      using cont
-      apply (simp add: split_01_prod k_def)
-      apply (rule clo1 clo2 continuous_on_cases_local continuous_intros | erule continuous_on_subset | simp add: linear image_subset_iff)+
-      apply (force simp: keq)
+  obtain h
+    where h: "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X1) Y1 h"
+      and h0: "\<And>x. h (0, x) = f x"
+      and h1: "\<And>x. h (1, x) = f' x"
+      and p: "\<And>t. \<lbrakk>0 \<le> t; t \<le> 1\<rbrakk> \<Longrightarrow> p (\<lambda>x. h (t,x))"
+    using assms unfolding homotopic_with_def by auto
+  obtain k
+    where k: "continuous_map (prod_topology (subtopology euclideanreal {0..1}) X2) Y2 k"
+      and k0: "\<And>x. k (0, x) = g x"
+      and k1: "\<And>x. k (1, x) = g' x"
+      and q: "\<And>t. \<lbrakk>0 \<le> t; t \<le> 1\<rbrakk> \<Longrightarrow> q (\<lambda>x. k (t,x))"
+    using assms unfolding homotopic_with_def by auto
+  let ?hk = "\<lambda>(t,x,y). (h(t,x), k(t,y))"
+  show ?thesis
+    unfolding homotopic_with_def
+  proof (intro conjI allI exI)
+    show "continuous_map (prod_topology (subtopology euclideanreal {0..1}) (prod_topology X1 X2))
+                         (prod_topology Y1 Y2) ?hk"
+      unfolding continuous_map_pairwise case_prod_unfold
+      by (rule conjI continuous_map_pairedI continuous_intros continuous_map_id [unfolded id_def]
+          continuous_map_fst_of [unfolded o_def] continuous_map_snd_of [unfolded o_def]
+          continuous_map_compose [OF _ h, unfolded o_def]
+          continuous_map_compose [OF _ k, unfolded o_def])+
+  next
+    fix x
+    show "?hk (0, x) = (f (fst x), g (snd x))" "?hk (1, x) = (f' (fst x), g' (snd x))"
+      by (auto simp: case_prod_beta h0 k0 h1 k1)
+  qed (auto simp: p q r)
+qed
+
+
+lemma homotopic_with_product_topology:
+  assumes ht: "\<And>i. i \<in> I \<Longrightarrow> homotopic_with (p i) (X i) (Y i) (f i) (g i)"
+    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)))"
+  shows "homotopic_with q (product_topology X I) (product_topology Y I)
+                          (\<lambda>z. (\<lambda>i\<in>I. (f i) (z i))) (\<lambda>z. (\<lambda>i\<in>I. (g i) (z i)))"
+proof -
+  obtain h
+    where h: "\<And>i. i \<in> I \<Longrightarrow> continuous_map (prod_topology (subtopology euclideanreal {0..1}) (X i)) (Y i) (h i)"
+      and h0: "\<And>i x. i \<in> I \<Longrightarrow> h i (0, x) = f i x"
+      and h1: "\<And>i x. i \<in> I \<Longrightarrow> h i (1, x) = g i x"
+      and p: "\<And>i t. \<lbrakk>i \<in> I; t \<in> {0..1}\<rbrakk> \<Longrightarrow> p i (\<lambda>x. h i (t,x))"
+    using ht unfolding homotopic_with_def by metis
+  show ?thesis
+    unfolding homotopic_with_def
+  proof (intro conjI allI exI)
+    let ?h = "\<lambda>(t,z). \<lambda>i\<in>I. h i (t,z i)"
+    have "continuous_map (prod_topology (subtopology euclideanreal {0..1}) (product_topology X I))
+                         (Y i) (\<lambda>x. h i (fst x, snd x i))" if "i \<in> I" for i
+      unfolding continuous_map_pairwise case_prod_unfold
+      apply (intro conjI that  continuous_intros continuous_map_compose [OF _ h, unfolded o_def])
+      using continuous_map_componentwise continuous_map_snd that apply fastforce
       done
-    moreover have "k ` ({0..1} \<times> X) \<subseteq> Y"
-      using Y by (force simp: k_def)
-    moreover have "\<forall>x. k (0, x) = f x"
-      by (simp add: k_def k12)
-    moreover have "(\<forall>x. k (1, x) = h x)"
-      by (simp add: k_def k12)
-    moreover have "\<forall>t\<in>{0..1}. P (\<lambda>x. k (t, x))"
-      using P
-      apply (clarsimp simp add: k_def)
-      apply (case_tac "t \<le> 1/2", auto)
-      done
-    ultimately have *: "\<exists>k :: real \<times> 'a \<Rightarrow> 'b.
-                       continuous_on ({0..1} \<times> X) k \<and> k ` ({0..1} \<times> X) \<subseteq> Y \<and>
-                       (\<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)))"
-      by blast
-  } note * = this
-  show ?thesis
-    using assms by (auto intro: * simp add: homotopic_with_def)
+    then show "continuous_map (prod_topology (subtopology euclideanreal {0..1}) (product_topology X I))
+         (product_topology Y I) ?h"
+      by (auto simp: continuous_map_componentwise case_prod_beta)
+    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
+      by (auto simp: case_prod_beta h0 h1)
+    show "\<forall>t\<in>{0..1}. q (\<lambda>x. ?h (t, x))"
+      by (force intro: p pq)
+  qed
 qed
 
-proposition homotopic_compose:
-      fixes s :: "'a::real_normed_vector set"
-      shows "\<lbrakk>homotopic_with (\<lambda>x. True) s t f f'; homotopic_with (\<lambda>x. True) t u g g'\<rbrakk>
-             \<Longrightarrow> homotopic_with (\<lambda>x. True) s u (g \<circ> f) (g' \<circ> f')"
-  apply (rule homotopic_with_trans [where g = "g \<circ> f'"])
-  apply (metis homotopic_compose_continuous_left homotopic_with_imp_continuous homotopic_with_imp_subset1)
-  by (metis homotopic_compose_continuous_right homotopic_with_imp_continuous homotopic_with_imp_subset2)
-
-
 text\<open>Homotopic triviality implicitly incorporates path-connectedness.\<close>
 lemma homotopic_triviality:
-  fixes S :: "'a::real_normed_vector set"
   shows  "(\<forall>f g. continuous_on S f \<and> f ` S \<subseteq> T \<and>
                  continuous_on S g \<and> g ` S \<subseteq> T
-                 \<longrightarrow> homotopic_with (\<lambda>x. True) S T f g) \<longleftrightarrow>
+                 \<longrightarrow> homotopic_with_canon (\<lambda>x. True) S T f g) \<longleftrightarrow>
           (S = {} \<or> path_connected T) \<and>
-          (\<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)))"
+          (\<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)))"
           (is "?lhs = ?rhs")
 proof (cases "S = {} \<or> T = {}")
-  case True then show ?thesis by auto
+  case True then show ?thesis
+    by (auto simp: homotopic_on_emptyI)
 next
   case False show ?thesis
   proof
     assume LHS [rule_format]: ?lhs
     have pab: "path_component T a b" if "a \<in> T" "b \<in> T" for a b
     proof -
-      have "homotopic_with (\<lambda>x. True) S T (\<lambda>x. a) (\<lambda>x. b)"
+      have "homotopic_with_canon (\<lambda>x. True) S T (\<lambda>x. a) (\<lambda>x. b)"
         by (simp add: LHS continuous_on_const image_subset_iff that)
       then show ?thesis
-        using False homotopic_constant_maps by blast
+        using False homotopic_constant_maps [of "top_of_set S" "top_of_set T" a b] by auto
     qed
-      moreover
-    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
-      by (metis (full_types) False LHS equals0I homotopic_constant_maps homotopic_with_imp_continuous homotopic_with_imp_subset2 pab that)
+    moreover
+    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
+      using False LHS continuous_on_const that by blast
     ultimately show ?rhs
       by (simp add: path_connected_component)
   next
@@ -350,15 +498,15 @@
     proof clarify
       fix f g
       assume "continuous_on S f" "f ` S \<subseteq> T" "continuous_on S g" "g ` S \<subseteq> T"
-      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)"
+      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)"
         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
       then have "c \<in> T" "d \<in> T"
-        using False homotopic_with_imp_subset2 by fastforce+
+        using False homotopic_with_imp_continuous_maps by fastforce+
       with T have "path_component T c d"
         using path_connected_component by blast
-      then have "homotopic_with (\<lambda>x. True) S T (\<lambda>x. c) (\<lambda>x. d)"
+      then have "homotopic_with_canon (\<lambda>x. True) S T (\<lambda>x. c) (\<lambda>x. d)"
         by (simp add: homotopic_constant_maps)
-      with c d show "homotopic_with (\<lambda>x. True) S T f g"
+      with c d show "homotopic_with_canon (\<lambda>x. True) S T f g"
         by (meson homotopic_with_symD homotopic_with_trans)
     qed
   qed
@@ -371,7 +519,7 @@
 definition%important homotopic_paths :: "['a set, real \<Rightarrow> 'a, real \<Rightarrow> 'a::topological_space] \<Rightarrow> bool"
   where
      "homotopic_paths s p q \<equiv>
-       homotopic_with (\<lambda>r. pathstart r = pathstart p \<and> pathfinish r = pathfinish p) {0..1} s p q"
+       homotopic_with_canon (\<lambda>r. pathstart r = pathstart p \<and> pathfinish r = pathfinish p) {0..1} s p q"
 
 lemma homotopic_paths:
    "homotopic_paths s p q \<longleftrightarrow>
@@ -393,14 +541,14 @@
 
 lemma homotopic_paths_imp_path:
      "homotopic_paths s p q \<Longrightarrow> path p \<and> path q"
-  using homotopic_paths_def homotopic_with_imp_continuous path_def by blast
+  using homotopic_paths_def homotopic_with_imp_continuous_maps path_def continuous_map_subtopology_eu by blast
 
 lemma homotopic_paths_imp_subset:
      "homotopic_paths s p q \<Longrightarrow> path_image p \<subseteq> s \<and> path_image q \<subseteq> s"
-  by (simp add: homotopic_paths_def homotopic_with_imp_subset1 homotopic_with_imp_subset2 path_image_def)
+  by (metis (mono_tags) continuous_map_subtopology_eu homotopic_paths_def homotopic_with_imp_continuous_maps path_image_def)
 
 proposition homotopic_paths_refl [simp]: "homotopic_paths s p p \<longleftrightarrow> path p \<and> path_image p \<subseteq> s"
-by (simp add: homotopic_paths_def homotopic_with_refl path_def path_image_def)
+  by (simp add: homotopic_paths_def path_def path_image_def)
 
 proposition homotopic_paths_sym: "homotopic_paths s p q \<Longrightarrow> homotopic_paths s q p"
   by (metis (mono_tags) homotopic_paths_def homotopic_paths_imp_pathfinish homotopic_paths_imp_pathstart homotopic_with_symD)
@@ -409,10 +557,16 @@
   by (metis homotopic_paths_sym)
 
 proposition homotopic_paths_trans [trans]:
-     "\<lbrakk>homotopic_paths s p q; homotopic_paths s q r\<rbrakk> \<Longrightarrow> homotopic_paths s p r"
-  apply (simp add: homotopic_paths_def)
-  apply (rule homotopic_with_trans, assumption)
-  by (metis (mono_tags, lifting) homotopic_with_imp_property homotopic_with_mono)
+  assumes "homotopic_paths s p q" "homotopic_paths s q r"
+  shows "homotopic_paths s p r"
+proof -
+  have "pathstart q = pathstart p" "pathfinish q = pathfinish p"
+    using assms by (simp_all add: homotopic_paths_imp_pathstart homotopic_paths_imp_pathfinish)
+  then have "homotopic_with_canon (\<lambda>f. pathstart f = pathstart p \<and> pathfinish f = pathfinish p) {0..1} s q r"
+    using \<open>homotopic_paths s q r\<close> homotopic_paths_def by force
+  then show ?thesis
+    using assms homotopic_paths_def homotopic_with_trans by blast
+qed
 
 proposition homotopic_paths_eq:
      "\<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"
@@ -460,7 +614,7 @@
 qed
 
 lemma homotopic_paths_subset: "\<lbrakk>homotopic_paths s p q; s \<subseteq> t\<rbrakk> \<Longrightarrow> homotopic_paths t p q"
-  using homotopic_paths_def homotopic_with_subset_right by blast
+  unfolding homotopic_paths by fast
 
 
 text\<open> A slightly ad-hoc but useful lemma in constructing homotopies.\<close>
@@ -514,9 +668,7 @@
 proposition homotopic_paths_continuous_image:
     "\<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)"
   unfolding homotopic_paths_def
-  apply (rule homotopic_with_compose_continuous_left [of _ _ _ s])
-  apply (auto simp: pathstart_def pathfinish_def elim!: homotopic_with_mono)
-  done
+  by (simp add: homotopic_with_compose_continuous_map_left pathfinish_compose pathstart_compose)
 
 
 subsection\<open>Group properties for homotopy of paths\<close>
@@ -586,7 +738,7 @@
 
 definition%important homotopic_loops :: "'a::topological_space set \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> bool"  where
  "homotopic_loops s p q \<equiv>
-     homotopic_with (\<lambda>r. pathfinish r = pathstart r) {0..1} s p q"
+     homotopic_with_canon (\<lambda>r. pathfinish r = pathstart r) {0..1} s p q"
 
 lemma homotopic_loops:
    "homotopic_loops s p q \<longleftrightarrow>
@@ -604,17 +756,17 @@
 proposition homotopic_loops_imp_path:
      "homotopic_loops s p q \<Longrightarrow> path p \<and> path q"
   unfolding homotopic_loops_def path_def
-  using homotopic_with_imp_continuous by blast
+  using homotopic_with_imp_continuous_maps continuous_map_subtopology_eu by blast
 
 proposition homotopic_loops_imp_subset:
      "homotopic_loops s p q \<Longrightarrow> path_image p \<subseteq> s \<and> path_image q \<subseteq> s"
   unfolding homotopic_loops_def path_image_def
-  by (metis homotopic_with_imp_subset1 homotopic_with_imp_subset2)
+  by (meson continuous_map_subtopology_eu homotopic_with_imp_continuous_maps)
 
 proposition homotopic_loops_refl:
      "homotopic_loops s p p \<longleftrightarrow>
       path p \<and> path_image p \<subseteq> s \<and> pathfinish p = pathstart p"
-  by (simp add: homotopic_loops_def homotopic_with_refl path_image_def path_def)
+  by (simp add: homotopic_loops_def path_image_def path_def)
 
 proposition homotopic_loops_sym: "homotopic_loops s p q \<Longrightarrow> homotopic_loops s q p"
   by (simp add: homotopic_loops_def homotopic_with_sym)
@@ -628,7 +780,7 @@
 
 proposition homotopic_loops_subset:
    "\<lbrakk>homotopic_loops s p q; s \<subseteq> t\<rbrakk> \<Longrightarrow> homotopic_loops t p q"
-  by (simp add: homotopic_loops_def homotopic_with_subset_right)
+  by (fastforce simp add: homotopic_loops)
 
 proposition homotopic_loops_eq:
    "\<lbrakk>path p; path_image p \<subseteq> s; pathfinish p = pathstart p; \<And>t. t \<in> {0..1} \<Longrightarrow> p(t) = q(t)\<rbrakk>
@@ -642,16 +794,14 @@
 proposition homotopic_loops_continuous_image:
    "\<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)"
   unfolding homotopic_loops_def
-  apply (rule homotopic_with_compose_continuous_left)
-  apply (erule homotopic_with_mono)
-  by (simp add: pathfinish_def pathstart_def)
+  by (simp add: homotopic_with_compose_continuous_map_left pathfinish_def pathstart_def)
 
 
 subsection\<open>Relations between the two variants of homotopy\<close>
 
 proposition homotopic_paths_imp_homotopic_loops:
     "\<lbrakk>homotopic_paths s p q; pathfinish p = pathstart p; pathfinish q = pathstart p\<rbrakk> \<Longrightarrow> homotopic_loops s p q"
-  by (auto simp: homotopic_paths_def homotopic_loops_def intro: homotopic_with_mono)
+  by (auto simp: homotopic_with_def homotopic_paths_def homotopic_loops_def)
 
 proposition homotopic_loops_imp_homotopic_paths_null:
   assumes "homotopic_loops s p (linepath a a)"
@@ -828,7 +978,7 @@
   assumes contf: "continuous_on s f"
       and contg:"continuous_on s g"
       and sub: "\<And>x. x \<in> s \<Longrightarrow> closed_segment (f x) (g x) \<subseteq> t"
-    shows "homotopic_with (\<lambda>z. True) s t f g"
+    shows "homotopic_with_canon (\<lambda>z. True) s t f g"
   apply (simp add: homotopic_with_def)
   apply (rule_tac x="\<lambda>y. ((1 - (fst y)) *\<^sub>R f(snd y) + (fst y) *\<^sub>R g(snd y))" in exI)
   apply (intro conjI)
@@ -1208,7 +1358,7 @@
 subsection\<open>Contractible sets\<close>
 
 definition%important contractible where
- "contractible S \<equiv> \<exists>a. homotopic_with (\<lambda>x. True) S S id (\<lambda>x. a)"
+ "contractible S \<equiv> \<exists>a. homotopic_with_canon (\<lambda>x. True) S S id (\<lambda>x. a)"
 
 proposition contractible_imp_simply_connected:
   fixes S :: "_::real_normed_vector set"
@@ -1217,10 +1367,10 @@
   case True then show ?thesis by force
 next
   case False
-  obtain a where a: "homotopic_with (\<lambda>x. True) S S id (\<lambda>x. a)"
+  obtain a where a: "homotopic_with_canon (\<lambda>x. True) S S id (\<lambda>x. a)"
     using assms by (force simp: contractible_def)
   then have "a \<in> S"
-    by (metis False homotopic_constant_maps homotopic_with_symD homotopic_with_trans path_component_mem(2))
+    by (metis False homotopic_constant_maps homotopic_with_symD homotopic_with_trans path_component_in_topspace topspace_euclidean_subtopology)
   show ?thesis
     apply (simp add: simply_connected_eq_contractible_loop_all False)
     apply (rule bexI [OF _ \<open>a \<in> S\<close>])
@@ -1246,14 +1396,14 @@
   assumes f: "continuous_on S f" "f ` S \<subseteq> T"
       and g: "continuous_on T g" "g ` T \<subseteq> U"
       and T: "contractible T"
-    obtains c where "homotopic_with (\<lambda>h. True) S U (g \<circ> f) (\<lambda>x. c)"
+    obtains c where "homotopic_with_canon (\<lambda>h. True) S U (g \<circ> f) (\<lambda>x. c)"
 proof -
-  obtain b where b: "homotopic_with (\<lambda>x. True) T T id (\<lambda>x. b)"
+  obtain b where b: "homotopic_with_canon (\<lambda>x. True) T T id (\<lambda>x. b)"
     using assms by (force simp: contractible_def)
-  have "homotopic_with (\<lambda>f. True) T U (g \<circ> id) (g \<circ> (\<lambda>x. b))"
-    by (rule homotopic_compose_continuous_left [OF b g])
-  then have "homotopic_with (\<lambda>f. True) S U (g \<circ> id \<circ> f) (g \<circ> (\<lambda>x. b) \<circ> f)"
-    by (rule homotopic_compose_continuous_right [OF _ f])
+  have "homotopic_with_canon (\<lambda>f. True) T U (g \<circ> id) (g \<circ> (\<lambda>x. b))"
+    by (metis Abstract_Topology.continuous_map_subtopology_eu b g homotopic_compose_continuous_map_left)
+  then have "homotopic_with_canon (\<lambda>f. True) S U (g \<circ> id \<circ> f) (g \<circ> (\<lambda>x. b) \<circ> f)"
+    by (simp add: f homotopic_with_compose_continuous_map_right)
   then show ?thesis
     by (simp add: comp_def that)
 qed
@@ -1261,7 +1411,7 @@
 lemma nullhomotopic_into_contractible:
   assumes f: "continuous_on S f" "f ` S \<subseteq> T"
       and T: "contractible T"
-    obtains c where "homotopic_with (\<lambda>h. True) S T f (\<lambda>x. c)"
+    obtains c where "homotopic_with_canon (\<lambda>h. True) S T f (\<lambda>x. c)"
 apply (rule nullhomotopic_through_contractible [OF f, of id T])
 using assms
 apply (auto simp: continuous_on_id)
@@ -1270,7 +1420,7 @@
 lemma nullhomotopic_from_contractible:
   assumes f: "continuous_on S f" "f ` S \<subseteq> T"
       and S: "contractible S"
-    obtains c where "homotopic_with (\<lambda>h. True) S T f (\<lambda>x. c)"
+    obtains c where "homotopic_with_canon (\<lambda>h. True) S T f (\<lambda>x. c)"
 apply (rule nullhomotopic_through_contractible [OF continuous_on_id _ f S, of S])
 using assms
 apply (auto simp: comp_def)
@@ -1283,13 +1433,13 @@
           "continuous_on S f2" "f2 ` S \<subseteq> T"
           "continuous_on T g2" "g2 ` T \<subseteq> U"
           "contractible T" "path_connected U"
-   shows "homotopic_with (\<lambda>h. True) S U (g1 \<circ> f1) (g2 \<circ> f2)"
+   shows "homotopic_with_canon (\<lambda>h. True) S U (g1 \<circ> f1) (g2 \<circ> f2)"
 proof -
-  obtain c1 where c1: "homotopic_with (\<lambda>h. True) S U (g1 \<circ> f1) (\<lambda>x. c1)"
+  obtain c1 where c1: "homotopic_with_canon (\<lambda>h. True) S U (g1 \<circ> f1) (\<lambda>x. c1)"
     apply (rule nullhomotopic_through_contractible [of S f1 T g1 U])
     using assms apply auto
     done
-  obtain c2 where c2: "homotopic_with (\<lambda>h. True) S U (g2 \<circ> f2) (\<lambda>x. c2)"
+  obtain c2 where c2: "homotopic_with_canon (\<lambda>h. True) S U (g2 \<circ> f2) (\<lambda>x. c2)"
     apply (rule nullhomotopic_through_contractible [of S f2 T g2 U])
     using assms apply auto
     done
@@ -1299,7 +1449,7 @@
   next
     case False
     with c1 c2 have "c1 \<in> U" "c2 \<in> U"
-      using homotopic_with_imp_subset2 all_not_in_conv image_subset_iff by blast+
+      using homotopic_with_imp_continuous_maps by fastforce+
     with \<open>path_connected U\<close> show ?thesis by blast
   qed
   show ?thesis
@@ -1315,24 +1465,24 @@
   assumes f: "continuous_on S f" "f ` S \<subseteq> T"
       and g: "continuous_on S g" "g ` S \<subseteq> T"
       and T: "contractible T"
-    shows "homotopic_with (\<lambda>h. True) S T f g"
+    shows "homotopic_with_canon (\<lambda>h. True) S T f g"
 using homotopic_through_contractible [of S f T id T g id]
-by (simp add: assms contractible_imp_path_connected continuous_on_id)
+by (simp add: assms contractible_imp_path_connected)
 
 lemma homotopic_from_contractible:
   fixes S :: "'a::real_normed_vector set" and T:: "'b::real_normed_vector set"
   assumes f: "continuous_on S f" "f ` S \<subseteq> T"
       and g: "continuous_on S g" "g ` S \<subseteq> T"
       and "contractible S" "path_connected T"
-    shows "homotopic_with (\<lambda>h. True) S T f g"
+    shows "homotopic_with_canon (\<lambda>h. True) S T f g"
 using homotopic_through_contractible [of S id S f T id g]
-by (simp add: assms contractible_imp_path_connected continuous_on_id)
+by (simp add: assms contractible_imp_path_connected)
 
 lemma starlike_imp_contractible_gen:
   fixes S :: "'a::real_normed_vector set"
   assumes S: "starlike S"
       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)"
-    obtains a where "homotopic_with P S S (\<lambda>x. x) (\<lambda>x. a)"
+    obtains a where "homotopic_with_canon P S S (\<lambda>x. x) (\<lambda>x. a)"
 proof -
   obtain a where "a \<in> S" and a: "\<And>x. x \<in> S \<Longrightarrow> closed_segment a x \<subseteq> S"
     using S by (auto simp: starlike_def)
@@ -1385,7 +1535,7 @@
 using convex_imp_simply_connected is_interval_convex_1 is_interval_path_connected_1 simply_connected_imp_path_connected by auto
 
 lemma contractible_empty [simp]: "contractible {}"
-  by (simp add: contractible_def homotopic_with)
+  by (simp add: contractible_def homotopic_on_emptyI)
 
 lemma contractible_convex_tweak_boundary_points:
   fixes S :: "'a::euclidean_space set"
@@ -1445,27 +1595,6 @@
     done
 qed
 
-lemma homotopy_dominated_contractibility:
-  fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set"
-  assumes S: "contractible S"
-      and f: "continuous_on S f" "image f S \<subseteq> T"
-      and g: "continuous_on T g" "image g T \<subseteq> S"
-      and hom: "homotopic_with (\<lambda>x. True) T T (f \<circ> g) id"
-    shows "contractible T"
-proof -
-  obtain b where "homotopic_with (\<lambda>h. True) S T f (\<lambda>x. b)"
-    using nullhomotopic_from_contractible [OF f S] .
-  then have homg: "homotopic_with (\<lambda>x. True) T T ((\<lambda>x. b) \<circ> g) (f \<circ> g)"
-    by (rule homotopic_with_compose_continuous_right [OF homotopic_with_symD g])
-  show ?thesis
-    apply (simp add: contractible_def)
-    apply (rule exI [where x = b])
-    apply (rule homotopic_with_symD)
-    apply (rule homotopic_with_trans [OF _ hom])
-    using homg apply (simp add: o_def)
-    done
-qed
-
 
 subsection\<open>Local versions of topological properties in general\<close>
 
@@ -1541,7 +1670,7 @@
 apply (simp add: open_Int)
 apply (rule_tac x="V1 \<inter> V2" in exI)
 apply (auto intro: P)
-done
+  done
 
 lemma locally_Times:
   fixes S :: "('a::metric_space) set" and T :: "('b::metric_space) set"
@@ -1561,7 +1690,7 @@
   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"
     apply (rule_tac x="U1 \<times> V1" in exI)
     apply (rule_tac x="U2 \<times> V2" in exI)
-    apply (auto simp: openin_Times R)
+    apply (auto simp: openin_Times R openin_Times_eq)
     done
 qed
 
@@ -3195,10 +3324,10 @@
       and Qeq: "\<And>h k. (\<And>x. x \<in> u \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
       and hom: "\<And>f g. \<lbrakk>continuous_on u f; f ` u \<subseteq> s; P f;
                        continuous_on u g; g ` u \<subseteq> s; P g\<rbrakk>
-                       \<Longrightarrow> homotopic_with P u s f g"
+                       \<Longrightarrow> homotopic_with_canon P u s f g"
       and contf: "continuous_on u f" and imf: "f ` u \<subseteq> t" and Qf: "Q f"
       and contg: "continuous_on u g" and img: "g ` u \<subseteq> t" and Qg: "Q g"
-    shows "homotopic_with Q u t f g"
+    shows "homotopic_with_canon Q u t f g"
 proof -
   have feq: "\<And>x. x \<in> u \<Longrightarrow> (h \<circ> (k \<circ> f)) x = f x" using idhk imf by auto
   have geq: "\<And>x. x \<in> u \<Longrightarrow> (h \<circ> (k \<circ> g)) x = g x" using idhk img by auto
@@ -3214,17 +3343,15 @@
     using img imk by fastforce
   moreover have "P (k \<circ> g)"
     by (simp add: P Qg contg img)
-  ultimately have "homotopic_with P u s (k \<circ> f) (k \<circ> g)"
+  ultimately have "homotopic_with_canon P u s (k \<circ> f) (k \<circ> g)"
     by (rule hom)
-  then have "homotopic_with Q u t (h \<circ> (k \<circ> f)) (h \<circ> (k \<circ> g))"
+  then have "homotopic_with_canon Q u t (h \<circ> (k \<circ> f)) (h \<circ> (k \<circ> g))"
     apply (rule homotopic_with_compose_continuous_left [OF homotopic_with_mono])
     using Q by (auto simp: conth imh)
   then show ?thesis
     apply (rule homotopic_with_eq)
-    apply (metis feq)
-    apply (metis geq)
-    apply (metis Qeq)
-    done
+    using feq geq apply fastforce+
+    using Qeq topspace_euclidean_subtopology by blast
 qed
 
 lemma homotopically_trivial_retraction_null_gen:
@@ -3232,9 +3359,9 @@
       and Q: "\<And>f. \<lbrakk>continuous_on u f; f ` u \<subseteq> s; P f\<rbrakk> \<Longrightarrow> Q(h \<circ> f)"
       and Qeq: "\<And>h k. (\<And>x. x \<in> u \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
       and hom: "\<And>f. \<lbrakk>continuous_on u f; f ` u \<subseteq> s; P f\<rbrakk>
-                     \<Longrightarrow> \<exists>c. homotopic_with P u s f (\<lambda>x. c)"
+                     \<Longrightarrow> \<exists>c. homotopic_with_canon P u s f (\<lambda>x. c)"
       and contf: "continuous_on u f" and imf:"f ` u \<subseteq> t" and Qf: "Q f"
-  obtains c where "homotopic_with Q u t f (\<lambda>x. c)"
+  obtains c where "homotopic_with_canon Q u t f (\<lambda>x. c)"
 proof -
   have feq: "\<And>x. x \<in> u \<Longrightarrow> (h \<circ> (k \<circ> f)) x = f x" using idhk imf by auto
   have "continuous_on u (k \<circ> f)"
@@ -3243,17 +3370,17 @@
     using imf imk by fastforce
   moreover have "P (k \<circ> f)"
     by (simp add: P Qf contf imf)
-  ultimately obtain c where "homotopic_with P u s (k \<circ> f) (\<lambda>x. c)"
+  ultimately obtain c where "homotopic_with_canon P u s (k \<circ> f) (\<lambda>x. c)"
     by (metis hom)
-  then have "homotopic_with Q u t (h \<circ> (k \<circ> f)) (h \<circ> (\<lambda>x. c))"
+  then have "homotopic_with_canon Q u t (h \<circ> (k \<circ> f)) (h \<circ> (\<lambda>x. c))"
     apply (rule homotopic_with_compose_continuous_left [OF homotopic_with_mono])
     using Q by (auto simp: conth imh)
   then show ?thesis
     apply (rule_tac c = "h c" in that)
     apply (erule homotopic_with_eq)
-    apply (metis feq, simp)
-    apply (metis Qeq)
-    done
+    using feq apply auto[1]
+    apply simp
+    using Qeq topspace_euclidean_subtopology by blast
 qed
 
 lemma cohomotopically_trivial_retraction_gen:
@@ -3262,10 +3389,10 @@
       and Qeq: "\<And>h k. (\<And>x. x \<in> t \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
       and hom: "\<And>f g. \<lbrakk>continuous_on s f; f ` s \<subseteq> u; P f;
                        continuous_on s g; g ` s \<subseteq> u; P g\<rbrakk>
-                       \<Longrightarrow> homotopic_with P s u f g"
+                       \<Longrightarrow> homotopic_with_canon P s u f g"
       and contf: "continuous_on t f" and imf: "f ` t \<subseteq> u" and Qf: "Q f"
       and contg: "continuous_on t g" and img: "g ` t \<subseteq> u" and Qg: "Q g"
-    shows "homotopic_with Q t u f g"
+    shows "homotopic_with_canon Q t u f g"
 proof -
   have feq: "\<And>x. x \<in> t \<Longrightarrow> (f \<circ> h \<circ> k) x = f x" using idhk imf by auto
   have geq: "\<And>x. x \<in> t \<Longrightarrow> (g \<circ> h \<circ> k) x = g x" using idhk img by auto
@@ -3281,17 +3408,16 @@
     using img imh by fastforce
   moreover have "P (g \<circ> h)"
     by (simp add: P Qg contg img)
-  ultimately have "homotopic_with P s u (f \<circ> h) (g \<circ> h)"
+  ultimately have "homotopic_with_canon P s u (f \<circ> h) (g \<circ> h)"
     by (rule hom)
-  then have "homotopic_with Q t u (f \<circ> h \<circ> k) (g \<circ> h \<circ> k)"
+  then have "homotopic_with_canon Q t u (f \<circ> h \<circ> k) (g \<circ> h \<circ> k)"
     apply (rule homotopic_with_compose_continuous_right [OF homotopic_with_mono])
     using Q by (auto simp: contk imk)
   then show ?thesis
     apply (rule homotopic_with_eq)
-    apply (metis feq)
-    apply (metis geq)
-    apply (metis Qeq)
-    done
+    using feq apply auto[1]
+    using geq apply auto[1]
+    using Qeq topspace_euclidean_subtopology by blast
 qed
 
 lemma cohomotopically_trivial_retraction_null_gen:
@@ -3299,9 +3425,9 @@
       and Q: "\<And>f. \<lbrakk>continuous_on s f; f ` s \<subseteq> u; P f\<rbrakk> \<Longrightarrow> Q(f \<circ> k)"
       and Qeq: "\<And>h k. (\<And>x. x \<in> t \<Longrightarrow> h x = k x) \<Longrightarrow> Q h = Q k"
       and hom: "\<And>f g. \<lbrakk>continuous_on s f; f ` s \<subseteq> u; P f\<rbrakk>
-                       \<Longrightarrow> \<exists>c. homotopic_with P s u f (\<lambda>x. c)"
+                       \<Longrightarrow> \<exists>c. homotopic_with_canon P s u f (\<lambda>x. c)"
       and contf: "continuous_on t f" and imf: "f ` t \<subseteq> u" and Qf: "Q f"
-  obtains c where "homotopic_with Q t u f (\<lambda>x. c)"
+  obtains c where "homotopic_with_canon Q t u f (\<lambda>x. c)"
 proof -
   have feq: "\<And>x. x \<in> t \<Longrightarrow> (f \<circ> h \<circ> k) x = f x" using idhk imf by auto
   have "continuous_on s (f \<circ> h)"
@@ -3310,17 +3436,17 @@
     using imf imh by fastforce
   moreover have "P (f \<circ> h)"
     by (simp add: P Qf contf imf)
-  ultimately obtain c where "homotopic_with P s u (f \<circ> h) (\<lambda>x. c)"
+  ultimately obtain c where "homotopic_with_canon P s u (f \<circ> h) (\<lambda>x. c)"
     by (metis hom)
-  then have "homotopic_with Q t u (f \<circ> h \<circ> k) ((\<lambda>x. c) \<circ> k)"
+  then have "homotopic_with_canon Q t u (f \<circ> h \<circ> k) ((\<lambda>x. c) \<circ> k)"
     apply (rule homotopic_with_compose_continuous_right [OF homotopic_with_mono])
     using Q by (auto simp: contk imk)
   then show ?thesis
     apply (rule_tac c = c in that)
     apply (erule homotopic_with_eq)
-    apply (metis feq, simp)
-    apply (metis Qeq)
-    done
+    using feq apply auto[1]
+    apply simp
+    using Qeq topspace_euclidean_subtopology by blast
 qed
 
 end
@@ -3346,59 +3472,64 @@
 
 subsection\<open>Homotopy equivalence\<close>
 
-definition%important homotopy_eqv :: "'a::topological_space set \<Rightarrow> 'b::topological_space set \<Rightarrow> bool"
-             (infix "homotopy'_eqv" 50)
-  where "S homotopy_eqv T \<equiv>
-        \<exists>f g. continuous_on S f \<and> f ` S \<subseteq> T \<and>
-              continuous_on T g \<and> g ` T \<subseteq> S \<and>
-              homotopic_with (\<lambda>x. True) S S (g \<circ> f) id \<and>
-              homotopic_with (\<lambda>x. True) T T (f \<circ> g) id"
-
-lemma homeomorphic_imp_homotopy_eqv: "S homeomorphic T \<Longrightarrow> S homotopy_eqv T"
-  unfolding homeomorphic_def homotopy_eqv_def homeomorphism_def
-  by (fastforce intro!: homotopic_with_equal continuous_on_compose)
-
-lemma homotopy_eqv_refl: "S homotopy_eqv S"
-  by (rule homeomorphic_imp_homotopy_eqv homeomorphic_refl)+
-
-lemma homotopy_eqv_sym: "S homotopy_eqv T \<longleftrightarrow> T homotopy_eqv S"
-  by (auto simp: homotopy_eqv_def)
+subsection\<open>Homotopy equivalence of topological spaces.\<close>
+
+definition%important homotopy_equivalent_space
+             (infix "homotopy'_equivalent'_space" 50)
+  where "X homotopy_equivalent_space Y \<equiv>
+        (\<exists>f g. continuous_map X Y f \<and>
+              continuous_map Y X g \<and>
+              homotopic_with (\<lambda>x. True) X X (g \<circ> f) id \<and>
+              homotopic_with (\<lambda>x. True) Y Y (f \<circ> g) id)"
+
+lemma homeomorphic_imp_homotopy_equivalent_space:
+  "X homeomorphic_space Y \<Longrightarrow> X homotopy_equivalent_space Y"
+  unfolding homeomorphic_space_def homotopy_equivalent_space_def
+  apply (erule ex_forward)+
+  by (simp add: homotopic_with_equal homotopic_with_sym homeomorphic_maps_def)
+
+lemma homotopy_equivalent_space_refl:
+   "X homotopy_equivalent_space X"
+  by (simp add: homeomorphic_imp_homotopy_equivalent_space homeomorphic_space_refl)
+
+lemma homotopy_equivalent_space_sym:
+   "X homotopy_equivalent_space Y \<longleftrightarrow> Y homotopy_equivalent_space X"
+  by (meson homotopy_equivalent_space_def)
 
 lemma homotopy_eqv_trans [trans]:
-    fixes S :: "'a::real_normed_vector set" and U :: "'c::real_normed_vector set"
-  assumes ST: "S homotopy_eqv T" and TU: "T homotopy_eqv U"
-    shows "S homotopy_eqv U"
+  assumes 1: "X homotopy_equivalent_space Y" and 2: "Y homotopy_equivalent_space U"
+    shows "X homotopy_equivalent_space U"
 proof -
-  obtain f1 g1 where f1: "continuous_on S f1" "f1 ` S \<subseteq> T"
-                 and g1: "continuous_on T g1" "g1 ` T \<subseteq> S"
-                 and hom1: "homotopic_with (\<lambda>x. True) S S (g1 \<circ> f1) id"
-                           "homotopic_with (\<lambda>x. True) T T (f1 \<circ> g1) id"
-    using ST by (auto simp: homotopy_eqv_def)
-  obtain f2 g2 where f2: "continuous_on T f2" "f2 ` T \<subseteq> U"
-                 and g2: "continuous_on U g2" "g2 ` U \<subseteq> T"
-                 and hom2: "homotopic_with (\<lambda>x. True) T T (g2 \<circ> f2) id"
+  obtain f1 g1 where f1: "continuous_map X Y f1"
+                 and g1: "continuous_map Y X g1"
+                 and hom1: "homotopic_with (\<lambda>x. True) X X (g1 \<circ> f1) id"
+                           "homotopic_with (\<lambda>x. True) Y Y (f1 \<circ> g1) id"
+    using 1 by (auto simp: homotopy_equivalent_space_def)
+  obtain f2 g2 where f2: "continuous_map Y U f2"
+                 and g2: "continuous_map U Y g2"
+                 and hom2: "homotopic_with (\<lambda>x. True) Y Y (g2 \<circ> f2) id"
                            "homotopic_with (\<lambda>x. True) U U (f2 \<circ> g2) id"
-    using TU by (auto simp: homotopy_eqv_def)
-  have "homotopic_with (\<lambda>f. True) S T (g2 \<circ> f2 \<circ> f1) (id \<circ> f1)"
-    by (rule homotopic_with_compose_continuous_right hom2 f1)+
-  then have "homotopic_with (\<lambda>f. True) S T (g2 \<circ> (f2 \<circ> f1)) (id \<circ> f1)"
+    using 2 by (auto simp: homotopy_equivalent_space_def)
+  have "homotopic_with (\<lambda>f. True) X Y (g2 \<circ> f2 \<circ> f1) (id \<circ> f1)"
+    using f1 hom2(1) homotopic_compose_continuous_map_right by blast
+  then have "homotopic_with (\<lambda>f. True) X Y (g2 \<circ> (f2 \<circ> f1)) (id \<circ> f1)"
     by (simp add: o_assoc)
-  then have "homotopic_with (\<lambda>x. True) S S
+  then have "homotopic_with (\<lambda>x. True) X X
          (g1 \<circ> (g2 \<circ> (f2 \<circ> f1))) (g1 \<circ> (id \<circ> f1))"
-    by (simp add: g1 homotopic_with_compose_continuous_left)
-  moreover have "homotopic_with (\<lambda>x. True) S S (g1 \<circ> id \<circ> f1) id"
+    by (simp add: g1 homotopic_compose_continuous_map_left)
+  moreover have "homotopic_with (\<lambda>x. True) X X (g1 \<circ> id \<circ> f1) id"
     using hom1 by simp
-  ultimately have SS: "homotopic_with (\<lambda>x. True) S S (g1 \<circ> g2 \<circ> (f2 \<circ> f1)) id"
+  ultimately have SS: "homotopic_with (\<lambda>x. True) X X (g1 \<circ> g2 \<circ> (f2 \<circ> f1)) id"
     apply (simp add: o_assoc)
     apply (blast intro: homotopic_with_trans)
     done
-  have "homotopic_with (\<lambda>f. True) U T (f1 \<circ> g1 \<circ> g2) (id \<circ> g2)"
-    by (rule homotopic_with_compose_continuous_right hom1 g2)+
-  then have "homotopic_with (\<lambda>f. True) U T (f1 \<circ> (g1 \<circ> g2)) (id \<circ> g2)"
+  have "homotopic_with (\<lambda>f. True) U Y (f1 \<circ> g1 \<circ> g2) (id \<circ> g2)"
+    using g2 hom1(2) homotopic_with_compose_continuous_map_right by fastforce
+  then have "homotopic_with (\<lambda>f. True) U Y (f1 \<circ> (g1 \<circ> g2)) (id \<circ> g2)"
     by (simp add: o_assoc)
   then have "homotopic_with (\<lambda>x. True) U U
          (f2 \<circ> (f1 \<circ> (g1 \<circ> g2))) (f2 \<circ> (id \<circ> g2))"
-    by (simp add: f2 homotopic_with_compose_continuous_left)
+    by (simp add: f2 homotopic_with_compose_continuous_map_left)
   moreover have "homotopic_with (\<lambda>x. True) U U (f2 \<circ> id \<circ> g2) id"
     using hom2 by simp
   ultimately have UU: "homotopic_with (\<lambda>x. True) U U (f2 \<circ> f1 \<circ> (g1 \<circ> g2)) id"
@@ -3406,14 +3537,382 @@
     apply (blast intro: homotopic_with_trans)
     done
   show ?thesis
-    unfolding homotopy_eqv_def
-    apply (rule_tac x = "f2 \<circ> f1" in exI)
-    apply (rule_tac x = "g1 \<circ> g2" in exI)
-    apply (intro conjI continuous_on_compose SS UU)
-    using f1 f2 g1 g2  apply (force simp: elim!: continuous_on_subset)+
-    done
+    unfolding homotopy_equivalent_space_def
+    by (blast intro: f1 f2 g1 g2 continuous_map_compose SS UU)
+qed
+
+lemma deformation_retraction_imp_homotopy_equivalent_space:
+  "\<lbrakk>homotopic_with (\<lambda>x. True) X X (s \<circ> r) id; retraction_maps X Y r s\<rbrakk>
+    \<Longrightarrow> X homotopy_equivalent_space Y"
+  unfolding homotopy_equivalent_space_def retraction_maps_def
+  apply (rule_tac x=r in exI)
+  apply (rule_tac x=s in exI)
+  apply (auto simp: homotopic_with_equal continuous_map_compose)
+  done
+
+lemma deformation_retract_imp_homotopy_equivalent_space:
+   "\<lbrakk>homotopic_with (\<lambda>x. True) X X r id; retraction_maps X Y r id\<rbrakk>
+    \<Longrightarrow> X homotopy_equivalent_space Y"
+  using deformation_retraction_imp_homotopy_equivalent_space by force
+
+lemma deformation_retract_of_space:
+  "S \<subseteq> topspace X \<and>
+   (\<exists>r. homotopic_with (\<lambda>x. True) X X id r \<and> retraction_maps X (subtopology X S) r id) \<longleftrightarrow>
+   S retract_of_space X \<and> (\<exists>f. homotopic_with (\<lambda>x. True) X X id f \<and> f ` (topspace X) \<subseteq> S)"
+proof (cases "S \<subseteq> topspace X")
+  case True
+  moreover have "(\<exists>r. homotopic_with (\<lambda>x. True) X X id r \<and> retraction_maps X (subtopology X S) r id)
+             \<longleftrightarrow> (S retract_of_space X \<and> (\<exists>f. homotopic_with (\<lambda>x. True) X X id f \<and> f ` topspace X \<subseteq> S))"
+    unfolding retract_of_space_def
+  proof safe
+    fix f r
+    assume f: "homotopic_with (\<lambda>x. True) X X id f"
+      and fS: "f ` topspace X \<subseteq> S"
+      and r: "continuous_map X (subtopology X S) r"
+      and req: "\<forall>x\<in>S. r x = x"
+    show "\<exists>r. homotopic_with (\<lambda>x. True) X X id r \<and> retraction_maps X (subtopology X S) r id"
+    proof (intro exI conjI)
+      have "homotopic_with (\<lambda>x. True) X X f r"
+        proof (rule homotopic_with_eq)
+          show "homotopic_with (\<lambda>x. True) X X (r \<circ> f) (r \<circ> id)"
+            using homotopic_with_symD continuous_map_into_fulltopology f homotopic_compose_continuous_map_left r by blast
+          show "f x = (r \<circ> f) x" if "x \<in> topspace X" for x
+            using that fS req by auto
+        qed auto
+      then show "homotopic_with (\<lambda>x. True) X X id r"
+        by (rule homotopic_with_trans [OF f])
+    next
+      show "retraction_maps X (subtopology X S) r id"
+        by (simp add: r req retraction_maps_def topspace_subtopology)
+    qed
+  qed (use True in \<open>auto simp: retraction_maps_def topspace_subtopology_subset continuous_map_in_subtopology\<close>)
+  ultimately show ?thesis by simp
+qed (auto simp: retract_of_space_def retraction_maps_def)
+
+
+
+subsection\<open>Contractible spaces\<close>
+
+text\<open>The definition (which agrees with "contractible" on subsets of Euclidean space)
+is a little cryptic because we don't in fact assume that the constant "a" is in the space.
+This forces the convention that the empty space / set is contractible, avoiding some special cases. \<close>
+
+definition contractible_space where
+  "contractible_space X \<equiv> \<exists>a. homotopic_with (\<lambda>x. True) X X id (\<lambda>x. a)"
+
+lemma contractible_space_top_of_set [simp]:"contractible_space (top_of_set S) \<longleftrightarrow> contractible S"
+  by (auto simp: contractible_space_def contractible_def)
+
+lemma contractible_space_empty:
+   "topspace X = {} \<Longrightarrow> contractible_space X"
+  apply (simp add: contractible_space_def homotopic_with_def)
+  apply (rule_tac x=undefined in exI)
+  apply (rule_tac x="\<lambda>(t,x). if t = 0 then x else undefined" in exI)
+  apply (auto simp: continuous_map_on_empty)
+  done
+
+lemma contractible_space_singleton:
+  "topspace X = {a} \<Longrightarrow> contractible_space X"
+  apply (simp add: contractible_space_def homotopic_with_def)
+  apply (rule_tac x=a in exI)
+  apply (rule_tac x="\<lambda>(t,x). if t = 0 then x else a" in exI)
+  apply (auto intro: continuous_map_eq [where f = "\<lambda>z. a"])
+  done
+
+lemma contractible_space_subset_singleton:
+   "topspace X \<subseteq> {a} \<Longrightarrow> contractible_space X"
+  by (meson contractible_space_empty contractible_space_singleton subset_singletonD)
+
+lemma contractible_space_subtopology_singleton:
+   "contractible_space(subtopology X {a})"
+  by (meson contractible_space_subset_singleton insert_subset path_connectedin_singleton path_connectedin_subtopology subsetI)
+
+lemma contractible_space:
+   "contractible_space X \<longleftrightarrow>
+        topspace X = {} \<or>
+        (\<exists>a \<in> topspace X. homotopic_with (\<lambda>x. True) X X id (\<lambda>x. a))"
+proof (cases "topspace X = {}")
+  case False
+  then show ?thesis
+    apply (auto simp: contractible_space_def)
+    using homotopic_with_imp_continuous_maps by fastforce
+qed (simp add: contractible_space_empty)
+
+lemma contractible_imp_path_connected_space:
+  assumes "contractible_space X" shows "path_connected_space X"
+proof (cases "topspace X = {}")
+  case False
+  have *: "path_connected_space X"
+    if "a \<in> topspace X" and conth: "continuous_map (prod_topology (top_of_set {0..1}) X) X h"
+      and h: "\<forall>x. h (0, x) = x" "\<forall>x. h (1, x) = a"
+    for a and h :: "real \<times> 'a \<Rightarrow> 'a"
+  proof -
+    have "path_component_of X b a" if "b \<in> topspace X" for b
+      using that unfolding path_component_of_def
+      apply (rule_tac x="h \<circ> (\<lambda>x. (x,b))" in exI)
+      apply (simp add: h pathin_def)
+      apply (rule continuous_map_compose [OF _ conth])
+      apply (auto simp: continuous_map_pairwise intro!: continuous_intros continuous_map_compose continuous_map_id [unfolded id_def])
+      done
+  then show ?thesis
+    by (metis path_component_of_equiv path_connected_space_iff_path_component)
+  qed
+  show ?thesis
+    using assms False by (auto simp: contractible_space homotopic_with_def *)
+qed (simp add: path_connected_space_topspace_empty)
+
+lemma contractible_imp_connected_space:
+   "contractible_space X \<Longrightarrow> connected_space X"
+  by (simp add: contractible_imp_path_connected_space path_connected_imp_connected_space)
+
+lemma contractible_space_alt:
+   "contractible_space X \<longleftrightarrow> (\<forall>a \<in> topspace X. homotopic_with (\<lambda>x. True) X X id (\<lambda>x. a))" (is "?lhs = ?rhs")
+proof
+  assume X: ?lhs
+  then obtain a where a: "homotopic_with (\<lambda>x. True) X X id (\<lambda>x. a)"
+    by (auto simp: contractible_space_def)
+  show ?rhs
+  proof
+    show "homotopic_with (\<lambda>x. True) X X id (\<lambda>x. b)" if "b \<in> topspace X" for b
+      apply (rule homotopic_with_trans [OF a])
+      using homotopic_constant_maps path_connected_space_imp_path_component_of
+      by (metis (full_types) X a continuous_map_const contractible_imp_path_connected_space homotopic_with_imp_continuous_maps that)
+  qed
+next
+  assume R: ?rhs
+  then show ?lhs
+    apply (simp add: contractible_space_def)
+    by (metis equals0I homotopic_on_emptyI)
+qed
+
+
+lemma compose_const [simp]: "f \<circ> (\<lambda>x. a) = (\<lambda>x. f a)" "(\<lambda>x. a) \<circ> g = (\<lambda>x. a)"
+  by (simp_all add: o_def)
+
+lemma nullhomotopic_through_contractible_space:
+  assumes f: "continuous_map X Y f" and g: "continuous_map Y Z g" and Y: "contractible_space Y"
+  obtains c where "homotopic_with (\<lambda>h. True) X Z (g \<circ> f) (\<lambda>x. c)"
+proof -
+  obtain b where b: "homotopic_with (\<lambda>x. True) Y Y id (\<lambda>x. b)"
+    using Y by (auto simp: contractible_space_def)
+  show thesis
+    using homotopic_compose_continuous_map_right
+           [OF homotopic_compose_continuous_map_left [OF b g] f]
+    by (simp add: that)
 qed
 
+lemma nullhomotopic_into_contractible_space:
+  assumes f: "continuous_map X Y f" and Y: "contractible_space Y"
+  obtains c where "homotopic_with (\<lambda>h. True) X Y f (\<lambda>x. c)"
+  using nullhomotopic_through_contractible_space [OF f _ Y]
+  by (metis continuous_map_id id_comp)
+
+lemma nullhomotopic_from_contractible_space:
+  assumes f: "continuous_map X Y f" and X: "contractible_space X"
+  obtains c where "homotopic_with (\<lambda>h. True) X Y f (\<lambda>x. c)"
+  using nullhomotopic_through_contractible_space [OF _ f X]
+  by (metis comp_id continuous_map_id)
+
+lemma homotopy_dominated_contractibility:
+  assumes f: "continuous_map X Y f" and g: "continuous_map Y X g"
+    and hom: "homotopic_with (\<lambda>x. True) Y Y (f \<circ> g) id" and X: "contractible_space X"
+  shows "contractible_space Y"
+proof -
+  obtain c where c: "homotopic_with (\<lambda>h. True) X Y f (\<lambda>x. c)"
+    using nullhomotopic_from_contractible_space [OF f X] .
+  have "homotopic_with (\<lambda>x. True) Y Y (f \<circ> g) (\<lambda>x. c)"
+    using homotopic_compose_continuous_map_right [OF c g] by fastforce
+  then have "homotopic_with (\<lambda>x. True) Y Y id (\<lambda>x. c)"
+    using homotopic_with_trans [OF _ hom] homotopic_with_symD by blast
+  then show ?thesis
+    unfolding contractible_space_def ..
+qed
+
+lemma homotopy_equivalent_space_contractibility:
+   "X homotopy_equivalent_space Y \<Longrightarrow> (contractible_space X \<longleftrightarrow> contractible_space Y)"
+  unfolding homotopy_equivalent_space_def
+  by (blast intro: homotopy_dominated_contractibility)
+
+lemma homeomorphic_space_contractibility:
+   "X homeomorphic_space Y
+        \<Longrightarrow> (contractible_space X \<longleftrightarrow> contractible_space Y)"
+  by (simp add: homeomorphic_imp_homotopy_equivalent_space homotopy_equivalent_space_contractibility)
+
+lemma contractible_eq_homotopy_equivalent_singleton_subtopology:
+   "contractible_space X \<longleftrightarrow>
+        topspace X = {} \<or> (\<exists>a \<in> topspace X. X homotopy_equivalent_space (subtopology X {a}))"(is "?lhs = ?rhs")
+proof (cases "topspace X = {}")
+  case False
+  show ?thesis
+  proof
+    assume ?lhs
+    then obtain a where a: "homotopic_with (\<lambda>x. True) X X id (\<lambda>x. a)"
+      by (auto simp: contractible_space_def)
+    then have "a \<in> topspace X"
+      by (metis False continuous_map_const homotopic_with_imp_continuous_maps)
+    then have "X homotopy_equivalent_space subtopology X {a}"
+      unfolding homotopy_equivalent_space_def
+      apply (rule_tac x="\<lambda>x. a" in exI)
+      apply (rule_tac x=id in exI)
+      apply (auto simp: homotopic_with_sym topspace_subtopology_subset a)
+      using connectedin_absolute connectedin_sing contractible_space_alt contractible_space_subtopology_singleton by fastforce
+    with \<open>a \<in> topspace X\<close> show ?rhs
+      by blast
+  next
+    assume ?rhs
+    then show ?lhs
+      by (meson False contractible_space_subtopology_singleton homotopy_equivalent_space_contractibility)
+  qed
+qed (simp add: contractible_space_empty)
+
+lemma contractible_space_retraction_map_image:
+  assumes "retraction_map X Y f" and X: "contractible_space X"
+  shows "contractible_space Y"
+proof -
+  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"
+    using assms by (auto simp: retraction_map_def retraction_maps_def)
+  obtain a where a: "homotopic_with (\<lambda>x. True) X X id (\<lambda>x. a)"
+    using X by (auto simp: contractible_space_def)
+  have "homotopic_with (\<lambda>x. True) Y Y id (\<lambda>x. f a)"
+  proof (rule homotopic_with_eq)
+    show "homotopic_with (\<lambda>x. True) Y Y (f \<circ> id \<circ> g) (f \<circ> (\<lambda>x. a) \<circ> g)"
+      using f g a homotopic_compose_continuous_map_left homotopic_compose_continuous_map_right by metis
+  qed (use fg in auto)
+  then show ?thesis
+    unfolding contractible_space_def by blast
+qed
+
+lemma contractible_space_prod_topology:
+   "contractible_space(prod_topology X Y) \<longleftrightarrow>
+    topspace X = {} \<or> topspace Y = {} \<or> contractible_space X \<and> contractible_space Y"
+proof (cases "topspace X = {} \<or> topspace Y = {}")
+  case True
+  then have "topspace (prod_topology X Y) = {}"
+    by simp
+  then show ?thesis
+    by (auto simp: contractible_space_empty)
+next
+  case False
+  have "contractible_space(prod_topology X Y) \<longleftrightarrow> contractible_space X \<and> contractible_space Y"
+  proof safe
+    assume XY: "contractible_space (prod_topology X Y)"
+    with False have "retraction_map (prod_topology X Y) X fst"
+      by (auto simp: contractible_space False retraction_map_fst)
+    then show "contractible_space X"
+      by (rule contractible_space_retraction_map_image [OF _ XY])
+    have "retraction_map (prod_topology X Y) Y snd"
+      using False XY  by (auto simp: contractible_space False retraction_map_snd)
+    then show "contractible_space Y"
+      by (rule contractible_space_retraction_map_image [OF _ XY])
+  next
+    assume "contractible_space X" and "contractible_space Y"
+    with False obtain a b
+      where "a \<in> topspace X" and a: "homotopic_with (\<lambda>x. True) X X id (\<lambda>x. a)"
+        and "b \<in> topspace Y" and b: "homotopic_with (\<lambda>x. True) Y Y id (\<lambda>x. b)"
+      by (auto simp: contractible_space)
+    with False show "contractible_space (prod_topology X Y)"
+      apply (simp add: contractible_space)
+      apply (rule_tac x=a in bexI)
+       apply (rule_tac x=b in bexI)
+      using homotopic_with_prod_topology [OF a b]
+    	  apply (metis (no_types, lifting) case_prod_Pair case_prod_beta' eq_id_iff)
+    	 apply auto
+    	done
+  qed
+  with False show ?thesis
+    by auto
+qed
+
+
+
+
+lemma contractible_space_product_topology:
+  "contractible_space(product_topology X I) \<longleftrightarrow>
+    topspace (product_topology X I) = {} \<or> (\<forall>i \<in> I. contractible_space(X i))"
+proof (cases "topspace (product_topology X I) = {}")
+  case False
+  have 1: "contractible_space (X i)"
+    if XI: "contractible_space (product_topology X I)" and "i \<in> I"
+    for i
+  proof (rule contractible_space_retraction_map_image [OF _ XI])
+    show "retraction_map (product_topology X I) (X i) (\<lambda>x. x i)"
+      using False by (simp add: retraction_map_product_projection \<open>i \<in> I\<close>)
+  qed
+  have 2: "contractible_space (product_topology X I)"
+    if "x \<in> topspace (product_topology X I)" and cs: "\<forall>i\<in>I. contractible_space (X i)"
+    for x :: "'a \<Rightarrow> 'b"
+  proof -
+    obtain f where f: "\<And>i. i\<in>I \<Longrightarrow> homotopic_with (\<lambda>x. True) (X i) (X i) id (\<lambda>x. f i)"
+      using cs unfolding contractible_space_def by metis
+    have "homotopic_with (\<lambda>x. True)
+                         (product_topology X I) (product_topology X I) id (\<lambda>x. restrict f I)"
+      by (rule homotopic_with_eq [OF homotopic_with_product_topology [OF f]]) (auto simp: topspace_product_topology)
+    then show ?thesis
+      by (auto simp: contractible_space_def)
+  qed
+  show ?thesis
+    using False 1 2 by blast
+qed (simp add: contractible_space_empty)
+
+
+lemma contractible_space_subtopology_euclideanreal [simp]:
+  "contractible_space(subtopology euclideanreal S) \<longleftrightarrow> is_interval S"
+  (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then have "path_connectedin (subtopology euclideanreal S) S"
+    using contractible_imp_path_connected_space path_connectedin_topspace path_connectedin_absolute
+    by (simp add: contractible_imp_path_connected) 
+  then show ?rhs
+    by (simp add: is_interval_path_connected_1)
+next
+  assume ?rhs
+  then have "convex S"
+    by (simp add: is_interval_convex_1)
+  show ?lhs
+  proof (cases "S = {}")
+    case False
+    then obtain z where "z \<in> S"
+      by blast
+    show ?thesis
+      unfolding contractible_space_def homotopic_with_def
+    proof (intro exI conjI allI)
+      show "continuous_map (prod_topology (top_of_set {0..1}) (top_of_set S)) (top_of_set S)
+                           (\<lambda>(t,x). (1 - t) * x + t * z)"
+        apply (auto simp: case_prod_unfold)
+         apply (intro continuous_intros)
+        using  \<open>z \<in> S\<close> apply (auto intro: convexD [OF \<open>convex S\<close>, simplified])
+        done
+    qed auto
+  qed (simp add: contractible_space_empty)
+qed
+
+
+corollary contractible_space_euclideanreal: "contractible_space euclideanreal"
+proof -
+  have "contractible_space (subtopology euclideanreal UNIV)"
+    using contractible_space_subtopology_euclideanreal by blast
+  then show ?thesis
+    by simp
+qed
+
+
+abbreviation%important homotopy_eqv :: "'a::topological_space set \<Rightarrow> 'b::topological_space set \<Rightarrow> bool"
+             (infix "homotopy'_eqv" 50)
+  where "S homotopy_eqv T \<equiv> top_of_set S homotopy_equivalent_space top_of_set T"
+
+
+
+
+
+lemma homeomorphic_imp_homotopy_eqv: "S homeomorphic T \<Longrightarrow> S homotopy_eqv T"
+  unfolding homeomorphic_def homeomorphism_def homotopy_equivalent_space_def
+  apply (erule ex_forward)+
+  apply auto
+   apply (metis homotopic_with_id2 topspace_euclidean_subtopology)
+  by (metis (full_types) homotopic_with_id2 imageE topspace_euclidean_subtopology)
+
+
 lemma homotopy_eqv_inj_linear_image:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "linear f" "inj f"
@@ -3436,33 +3935,33 @@
       and g: "continuous_on U g" "g ` U \<subseteq> T"
       and homUS: "\<And>f g. \<lbrakk>continuous_on U f; f ` U \<subseteq> S;
                          continuous_on U g; g ` U \<subseteq> S\<rbrakk>
-                         \<Longrightarrow> homotopic_with (\<lambda>x. True) U S f g"
-    shows "homotopic_with (\<lambda>x. True) U T f g"
+                         \<Longrightarrow> homotopic_with_canon (\<lambda>x. True) U S f g"
+    shows "homotopic_with_canon (\<lambda>x. True) U T f g"
 proof -
   obtain h k where h: "continuous_on S h" "h ` S \<subseteq> T"
                and k: "continuous_on T k" "k ` T \<subseteq> S"
-               and hom: "homotopic_with (\<lambda>x. True) S S (k \<circ> h) id"
-                        "homotopic_with (\<lambda>x. True) T T (h \<circ> k) id"
-    using assms by (auto simp: homotopy_eqv_def)
-  have "homotopic_with (\<lambda>f. True) U S (k \<circ> f) (k \<circ> g)"
+               and hom: "homotopic_with_canon (\<lambda>x. True) S S (k \<circ> h) id"
+                        "homotopic_with_canon (\<lambda>x. True) T T (h \<circ> k) id"
+    using assms by (auto simp: homotopy_equivalent_space_def)
+  have "homotopic_with_canon (\<lambda>f. True) U S (k \<circ> f) (k \<circ> g)"
     apply (rule homUS)
     using f g k
     apply (safe intro!: continuous_on_compose h k f elim!: continuous_on_subset)
     apply (force simp: o_def)+
     done
-  then have "homotopic_with (\<lambda>x. True) U T (h \<circ> (k \<circ> f)) (h \<circ> (k \<circ> g))"
+  then have "homotopic_with_canon (\<lambda>x. True) U T (h \<circ> (k \<circ> f)) (h \<circ> (k \<circ> g))"
     apply (rule homotopic_with_compose_continuous_left)
     apply (simp_all add: h)
     done
-  moreover have "homotopic_with (\<lambda>x. True) U T (h \<circ> k \<circ> f) (id \<circ> f)"
+  moreover have "homotopic_with_canon (\<lambda>x. True) U T (h \<circ> k \<circ> f) (id \<circ> f)"
     apply (rule homotopic_with_compose_continuous_right [where X=T and Y=T])
     apply (auto simp: hom f)
     done
-  moreover have "homotopic_with (\<lambda>x. True) U T (h \<circ> k \<circ> g) (id \<circ> g)"
+  moreover have "homotopic_with_canon (\<lambda>x. True) U T (h \<circ> k \<circ> g) (id \<circ> g)"
     apply (rule homotopic_with_compose_continuous_right [where X=T and Y=T])
     apply (auto simp: hom g)
     done
-  ultimately show "homotopic_with (\<lambda>x. True) U T f g"
+  ultimately show "homotopic_with_canon (\<lambda>x. True) U T f g"
     apply (simp add: o_assoc)
     using homotopic_with_trans homotopic_with_sym by blast
 qed
@@ -3474,13 +3973,24 @@
   assumes "S homotopy_eqv T"
     shows "(\<forall>f g. continuous_on U f \<and> f ` U \<subseteq> S \<and>
                    continuous_on U g \<and> g ` U \<subseteq> S
-                   \<longrightarrow> homotopic_with (\<lambda>x. True) U S f g) \<longleftrightarrow>
+                   \<longrightarrow> homotopic_with_canon (\<lambda>x. True) U S f g) \<longleftrightarrow>
            (\<forall>f g. continuous_on U f \<and> f ` U \<subseteq> T \<and>
                   continuous_on U g \<and> g ` U \<subseteq> T
-                  \<longrightarrow> homotopic_with (\<lambda>x. True) U T f g)"
-apply (rule iffI)
-apply (metis assms homotopy_eqv_homotopic_triviality_imp)
-by (metis (no_types) assms homotopy_eqv_homotopic_triviality_imp homotopy_eqv_sym)
+                  \<longrightarrow> homotopic_with_canon (\<lambda>x. True) U T f g)"
+      (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then show ?rhs
+    by (metis assms homotopy_eqv_homotopic_triviality_imp)
+next
+  assume ?rhs
+  moreover
+  have "T homotopy_eqv S"
+    using assms homotopy_equivalent_space_sym by blast
+  ultimately show ?lhs
+    by (blast intro: homotopy_eqv_homotopic_triviality_imp)
+qed
+
 
 lemma homotopy_eqv_cohomotopic_triviality_null_imp:
   fixes S :: "'a::real_normed_vector set"
@@ -3489,23 +3999,23 @@
   assumes "S homotopy_eqv T"
       and f: "continuous_on T f" "f ` T \<subseteq> U"
       and homSU: "\<And>f. \<lbrakk>continuous_on S f; f ` S \<subseteq> U\<rbrakk>
-                      \<Longrightarrow> \<exists>c. homotopic_with (\<lambda>x. True) S U f (\<lambda>x. c)"
-  obtains c where "homotopic_with (\<lambda>x. True) T U f (\<lambda>x. c)"
+                      \<Longrightarrow> \<exists>c. homotopic_with_canon (\<lambda>x. True) S U f (\<lambda>x. c)"
+  obtains c where "homotopic_with_canon (\<lambda>x. True) T U f (\<lambda>x. c)"
 proof -
   obtain h k where h: "continuous_on S h" "h ` S \<subseteq> T"
                and k: "continuous_on T k" "k ` T \<subseteq> S"
-               and hom: "homotopic_with (\<lambda>x. True) S S (k \<circ> h) id"
-                        "homotopic_with (\<lambda>x. True) T T (h \<circ> k) id"
-    using assms by (auto simp: homotopy_eqv_def)
-  obtain c where "homotopic_with (\<lambda>x. True) S U (f \<circ> h) (\<lambda>x. c)"
+               and hom: "homotopic_with_canon (\<lambda>x. True) S S (k \<circ> h) id"
+                        "homotopic_with_canon (\<lambda>x. True) T T (h \<circ> k) id"
+    using assms by (auto simp: homotopy_equivalent_space_def)
+  obtain c where "homotopic_with_canon (\<lambda>x. True) S U (f \<circ> h) (\<lambda>x. c)"
     apply (rule exE [OF homSU [of "f \<circ> h"]])
     apply (intro continuous_on_compose h)
     using h f  apply (force elim!: continuous_on_subset)+
     done
-  then have "homotopic_with (\<lambda>x. True) T U ((f \<circ> h) \<circ> k) ((\<lambda>x. c) \<circ> k)"
+  then have "homotopic_with_canon (\<lambda>x. True) T U ((f \<circ> h) \<circ> k) ((\<lambda>x. c) \<circ> k)"
     apply (rule homotopic_with_compose_continuous_right [where X=S])
     using k by auto
-  moreover have "homotopic_with (\<lambda>x. True) T U (f \<circ> id) (f \<circ> (h \<circ> k))"
+  moreover have "homotopic_with_canon (\<lambda>x. True) T U (f \<circ> id) (f \<circ> (h \<circ> k))"
     apply (rule homotopic_with_compose_continuous_left [where Y=T])
       apply (simp add: hom homotopic_with_symD)
      using f apply auto
@@ -3522,12 +4032,12 @@
     and U :: "'c::real_normed_vector set"
   assumes "S homotopy_eqv T"
     shows "(\<forall>f. continuous_on S f \<and> f ` S \<subseteq> U
-                \<longrightarrow> (\<exists>c. homotopic_with (\<lambda>x. True) S U f (\<lambda>x. c))) \<longleftrightarrow>
+                \<longrightarrow> (\<exists>c. homotopic_with_canon (\<lambda>x. True) S U f (\<lambda>x. c))) \<longleftrightarrow>
            (\<forall>f. continuous_on T f \<and> f ` T \<subseteq> U
-                \<longrightarrow> (\<exists>c. homotopic_with (\<lambda>x. True) T U f (\<lambda>x. c)))"
+                \<longrightarrow> (\<exists>c. homotopic_with_canon (\<lambda>x. True) T U f (\<lambda>x. c)))"
 apply (rule iffI)
 apply (metis assms homotopy_eqv_cohomotopic_triviality_null_imp)
-by (metis assms homotopy_eqv_cohomotopic_triviality_null_imp homotopy_eqv_sym)
+by (metis assms homotopy_eqv_cohomotopic_triviality_null_imp homotopy_equivalent_space_sym)
 
 lemma homotopy_eqv_homotopic_triviality_null_imp:
   fixes S :: "'a::real_normed_vector set"
@@ -3536,23 +4046,23 @@
   assumes "S homotopy_eqv T"
       and f: "continuous_on U f" "f ` U \<subseteq> T"
       and homSU: "\<And>f. \<lbrakk>continuous_on U f; f ` U \<subseteq> S\<rbrakk>
-                      \<Longrightarrow> \<exists>c. homotopic_with (\<lambda>x. True) U S f (\<lambda>x. c)"
-    shows "\<exists>c. homotopic_with (\<lambda>x. True) U T f (\<lambda>x. c)"
+                      \<Longrightarrow> \<exists>c. homotopic_with_canon (\<lambda>x. True) U S f (\<lambda>x. c)"
+    shows "\<exists>c. homotopic_with_canon (\<lambda>x. True) U T f (\<lambda>x. c)"
 proof -
   obtain h k where h: "continuous_on S h" "h ` S \<subseteq> T"
                and k: "continuous_on T k" "k ` T \<subseteq> S"
-               and hom: "homotopic_with (\<lambda>x. True) S S (k \<circ> h) id"
-                        "homotopic_with (\<lambda>x. True) T T (h \<circ> k) id"
-    using assms by (auto simp: homotopy_eqv_def)
-  obtain c::'a where "homotopic_with (\<lambda>x. True) U S (k \<circ> f) (\<lambda>x. c)"
+               and hom: "homotopic_with_canon (\<lambda>x. True) S S (k \<circ> h) id"
+                        "homotopic_with_canon (\<lambda>x. True) T T (h \<circ> k) id"
+    using assms by (auto simp: homotopy_equivalent_space_def)
+  obtain c::'a where "homotopic_with_canon (\<lambda>x. True) U S (k \<circ> f) (\<lambda>x. c)"
     apply (rule exE [OF homSU [of "k \<circ> f"]])
     apply (intro continuous_on_compose h)
     using k f  apply (force elim!: continuous_on_subset)+
     done
-  then have "homotopic_with (\<lambda>x. True) U T (h \<circ> (k \<circ> f)) (h \<circ> (\<lambda>x. c))"
+  then have "homotopic_with_canon (\<lambda>x. True) U T (h \<circ> (k \<circ> f)) (h \<circ> (\<lambda>x. c))"
     apply (rule homotopic_with_compose_continuous_left [where Y=S])
     using h by auto
-  moreover have "homotopic_with (\<lambda>x. True) U T (id \<circ> f) ((h \<circ> k) \<circ> f)"
+  moreover have "homotopic_with_canon (\<lambda>x. True) U T (id \<circ> f) ((h \<circ> k) \<circ> f)"
     apply (rule homotopic_with_compose_continuous_right [where X=T])
       apply (simp add: hom homotopic_with_symD)
      using f apply auto
@@ -3567,12 +4077,12 @@
     and U :: "'c::real_normed_vector set"
   assumes "S homotopy_eqv T"
     shows "(\<forall>f. continuous_on U f \<and> f ` U \<subseteq> S
-                  \<longrightarrow> (\<exists>c. homotopic_with (\<lambda>x. True) U S f (\<lambda>x. c))) \<longleftrightarrow>
+                  \<longrightarrow> (\<exists>c. homotopic_with_canon (\<lambda>x. True) U S f (\<lambda>x. c))) \<longleftrightarrow>
            (\<forall>f. continuous_on U f \<and> f ` U \<subseteq> T
-                  \<longrightarrow> (\<exists>c. homotopic_with (\<lambda>x. True) U T f (\<lambda>x. c)))"
+                  \<longrightarrow> (\<exists>c. homotopic_with_canon (\<lambda>x. True) U T f (\<lambda>x. c)))"
 apply (rule iffI)
 apply (metis assms homotopy_eqv_homotopic_triviality_null_imp)
-by (metis assms homotopy_eqv_homotopic_triviality_null_imp homotopy_eqv_sym)
+by (metis assms homotopy_eqv_homotopic_triviality_null_imp homotopy_equivalent_space_sym)
 
 lemma homotopy_eqv_contractible_sets:
   fixes S :: "'a::real_normed_vector set"
@@ -3587,7 +4097,7 @@
   with assms obtain a b where "a \<in> S" "b \<in> T"
     by auto
   then show ?thesis
-    unfolding homotopy_eqv_def
+    unfolding homotopy_equivalent_space_def
     apply (rule_tac x="\<lambda>x. b" in exI)
     apply (rule_tac x="\<lambda>x. a" in exI)
     apply (intro assms conjI continuous_on_id' homotopic_into_contractible)
@@ -3598,20 +4108,19 @@
 lemma homotopy_eqv_empty1 [simp]:
   fixes S :: "'a::real_normed_vector set"
   shows "S homotopy_eqv ({}::'b::real_normed_vector set) \<longleftrightarrow> S = {}"
-apply (rule iffI)
-using homotopy_eqv_def apply fastforce
-by (simp add: homotopy_eqv_contractible_sets)
+  apply (rule iffI)
+   apply (metis Abstract_Topology.continuous_map_subtopology_eu emptyE equals0I homotopy_equivalent_space_def image_subset_iff)
+  by (simp add: homotopy_eqv_contractible_sets)
 
 lemma homotopy_eqv_empty2 [simp]:
   fixes S :: "'a::real_normed_vector set"
   shows "({}::'b::real_normed_vector set) homotopy_eqv S \<longleftrightarrow> S = {}"
-by (metis homotopy_eqv_empty1 homotopy_eqv_sym)
+  using homotopy_equivalent_space_sym homotopy_eqv_empty1 by blast
 
 lemma homotopy_eqv_contractibility:
   fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set"
   shows "S homotopy_eqv T \<Longrightarrow> (contractible S \<longleftrightarrow> contractible T)"
-unfolding homotopy_eqv_def
-by (blast intro: homotopy_dominated_contractibility)
+  by (meson contractible_space_top_of_set homotopy_equivalent_space_contractibility)
 
 lemma homotopy_eqv_sing:
   fixes S :: "'a::real_normed_vector set" and a :: "'b::real_normed_vector"
@@ -5034,11 +5543,15 @@
 
 proposition nullhomotopic_from_sphere_extension:
   fixes f :: "'M::euclidean_space \<Rightarrow> 'a::real_normed_vector"
-  shows  "(\<exists>c. homotopic_with (\<lambda>x. True) (sphere a r) S f (\<lambda>x. c)) \<longleftrightarrow>
+  shows  "(\<exists>c. homotopic_with_canon (\<lambda>x. True) (sphere a r) S f (\<lambda>x. c)) \<longleftrightarrow>
           (\<exists>g. continuous_on (cball a r) g \<and> g ` (cball a r) \<subseteq> S \<and>
                (\<forall>x \<in> sphere a r. g x = f x))"
          (is "?lhs = ?rhs")
 proof (cases r "0::real" rule: linorder_cases)
+  case less
+  then show ?thesis
+    by (simp add: homotopic_on_emptyI)
+next
   case equal
   then show ?thesis
     apply (auto simp: homotopic_with)
@@ -5051,9 +5564,11 @@
   have ?P if ?lhs using that
   proof
     fix c
-    assume c: "homotopic_with (\<lambda>x. True) (sphere a r) S f (\<lambda>x. c)"
-    then have contf: "continuous_on (sphere a r) f" and fim: "f ` sphere a r \<subseteq> S"
-      by (auto simp: homotopic_with_imp_subset1 homotopic_with_imp_continuous)
+    assume c: "homotopic_with_canon (\<lambda>x. True) (sphere a r) S f (\<lambda>x. c)"
+    then have contf: "continuous_on (sphere a r) f" 
+      by (metis homotopic_with_imp_continuous)
+    moreover have fim: "f ` sphere a r \<subseteq> S"
+      by (meson continuous_map_subtopology_eu c homotopic_with_imp_continuous_maps)
     show ?P
       using contf fim by (auto simp: sphere_def dist_norm norm_minus_commute)
   qed
@@ -5070,7 +5585,7 @@
   moreover have ?thesis if ?P
   proof
     assume ?lhs
-    then obtain c where "homotopic_with (\<lambda>x. True) (sphere a r) S (\<lambda>x. c) f"
+    then obtain c where "homotopic_with_canon (\<lambda>x. True) (sphere a r) S (\<lambda>x. c) f"
       using homotopic_with_sym by blast
     then obtain h where conth: "continuous_on ({0..1::real} \<times> sphere a r) h"
                     and him: "h ` ({0..1} \<times> sphere a r) \<subseteq> S"
@@ -5159,6 +5674,6 @@
   qed
   ultimately
   show ?thesis by meson
-qed simp
+qed 
 
 end
\ No newline at end of file
diff -r 8e916ed23d17 -r e7648f104d6b src/HOL/Analysis/Jordan_Curve.thy
--- a/src/HOL/Analysis/Jordan_Curve.thy	Tue Mar 26 16:27:29 2019 +0100
+++ b/src/HOL/Analysis/Jordan_Curve.thy	Tue Mar 26 17:01:55 2019 +0000
@@ -103,7 +103,7 @@
         using z by fastforce
     qed (auto simp: g h algebra_simps exp_add)
   qed
-  ultimately have *: "homotopic_with (\<lambda>x. True) (S \<union> T) (sphere 0 1)
+  ultimately have *: "homotopic_with_canon (\<lambda>x. True) (S \<union> T) (sphere 0 1)
                           (\<lambda>x. (x - a) /\<^sub>R cmod (x - a))  (\<lambda>x. (x - b) /\<^sub>R cmod (x - b))"
     by (subst homotopic_circlemaps_divide) (auto simp: inessential_eq_continuous_logarithm_circle)
   show ?thesis
diff -r 8e916ed23d17 -r e7648f104d6b src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Tue Mar 26 16:27:29 2019 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy	Tue Mar 26 17:01:55 2019 +0000
@@ -1976,6 +1976,13 @@
 definition path_components_of :: "'a topology \<Rightarrow> 'a set set"
   where "path_components_of X \<equiv> path_component_of_set X ` topspace X"
 
+lemma pathin_canon_iff: "pathin (top_of_set T) g \<longleftrightarrow> path g \<and> g ` {0..1} \<subseteq> T"
+  by (simp add: path_def pathin_def)
+
+lemma path_component_of_canon_iff [simp]:
+  "path_component_of (top_of_set T) a b \<longleftrightarrow> path_component T a b"
+  by (simp add: path_component_of_def pathin_canon_iff path_defs)
+
 lemma path_component_in_topspace:
    "path_component_of X x y \<Longrightarrow> x \<in> topspace X \<and> y \<in> topspace X"
   by (auto simp: path_component_of_def pathin_def continuous_map_def)
@@ -2028,13 +2035,11 @@
   qed (auto simp: g1 g2)
 qed
 
-
 lemma path_component_of_mono:
    "\<lbrakk>path_component_of (subtopology X S) x y; S \<subseteq> T\<rbrakk> \<Longrightarrow> path_component_of (subtopology X T) x y"
   unfolding path_component_of_def
   by (metis subsetD pathin_subtopology)
 
-
 lemma path_component_of:
   "path_component_of X x y \<longleftrightarrow> (\<exists>T. path_connectedin X T \<and> x \<in> T \<and> y \<in> T)"
   apply (auto simp: path_component_of_def)
diff -r 8e916ed23d17 -r e7648f104d6b src/HOL/Analysis/Product_Topology.thy
--- a/src/HOL/Analysis/Product_Topology.thy	Tue Mar 26 16:27:29 2019 +0100
+++ b/src/HOL/Analysis/Product_Topology.thy	Tue Mar 26 17:01:55 2019 +0000
@@ -80,13 +80,6 @@
   "prod_topology (subtopology euclidean S) (subtopology euclidean T) = subtopology euclidean (S \<times> T)"
   by (simp add: prod_topology_subtopology subtopology_subtopology Times_Int_Times)
 
-lemma continuous_map_subtopology_eu [simp]:
-  "continuous_map (subtopology euclidean S) (subtopology euclidean T) h \<longleftrightarrow> continuous_on S h \<and> h ` S \<subseteq> T"
-  apply safe
-  apply (metis continuous_map_closedin_preimage_eq continuous_map_in_subtopology continuous_on_closed order_refl topspace_euclidean_subtopology)
-  apply (simp add: continuous_map_closedin_preimage_eq image_subset_iff)
-  by (metis (no_types, hide_lams) continuous_map_closedin_preimage_eq continuous_map_in_subtopology continuous_on_closed order_refl topspace_euclidean_subtopology)
-
 lemma openin_prod_topology_alt:
      "openin (prod_topology X Y) S \<longleftrightarrow>
       (\<forall>x y. (x,y) \<in> S \<longrightarrow> (\<exists>U V. openin X U \<and> openin Y V \<and> x \<in> U \<and> y \<in> V \<and> U \<times> V \<subseteq> S))"
@@ -101,7 +94,7 @@
   unfolding open_map_def openin_prod_topology_alt
   by (force simp: openin_subopen [of Y "snd ` _"] intro: subset_snd_imageI)
 
-lemma openin_Times:
+lemma openin_prod_Times_iff:
      "openin (prod_topology X Y) (S \<times> T) \<longleftrightarrow> S = {} \<or> T = {} \<or> openin X S \<and> openin Y T"
 proof (cases "S = {} \<or> T = {}")
   case False
@@ -121,7 +114,7 @@
     by (clarsimp simp: closure_of_def openin_prod_topology_alt) (meson SigmaI subsetD)
 qed
 
-lemma closedin_Times:
+lemma closedin_prod_Times_iff:
    "closedin (prod_topology X Y) (S \<times> T) \<longleftrightarrow> S = {} \<or> T = {} \<or> closedin X S \<and> closedin Y T"
   by (auto simp: closure_of_Times times_eq_iff simp flip: closure_of_eq)
 
@@ -130,7 +123,7 @@
   show "(X interior_of S) \<times> Y interior_of T \<subseteq> S \<times> T"
     by (simp add: Sigma_mono interior_of_subset)
   show "openin (prod_topology X Y) ((X interior_of S) \<times> Y interior_of T)"
-    by (simp add: openin_Times)
+    by (simp add: openin_prod_Times_iff)
 next
   show "T' \<subseteq> (X interior_of S) \<times> Y interior_of T" if "T' \<subseteq> S \<times> T" "openin (prod_topology X Y) T'" for T'
   proof (clarsimp; intro conjI)
@@ -165,7 +158,7 @@
         unfolding continuous_map_def using True that
         apply clarify
         apply (drule_tac x="U \<times> topspace Y" in spec)
-        by (simp add: openin_Times mem_Times_iff cong: conj_cong)
+        by (simp add: openin_prod_Times_iff mem_Times_iff cong: conj_cong)
       with True show "continuous_map Z X (fst \<circ> f)"
         by (auto simp: continuous_map_def)
     next
@@ -174,7 +167,7 @@
         unfolding continuous_map_def using True that
         apply clarify
         apply (drule_tac x="topspace X \<times> V" in spec)
-        by (simp add: openin_Times mem_Times_iff cong: conj_cong)
+        by (simp add: openin_prod_Times_iff mem_Times_iff cong: conj_cong)
       with True show "continuous_map Z Y (snd \<circ> f)"
         by (auto simp: continuous_map_def)
     next
diff -r 8e916ed23d17 -r e7648f104d6b src/HOL/Analysis/T1_Spaces.thy
--- a/src/HOL/Analysis/T1_Spaces.thy	Tue Mar 26 16:27:29 2019 +0100
+++ b/src/HOL/Analysis/T1_Spaces.thy	Tue Mar 26 17:01:55 2019 +0000
@@ -209,7 +209,7 @@
     by simp
   have "t1_space (prod_topology X Y) \<longleftrightarrow> (t1_space X \<and> t1_space Y)"
     using False
-    by (force simp: t1_space_closedin_singleton closedin_Times eq simp del: insert_Times_insert)
+    by (force simp: t1_space_closedin_singleton closedin_prod_Times_iff eq simp del: insert_Times_insert)
   with False show ?thesis
     by simp
 qed
diff -r 8e916ed23d17 -r e7648f104d6b src/HOL/Analysis/Winding_Numbers.thy
--- a/src/HOL/Analysis/Winding_Numbers.thy	Tue Mar 26 16:27:29 2019 +0100
+++ b/src/HOL/Analysis/Winding_Numbers.thy	Tue Mar 26 17:01:55 2019 +0000
@@ -1137,23 +1137,25 @@
              and qeq:  "pathfinish q - pathstart q = 2 * of_real pi * \<i> * winding_number p \<zeta>"
              and peq: "\<And>t. t \<in> {0..1} \<Longrightarrow> p t = \<zeta> + exp(q t)"
     using winding_number_as_continuous_log [OF assms] by blast
-  have *: "homotopic_with (\<lambda>r. pathfinish r = pathstart r)
+  have *: "homotopic_with_canon (\<lambda>r. pathfinish r = pathstart r)
                        {0..1} (-{\<zeta>}) ((\<lambda>w. \<zeta> + exp w) \<circ> q) ((\<lambda>w. \<zeta> + exp w) \<circ> (\<lambda>t. 0))"
   proof (rule homotopic_with_compose_continuous_left)
-    show "homotopic_with (\<lambda>f. pathfinish ((\<lambda>w. \<zeta> + exp w) \<circ> f) = pathstart ((\<lambda>w. \<zeta> + exp w) \<circ> f))
+    show "homotopic_with_canon (\<lambda>f. pathfinish ((\<lambda>w. \<zeta> + exp w) \<circ> f) = pathstart ((\<lambda>w. \<zeta> + exp w) \<circ> f))
               {0..1} UNIV q (\<lambda>t. 0)"
     proof (rule homotopic_with_mono, simp_all add: pathfinish_def pathstart_def)
       have "homotopic_loops UNIV q (\<lambda>t. 0)"
-        by (rule homotopic_loops_linear) (use qeq \<open>path q\<close> in \<open>auto simp: continuous_on_const path_defs\<close>)
-      then show "homotopic_with (\<lambda>h. exp (h 1) = exp (h 0)) {0..1} UNIV q (\<lambda>t. 0)"
-        by (simp add: homotopic_loops_def homotopic_with_mono pathfinish_def pathstart_def)
+        by (rule homotopic_loops_linear) (use qeq \<open>path q\<close> in \<open>auto simp: path_defs\<close>)
+      then have "homotopic_with (\<lambda>r. r 1 = r 0) (top_of_set {0..1}) euclidean q (\<lambda>t. 0)"
+        by (simp add: homotopic_loops_def pathfinish_def pathstart_def)
+      then show "homotopic_with (\<lambda>h. exp (h 1) = exp (h 0)) (top_of_set {0..1}) euclidean q (\<lambda>t. 0)"
+        by (rule homotopic_with_mono) simp
     qed
     show "continuous_on UNIV (\<lambda>w. \<zeta> + exp w)"
       by (rule continuous_intros)+
     show "range (\<lambda>w. \<zeta> + exp w) \<subseteq> -{\<zeta>}"
       by auto
   qed
-  then have "homotopic_with (\<lambda>r. pathfinish r = pathstart r) {0..1} (-{\<zeta>}) p (\<lambda>x. \<zeta> + 1)"
+  then have "homotopic_with_canon (\<lambda>r. pathfinish r = pathstart r) {0..1} (-{\<zeta>}) p (\<lambda>x. \<zeta> + 1)"
     by (rule homotopic_with_eq) (auto simp: o_def peq pathfinish_def pathstart_def)
   then have "homotopic_loops (-{\<zeta>}) p (\<lambda>t. \<zeta> + 1)"
     by (simp add: homotopic_loops_def)
diff -r 8e916ed23d17 -r e7648f104d6b src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Tue Mar 26 16:27:29 2019 +0100
+++ b/src/HOL/Complete_Lattices.thy	Tue Mar 26 17:01:55 2019 +0000
@@ -998,6 +998,12 @@
   apply (auto simp: disjnt_def)
   using inj_on_eq_iff by fastforce
 
+lemma disjnt_Union1 [simp]: "disjnt (\<Union>\<A>) B \<longleftrightarrow> (\<forall>A \<in> \<A>. disjnt A B)"
+  by (auto simp: disjnt_def)
+
+lemma disjnt_Union2 [simp]: "disjnt B (\<Union>\<A>) \<longleftrightarrow> (\<forall>A \<in> \<A>. disjnt B A)"
+  by (auto simp: disjnt_def)
+
 
 subsubsection \<open>Unions of families\<close>
 
diff -r 8e916ed23d17 -r e7648f104d6b src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue Mar 26 16:27:29 2019 +0100
+++ b/src/HOL/Set.thy	Tue Mar 26 17:01:55 2019 +0000
@@ -1926,6 +1926,12 @@
 lemma disjnt_subset2 : "\<lbrakk>disjnt X Y; Z \<subseteq> Y\<rbrakk> \<Longrightarrow> disjnt X Z"
   by (auto simp: disjnt_def)
 
+lemma disjnt_Un1 [simp]: "disjnt (A \<union> B) C \<longleftrightarrow> disjnt A C \<and> disjnt B C"
+  by (auto simp: disjnt_def)
+
+lemma disjnt_Un2 [simp]: "disjnt C (A \<union> B) \<longleftrightarrow> disjnt C A \<and> disjnt C B"
+  by (auto simp: disjnt_def)
+
 lemma disjoint_image_subset: "\<lbrakk>pairwise disjnt \<A>; \<And>X. X \<in> \<A> \<Longrightarrow> f X \<subseteq> X\<rbrakk> \<Longrightarrow> pairwise disjnt (f `\<A>)"
   unfolding disjnt_def pairwise_def by fast