diff --git a/theories/homotopy.v b/theories/homotopy.v
index 0517fa9c2..b99fd7503 100644
--- a/theories/homotopy.v
+++ b/theories/homotopy.v
@@ -577,41 +577,41 @@ Qed.
 Definition equiv_rel_reparametrize := EquivRel reparametrize 
   reflexive_reparametrize symmetric_reparametrize transitive_reparametrize.
 
-Definition Path := {eq_quot equiv_rel_reparametrize}.
+Definition RPath := {eq_quot equiv_rel_reparametrize}.
 
-Definition path_init := lift_fun1 Path (fun f => f 0).
+Definition path_init := lift_fun1 RPath (fun f => f 0).
 
-Lemma path_init_mono : {mono \pi_Path : f / f 0 >-> path_init f}.
+Lemma path_init_mono : {mono \pi_RPath : f / f 0 >-> path_init f}.
 Proof.
 move=> f; unlock path_init.
-have : ((repr (\pi_(Path) f)) = f %[mod Path]) by rewrite reprK.
+have : ((repr (\pi_(RPath) f)) = f %[mod RPath]) by rewrite reprK.
 move=> /eqquotP /asboolP [] gamma /(_ 0).
 by rewrite bound_itvE /= parametrize_init; exact.
 Qed.
 
 Canonical pi_path_init_mono := PiMono1 path_init_mono.
 
-Definition path_final := lift_fun1 Path (fun f => f 1).
+Definition path_final := lift_fun1 RPath (fun f => f 1).
 
-Lemma path_final_mono : {mono \pi_Path : f / f 1 >-> path_final f}.
+Lemma path_final_mono : {mono \pi_RPath : f / f 1 >-> path_final f}.
 Proof.
 move=> f; unlock path_final.
-have : ((repr (\pi_(Path) f)) = f %[mod Path]) by rewrite reprK.
+have : ((repr (\pi_(RPath) f)) = f %[mod RPath]) by rewrite reprK.
 move=> /eqquotP /asboolP [] gamma /(_ 1).
 by rewrite bound_itvE /= parametrize_final; exact.
 Qed.
 
 Canonical pi_path_final_mono := PiMono1 path_final_mono.
 
-Definition path_image := lift_fun1 Path (fun f => f @` `[0,1] ).
+Definition path_image := lift_fun1 RPath (fun f => f @` `[0,1] ).
 
-Lemma path_image_mono : {mono \pi_Path : f / f @` `[0,1] >-> path_image f}.
+Lemma path_image_mono : {mono \pi_RPath : f / f @` `[0,1] >-> path_image f}.
 Proof.
 move=> f; unlock path_image; rewrite eqEsubset; split => z /= [w wI] <-.
-  have /eqquotP/asboolP [gamma fg]: f = repr (\pi_(Path) f) %[mod Path]. 
+  have /eqquotP/asboolP [gamma fg]: f = repr (\pi_(RPath) f) %[mod RPath]. 
     by rewrite reprK.
   by (exists (gamma w); last exact: fg); exact: (@funS _ _ _ _ gamma).
-have /eqquotP/asboolP [gamma fg]: repr (\pi_(Path) f) = f %[mod Path]. 
+have /eqquotP/asboolP [gamma fg]: repr (\pi_(RPath) f) = f %[mod RPath]. 
   by rewrite reprK.
 (exists (gamma w); last exact: fg); exact: (@funS _ _ _ _ gamma).
 Qed.
@@ -620,25 +620,25 @@ Canonical pi_path_image_mono := PiMono1 path_image_mono.
 
 Let cts_fun_rev (f : R -> T) := f \o rev_param.
 
-Definition path_reverse := lift_op1 Path cts_fun_rev.
+Definition path_reverse := lift_op1 RPath cts_fun_rev.
 
 Lemma path_reverse_morph : {morph \pi : f / cts_fun_rev f >-> path_reverse f}.
 Proof.
 move=> f /=; unlock path_reverse; apply/eqquotP/asboolP. 
