diff --git a/theories/homotopy.v b/theories/homotopy.v
index 4c447759b2..654be60d20 100644
--- a/theories/homotopy.v
+++ b/theories/homotopy.v
@@ -36,7 +36,7 @@ HB.structure Definition Path {R : realType} {T : topologicalType}
   (B : set T) := {f of @IsPath R T f & @Fun R T `[0,1]%classic B f}.
 
 Notation "{ 'path' R , B }" := (@Path.type R _ B) : form_scope.
-Notation "[ 'path' 'of' f ]" := ([the (@Path.type _ _ _) of f]) : form_scope.
+Notation "[ 'path' 'of' f ]" := ([the (@Path.type _ _ _) of (f: _ -> _)]) : form_scope.
 
 HB.mixin Record IsClosed {R : realType} {T : topologicalType}
     (f : R -> T)  := { endpointsE : f 0 = f 1 }.
@@ -47,7 +47,7 @@ HB.structure Definition Loop {R : realType} {T : topologicalType}
   (B : set T):= { f of @Path R _ B f & @IsClosed R T f}.
 
 Notation "{ 'loop' R , B }" := (@Loop.type R _ B) : form_scope.
-Notation "[ 'loop' 'of' f ]" := ([the (@Loop.type _ _ _) of f]) : form_scope.
+Notation "[ 'loop' 'of' f ]" := ([the (@Loop.type _ _ _) of (f : _ -> _)]) : form_scope.
 
 HB.mixin Record IsBetween {R : realType} {T : topologicalType}
     (init final : T) (f : R -> T) := 
@@ -62,14 +62,14 @@ HB.structure Definition PathBetween {R : realType} {T : topologicalType}
     { f of @Path R T B f & @IsBetween R T init final f}.
 
 Notation "{ 'path' R , B 'from' t1 'to' t2 }" := (@PathBetween.type R _ t1 t2 B) : form_scope.
-Notation "[ 'path' 'from' t1 'to' t2 'of' f ]" := ([the (@PathBetween.type _ _ t1 t2 _) of f]) : form_scope.
+Notation "[ 'path' 'from' t1 'to' t2 'of' f ]" := ([the (@PathBetween.type _ _ t1 t2 _) of (f : _ -> _)]) : form_scope.
 
 HB.structure Definition LoopAt {R : realType} {T : topologicalType}
     (init : T) (B : set T) := 
     { f of @Loop R T B f & @IsBetween R T init init f}.
 
-Notation "{ 'loop' R , B `on` t }" := (@LoopAt.type R _ t B) : form_scope.
-Notation "[ 'loop' 'at' t 'of' f ]" := ([the (@LoopAt.type _ _ t _) of f]) : form_scope.
+Notation "{ 'loop' R , B 'at' t }" := (@LoopAt.type R _ t B) : form_scope.
+Notation "[ 'loop' 'at' t 'of' f ]" := ([the (@LoopAt.type _ _ t _) of (f : _ -> _)]) : form_scope.
 
 Section Paths.
 Context {R : realType} {T : topologicalType}.
@@ -83,7 +83,7 @@ Proof. by []. Qed.
 HB.instance Definition _ := @IsFun.Build _ _ _ _ _ cst_fun.
 
 Local Lemma cst_path : {within `[0,1], continuous f}.
-Proof. by apply: subspace_restrict_domain => ? ?; exact: cst_continuous. Qed.
+Proof. by apply: continuous_subspaceT => ? ?; exact: cst_continuous. Qed.
 HB.instance Definition _ := @IsPath.Build R T f cst_path.
 
 HB.instance Definition _ := @IsClosed.Build R T f (erefl _).
@@ -116,13 +116,11 @@ HB.instance Definition _ :=
 
 Lemma rev_cts: continuous flip_f.
 Proof.
-  (* need to merge 739 for this*)
-(*move=> z; apply: subspace_continuous_restricted; rewrite /= /flip_f.
-move=> ?; apply: subspace_restrict_domain.
+move=> z; apply: subspaceT_continuous; rewrite /= /flip_f.
+move=> ?; apply: continuous_subspaceT.
 move=> ?; apply: (@continuousD R R R ); first exact: cst_continuous.
 exact: opp_continuous.
-*)
-Admitted.
+Qed.
 
 Section ReversePath.
 Variables (B : set T) (f : {path R, B}).
