diff -r 5e82015fa879 -r f2d327275065 src/HOL/Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Sun Mar 24 20:31:53 2019 +0100
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Tue Mar 26 17:01:36 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