-have /eqquotP/asboolP [gamma fg]: repr (\pi_(Path) f) = f %[mod Path]. 
+have /eqquotP/asboolP [gamma fg]: repr (\pi_(RPath) f) = f %[mod RPath]. 
   by rewrite reprK.
 exists (double_reverse_inj (inv_parametrization gamma)) => x x01 /=.
 have gx01 : (gamma^-1)%function (rev_param x) \in `[0, 1].
   apply: (@funS _ _ _ _ [fun of inv_parametrization gamma]).
   exact: funS.
-rewrite /cts_fun_rev /= (@rev_param_cancel _ `[0,1]%classic) -?fg ?inE // /Path.
+rewrite /cts_fun_rev /= (@rev_param_cancel _ `[0,1]%classic) -?fg ?inE // /RPath.
   have /= := (@funK _ _ _ (inv_parametrization gamma) (rev_param x)).
 by rewrite invV => -> //=; apply/mem_set; exact: funS.
 Qed.
 
 Canonical pi_path_reverse_morph := PiMorph1 path_reverse_morph.
 
-Lemma path_reverse_final_initE (f : Path) : 
+Lemma path_reverse_final_initE (f : RPath) : 
   path_final (path_reverse f) = path_init f.
 Proof.
 have := path_init_mono (repr f); rewrite reprK => ->.
@@ -647,7 +647,7 @@ rewrite (path_final_mono (cts_fun_rev (repr f))).
 by rewrite /cts_fun_rev /= /rev_param onem1.
 Qed.
 
-Lemma path_reverse_init_finalE (f : Path) : 
+Lemma path_reverse_init_finalE (f : RPath) : 
   path_init (path_reverse f) = path_final f.
 Proof.
 have := path_final_mono (repr f); rewrite reprK => ->.
@@ -656,18 +656,18 @@ rewrite (path_init_mono (cts_fun_rev (repr f))).
 by rewrite /cts_fun_rev /= /rev_param onem0.
 Qed.
 
-Lemma path_cts : {mono \pi_Path : f / {within `[0,1], continuous f}
+Lemma path_cts : {mono \pi_RPath : f / {within `[0,1], continuous f}
   >-> {within `[0,1], continuous (repr f)}}.
 Proof.
 move=> f; rewrite propeqE; split => ctsF.