@@ -138,6 +136,7 @@ HB.instance Definition _ :=
 HB.instance Definition _ := 
   @IsFun.Build R T `[0,1]%classic B flip_path flip_path_funS.
 
+
 Definition reverse_path := [path of flip_path].
 End ReversePath.
 
@@ -149,9 +148,7 @@ by split; rewrite /= /flip_path /= /flip_f onem0 onem1 -endpointsE.
 Qed.
 
 HB.instance Definition _ := rev_loop.
-
-Definition foo := [the (@Path.type R T B) of (reverse_path f)].
-Definition bar := [the (@JustClosed.type R T) of (reverse_path f)].
+End RevLoop.
 
 Section RevPathBetween.
 Context {t1 t2 : T} {B : set T} (f : {path R, B from t1 to t2}).
@@ -161,40 +158,31 @@ split; rewrite /= /flip_path /= /flip_f ?onem1 ?onem0.
   by rewrite final_point.
 by rewrite init_point.
 Qed.
+
 HB.instance Definition _ := @rev_pathbetween.
 
-Definition foo := [path of reverse_path f ].
+End RevPathBetween.
 
-Lemma rev_loopAt {t1 : T} {B : set T} (f : {path R, B from t1 to t2}) :
-  @IsBetween R T t2 t1 (reverse_path f). 
-Proof. 
-split; rewrite /= /flip_path /= /flip_f ?onem1 ?onem0.
-  by rewrite final_point.
-by rewrite init_point.
-Qed.
-HB.instance Definition _ t1 t2 B f := @rev_pathbetween t1 t2 B f.
+Section ReverseLoopAtBetween.
+Context {B : set T} (t : T) (f : {loop R, B at t}).
 
-Section ReversePathBetween
-Context {B : set T} (f : {loop R, B}).
-Lemma rev_loop : @IsClosed R T (reverse_path f). 
-Proof. 
-by split; rewrite /reverse_path //= /flip_path /= onem0 onem1 -endpointsE. 
-Qed.
+Lemma rev_loop_at : @IsBetween R T t t (reverse_path f). 
+Proof. apply: rev_pathbetween. Qed. 
 
-Lemma nbhs_subspaceW {T : topologicalType} (A : set T) (B : set T) (x : T) :
-  nbhs (x : T) B -> nbhs (x : subspace A) B.
-Proof.
-rewrite ?nbhsE /= => [[]] O [[]] oO Ox oB; exists O; split => //.
-by split=> //; exact: open_subspaceW.
-Qed.
+HB.instance Definition _ := @rev_loop_at.
+End ReverseLoopAtBetween.
+
+(* 
+Why doesn't this work?
+Definition foo := [path from t to t of (reverse_path f)].
+*)
 
 Section ChainPath.
-Context {R : realType} {T : topologicalType} (B : set T).
-Variables (f g : {path R, B}).
+Context (B : set T) (x1 x2 x3 : T) (f : {path R, B from x1 to x2}).
+Context (g : {path R, B from x2 to x3}).
 Let shift1 : R -> R := (fun r => r*2).
 Let shift2 : R -> R := (fun r => r*2 - 1).
 Definition chain := patch (g \o shift2) (`[0,1/2]%classic) (f \o shift1).
-Hypothesis f1g0 : g 0 = f 1.
 
 Local Lemma shift1fun : 
   @set_fun R R `[0,1/2]%classic `[0,1]%classic shift1.
@@ -214,7 +202,7 @@ move=> x; apply: (@continuous_comp
   [topologicalType of (subspace `[0,1/2])] 
   [topologicalType of (subspace `[0,1])] 
   T _ _ x); last exact: path_continuous.
-apply: subspace_restrict_range; apply: subspace_restrict_domain.
+apply: subspaceT_continuous; apply: continuous_subspaceT.
 by move => z; apply: (@continuousM R R _ _ z) => //; exact: cst_continuous.
 Qed.
 