-  have /eqquotP/asboolP [gamma fpp]: repr (\pi_Path f) = f %[mod Path]. 
+  have /eqquotP/asboolP [gamma fpp]: repr (\pi_RPath f) = f %[mod RPath]. 
     by rewrite reprK.
   apply: subspace_eq_continuous.
     move=> x /set_mem /=; move: x; exact: fpp.
   move=> x; apply: (@continuous_comp (subspace_topologicalType _) (subspace_topologicalType `[0,1]) _).
     by apply: subspaceT_continuous; [exact: funS | exact: continuous_fun].
   exact: ctsF.
-have /eqquotP/asboolP [gamma fpp]: f = repr (\pi_Path f) %[mod Path]. 
+have /eqquotP/asboolP [gamma fpp]: f = repr (\pi_RPath f) %[mod RPath]. 
   by rewrite reprK.
 apply: subspace_eq_continuous.
   move=> x /set_mem /=; move: x; exact: fpp.
@@ -678,14 +678,14 @@ Qed.
 
 Canonical pi_path_cts_mono := PiMono1 path_cts.
 
-Definition path_link := lift_op2 Path split_domain.
+Definition path_link := lift_op2 RPath split_domain.
 
 Lemma path_link_morph : {morph \pi : f g / split_domain f g >-> path_link f g}.
 Proof.
 move=> f g /=; unlock path_link; apply/eqquotP/asboolP. 
-have /eqquotP/asboolP [r1 fpp]: (f = (repr (\pi_(Path) f)) %[mod Path]). 
+have /eqquotP/asboolP [r1 fpp]: (f = (repr (\pi_(RPath) f)) %[mod RPath]). 
   by rewrite reprK.
-have /eqquotP/asboolP [r2 gpp]: (g = (repr (\pi_(Path) g)) %[mod Path]). 
+have /eqquotP/asboolP [r2 gpp]: (g = (repr (\pi_(RPath) g)) %[mod RPath]). 
   by rewrite reprK.
 exists (split_parametrize r1 r2) => x x01.
 have : affine 2 0 x \in `[0,2].
@@ -721,237 +721,46 @@ Canonical pi_path_chain_morph := PiMorph2 path_link_morph.
 
 End Reparametrization.
 
-HB.mixin Record IsPathFrom {R : realType} {T : topologicalType} (B : set T) 
-    (x : T) (f : @Path R _ B) :=
-  {
-    initial_in : B x;
-    from_point : path_init f = x;
-  }.
-
-HB.structure Definition PathFrom {R : realType} {T : topologicalType} (B : set T) 
-  (x : T) := {f of @IsPathFrom R T B x f}.
-
-HB.mixin Record IsPathTo {R : realType} {T : topologicalType} (B : set T)
-    (x : T) (f : @Path R _ B) :=
-  {
-    final_in : B x;
-    to_point : path_final f = x;
-  }.
-
-HB.structure Definition PathTo {R : realType} {T : topologicalType}  
-  (B : set T) (x : T) := {f of @IsPathTo R T B x f}.
-
-HB.structure Definition PathBetween {R : realType} {T : topologicalType} 
-  {B : set T} (x y : T) := {f of (@PathFrom R T B x f) & (@PathTo R T B y f)}.
-
-Notation "{ 'path' R 'from' x 'to' y 'in' B }" := 
-  (@PathBetween.type R _ B x y) : form_scope.
-
-Notation "{ 'Loop' R 'at' x 'in' B }" := 
-  (@PathBetween.type R _ B x x) : form_scope.
-
-Notation "[ 'loop' 'at' x 'of' f ]" := 
-  ([the (@PathBetween.type _ _ _ x x) of (f: @Path _ _ _)]) : form_scope.
-
-Section Paths.
-Context {R : realType} {T : topologicalType} (B : set T).
-Section ConstantPath.
-Variable (x : T).
-Hypothesis Bx : B x.
-
-Local Lemma cst_fun : set_fun `[(0:R),1]%classic B (cst x). 
-Proof. by []. Qed. 
-HB.instance Definition _ := @IsFun.Build _ _ _ _ _ cst_fun.
-
-Local Lemma cst_continuous : {within `[0,1], continuous (@cst R _ x)}.
-Proof. by apply: continuous_subspaceT => ? ?; exact: cst_continuous. Qed.
-
-HB.instance Definition _ := @IsContinuous.Build _ _ _ _ cst_continuous.
-
-Definition cst_path := \pi_(Path B) (@cst R _ x).
-
-Local Lemma cst_path_from : @PathFrom R T B x cst_path.
-Proof. by split; split; rewrite // path_init_mono. Qed.
-HB.instance Definition _ := cst_path_from.
-
-Local Lemma cst_path_to : @PathTo R T B x cst_path.
-Proof. by split; split; rewrite // path_final_mono. Qed.
-HB.instance Definition _ := cst_path_to.
-
-Definition cst_loop := [loop at x of cst_path].
-End ConstantPath.
-
-Section ReversePathEndpoints.
-Variable (x : T).
-Lemma path_rev_from (f : @PathFrom.type R T B x) : @PathTo R T B x (path_reverse f) .
-Proof. 
-split; split; first exact: (@initial_in _ _ _ _ f).
-by rewrite path_reverse_final_initE from_point.
-Qed.
-
-HB.instance Definition _ f := @path_rev_from f.
-
-Lemma path_rev_to (f : @PathTo.type R T B x) : @PathFrom R T B x (path_reverse f) .
-Proof. 
-split; split; first exact: (@final_in _ _ _ _ f).
-by rewrite path_reverse_init_finalE to_point.
-Qed.
-
-HB.instance Definition _ f := @path_rev_to f.
-End ReversePathEndpoints.
-
-Section ReverseLoop.
-Variable (x : T) (f : {Loop R at x in B}).
-
-HB.instance Definition _ := @path_rev_to x f.
-HB.instance Definition _ := @path_rev_from x f.
-HB.instance Definition _ := PathBetween.on (path_reverse f).
-
-End ReverseLoop.
-
-Section SplitDomainPath.
-Context (x : T) (f : PathTo.type R B x) (g : PathFrom.type R B x).
-
-Let f' := repr (f : Path B).
-Let g' := repr (g : Path B).
-
-Local Lemma endpointsE2 : g' 0 = f' 1.
-by rewrite -path_init_mono -path_final_mono ?reprK from_point to_point.
-Qed.
-
-Local Lemma cts_split_domain2 : {within `[0,1], continuous (split_domain f' g')}.
-Proof. by apply: h_cts; rewrite endpointsE2. Qed.
-
-HB.instance Definition P1 := @IsContinuous.Build _ _ _ _ cts_split_domain2.
-
-Definition split_path := \pi_(Path B) [continuous of (split_domain f' g')].
-End SplitDomainPath.
-
-Section SplitDomainMorph.
-Variables (p q : {continuous `[(0:R),1] >-> B}).
-Hypothesis endpointsE1 : q 0 = p 1.
+HB.mixin Record IsRPathFrom {R} {T : topologicalType}
+    (x : T) (f : @RPath R T) :=
+  { from_point : path_init f = x }.
 