@@ -237,7 +225,8 @@ apply: (@subspace_eq_continuous _ _ _ h2 chain).
     move=> /negP /= P /set_mem/andP [] ? ?; contradict P.
     by apply: mem_set; apply/andP; split => //; exact: ltW.
   move=> P Q; suff -> : q = 1/2.
-    rewrite /shift2 /shift1 divfK // subrr; exact: f1g0.
+    by rewrite /shift2 /shift1 divfK // subrr final_point init_point.
+
   case/set_mem/andP: P => qpos qhlf.
   move/negP:Q => /=; apply: contra_notP=> qnhlf.
   apply/mem_set/andP; split => //.
@@ -250,7 +239,7 @@ move=> x; apply: (@continuous_comp
   [topologicalType of (subspace `[1/2, 1])] 
   [topologicalType of (subspace `[0,1])] 
   T _ _ x); last exact: path_continuous.
-apply: subspace_restrict_range; apply: subspace_restrict_domain.
+apply: subspaceT_continuous; apply: continuous_subspaceT.
 move => z /=; rewrite /shift2. 
 apply (@continuousD R R R) => //; last exact: cst_continuous.
 apply (@continuousM R) => //; last exact: cst_continuous.
@@ -282,45 +271,22 @@ apply: funS; apply/andP; split => //; move: P; apply: contra_notP => /=.
 by move=> /negP; rewrite -ltNge => /ltW ?; apply/mem_set/andP; split.
 Qed.
 
-HB.instance Definition p1 := @IsPath.Build R T chain h_cts.
-HB.instance Definition p2 := @IsFun.Build _ _ _ B chain h_fun.
-
-Definition chain_path := [path of chain].
-End ChainPath.
-
-Section ChainLoop.
-Context {R : realType} {T : topologicalType} (B : set T).
-Variables (f g : {loop R, B}).
-
-Lemma fgpoint : f 1 = g 0.
-Proof.
-rewrite (@endpointsE _ _ _ f).
-
-Definition chain_loop_aux = chain_path ()
-
-Lemma chain_reverse {R : realType} {T : topologicalType} (B : set T) (f : {path R, B}) :
-  (chain f (rev_path f)) 0 = 
-  (chain f (f \o path_rev)) 1.
-
-Section HomotopiesAsPaths.
-Context {R : realType} {T : uniformType} (B : set T) (x : T).
-Hypothesis Bx : B x.
-
-Canonical paths_eqType := EqType {path R, B} gen_eqMixin.
-Canonical paths_choiceType := ChoiceType {path R, B} gen_choiceMixin.
-Canonical paths_PointedType :=
-  PointedType {path R, B} (@constant_path R T B x Bx).
-
-Definition include (f : {path R, B}) : {uniform` `[(0:R),1]%classic -> T} := f.
-
-Canonical PathSpace {R : realType} {T : uniformType} (B : set T) :=
-  weak_topologicalType include.
-End HomotopiesAsPaths.
+Lemma chain_init : chain 0 = x1.
+Proof. 
+rewrite /chain patchT /shift1 /= ?(@mul0r R) ?init_point //.
+rewrite mem_set //= bound_itvE; apply: divr_ge0 => //.
+Qed.
 
-HB.structure Definition PathHomotopy {R : realType} {T : topologicalType} 
-  (B : set T) := { f of IsPathHomotopy R T f & IsFun _ _ square B f }.
+Lemma chain_final : chain 1 = x3.
+Proof. 
+rewrite /chain patchC /shift2 /= mul1r. 
+  by rewrite (_ : 2 = 1+1) // addrK final_point //. 
+rewrite setCitv /= in_setU; apply/orP; right => /=.
+by rewrite set_itv_o_infty mem_set //= invr_cp1 // ?unitfE // ltr_addr.
+Qed.
+  
+HB.instance Definition _ :=  @IsBetween.Build R T x1 x3 chain chain_init chain_final.
+HB.instance Definition _ := @IsPath.Build R T chain h_cts.
+HB.instance Definition _ := @IsFun.Build _ _ _ B chain h_fun.
 
-Lemma hpath_path (h : @PathHomotopy.type R T B) : 
-  IsPath R _ (hpath h).
-Proof.
-split.
+End ChainPath.