-Lemma cts_split_domain1 : {within `[0,1], continuous (split_domain p q)}.
-Proof. by apply: h_cts; rewrite endpointsE1. Qed.
+HB.structure Definition RPathFrom {R} {T : topologicalType}
+  (x : T) := {f of @IsRPathFrom R T x f}.
 
-HB.instance Definition _ := Fun.on (split_domain p q).
-HB.instance Definition P2 := @IsContinuous.Build _ _ _ _ cts_split_domain1.
+HB.mixin Record IsRPathTo {R} {T : topologicalType}
+    (x : T) (f : @RPath R T) :=
+  { to_point : path_final f = x }.
 
-Let split_aux : {continuous `[0,1] >-> B} := HB.pack (split_domain p q) P2.
-
-Local Lemma path_from_q : @PathFrom R T B (q 0) (\pi_(Path B) q).
-Proof. 
-split; split; first by apply: funS; rewrite /= bound_itvE.
-exact: path_init_mono.
-Qed.
-
-HB.instance Definition _ := path_from_q.
-
-Local Lemma path_to_p : @PathTo R T B (q 0) (\pi_(Path B) p).
-Proof. 
-split; split; first by rewrite endpointsE1; apply: funS; rewrite /= bound_itvE.
-by rewrite endpointsE1 -path_final_mono.
-Qed.
-
-HB.instance Definition _ := path_to_p.
-
-Lemma split_domain_morph : 
-  \pi_(Path B) split_aux = split_path 
-    ([the (PathTo.type R B (q 0)) of (\pi_(Path B) p : Path B)]) 
-    ([the (PathFrom.type R B (q 0)) of (\pi_(Path B) q : Path B)]).
-Proof.
-apply/eqquotP/asboolP => //=.
-have /eqquotP/asboolP [gamma rpp]: repr (\pi_(Path B) p) = p %[mod Path B]. 
-  by rewrite reprK.
-have /eqquotP/asboolP [delta rqq]: repr (\pi_(Path B) q) = q %[mod Path B]. 
-  by rewrite reprK.
-eexists => x x01.
-rewrite /split_domain/patch /= -rpp -?rqq /=. 
-pose lhs := fun z => (inv_parametrization gamma) z / 2.
-pose rhs := fun z => ((inv_parametrization delta) z / 2) + 1/2.
-exists (split_domain lhs rhs  delta)
-
-
-Lemma split_domain_morph : \pi_(Path B) split1 = \pi_(Path B) split2.
-
-Lemma chain_from_x : @PathFrom R T B x (@chain y f g).
-Proof.
-split; split; first (apply: initial_in; exact: f).
-rewrite path_init_mono /= /ftheng /patch; case: ifP => //=.
-  by move=> _; rewrite mul0r -path_init_mono reprK from_point.
-by rewrite mem_setE /= in_itv /= => /andP [].
-Qed.
-
-HB.instance Definition _ := chain_from_x.
-End AddStart.
-
-Section AddEnd.
-Context (x y : T) (f : PathTo.type R B x) (g : {path R from x to y in B}) .
-
-Lemma chain_to_y : @PathTo R T B y (@chain x f g).
-Proof.
-split; split; first (apply: final_in; exact: g).
-rewrite path_final_mono /= /ftheng /patch; case: ifP => //=.
-  rewrite mem_setE /= in_itv /= => /andP [_]; rewrite ler_pdivl_mulr // mul1r.
-  by rewrite real_leNgt // => /negP []; rewrite ltr_addr.
-move=> _; rewrite mul1r (_ : 2 - 1 = 1) -?path_final_mono ?reprK ?to_point //.
-by apply/eqP; rewrite subr_eq.
-Qed.
-
-HB.instance Definition _ := chain_to_y.
-End AddEnd.
-
-Section AddLoop.
-Context (x : T) (f g : {Loop R at x in B}).
-
-HB.instance Definition _ := PathFrom.on (chain f g).
-HB.instance Definition _ := PathTo.on (chain f g).
-HB.instance Definition _ := PathBetween.on (chain f g).
-
-End AddLoop.
-
-Section loops_zmod.
-Variable (x : T).
-Hypotheses Bx : B x.
-
-Definition loop_id : {Loop R at x in B} := (cst_loop Bx).
-
-Definition loop_reverse (f : {Loop R at x in B}) : {Loop R at x in B} :=
-  [loop at x of (path_reverse f)].
-
-Definition loop_chain (f g : {Loop R at x in B}) : {Loop R at x in B} := 
-  [loop at x of @chain x f g].
-
-Definition loops_zmodMixin := 
-  @ZmodMixin {Loop R at x in B} (loop_id) 
-    (loop_reverse) (loop_chain).
+HB.structure Definition RPathTo {R} {T : topologicalType}  
+  (x : T) := {f of @IsRPathTo R T x f}.
 
+HB.structure Definition RPathBetween {R} {T : topologicalType} 
+  (x y : T) := {f of (@RPathFrom R T x f) & (@RPathTo R T y f)}.
 
+HB.mixin Record IsPath {R} {T : topologicalType} (B : set T) (f : @RPath R T) := 
+  {
+    continuous_path : {within `[0,1], continuous (repr f)};
+    path_fun : set_fun `[0,1]%classic B (repr f);
+  }.
 
-Section path_components.
+HB.structure Definition Path {R} {T : topologicalType} (B : set T) := 
+  { f of IsPath R T B f}.
 
-Definition same_path_component (t u : {x : T | B x}) := 
-  `[<exists (p : {path R, B from (projT1 t) to (projT1 u)}), True>].
+HB.structure Definition PathFrom {R} {T : topologicalType} (B : set T) (x : T) := 
+  { f of IsPath R T B f & IsRPathFrom R T x f}.
 
-Lemma reflexive_path_comp : reflexive same_path_component.
-Proof.
-by case=> t Bt; apply/asboolP; exists (constant_path Bt).
-Qed.
+HB.structure Definition PathTo {R} {T : topologicalType} (B : set T) (y : T) := 
+  { f of IsPath R T B f & IsRPathTo R T y f}.
 
-Lemma symmetric_path_comp : symmetric same_path_component.
-Proof.
-move=> x y. apply/asbool_equiv_eq; split; case=> f _. 
-  by exists [path from (projT1 y) to (projT1 x) of (reverse_path f)].
-by exists [path from (projT1 x) to (projT1 y) of (reverse_path f)].
-Qed.
+HB.structure Definition PathBetween {R} {T : topologicalType} (B : set T) (x y : T) := 
+  { f of IsPath R T B f & IsRPathFrom R T x f & IsRPathTo R T y f}.
 
-Lemma transitive_path_comp : transitive same_path_component.
-Proof.
-move=> ? ? ? /asboolP [f _] /asboolP [g _]; apply/asboolP. 
-by exists (chain f g).
-Qed.
+Notation "{ 'path' R 'from' x 'to' y 'in` B }" := 
+  (@PathBetween.type R _ B x y) : form_scope.
 
-Definition path_components_rel := EquivRel same_path_component 
-  reflexive_path_comp symmetric_path_comp transitive_path_comp.
+Notation "{ 'Loop' R 'at' x 'in' B }" := 
+  (@PathBetween.type R _ B x x) : form_scope.
 
-End path_components.
+Notation "[ 'loop' of' f ]" := 
+  ([the (@PathBetween.type _ _ _ _ _) of (f: @Path _ _ _)]) : form_scope.