homotopy stuff

theories/homotopy.v

@@ -45,7 +45,7 @@ HB.mixin Record CrossingFree {R : realType} {T : topologicalType}
 HB.structure Definition Loop {R : realType} {T : topologicalType}
   (B : set T):= { f of @Path R _ B f & @IsClosed R T f}.
 
-Notation "{ 'loop on' B }" := (@Loop.type _ _ B) : form_scope.
+Notation "{ 'loop' R , B }" := (@Loop.type _ _ B) : form_scope.
 
 HB.structure Definition JordanCurve {R : realType} {T : topologicalType} 
   (B : set T):= { f of @Loop R T B f & @CrossingFree R T f }.
@@ -71,6 +71,22 @@ HB.instance Definition _ := @IsClosed.Build R T f cst_closed.
 Definition constant_path := [the (@Loop.type R T [set x]) of f].
 End ConstantPath.
 
+Section PathShift.
+Context {R : realType} {T : topologicalType} (B : set T) (f : {path R, B}).
+
+Lemma shift_path (shift : {fun `[(0:R),1]%classic >-> `[(0:R),1]%classic}) : 
+ (continuous (shift : subspace `[0,1] -> subspace `[0,1])) ->
+ IsPath _ _ (f \o shift).
+Proof.
+move=> cts; split=> x. 
+apply: (@continuous_comp (subspace_topologicalType `[0,1]) 
+    (subspace_topologicalType `[0,1]) _). 
+  exact: cts.
+exact: path_continuous.
+Qed.
+
+End PathShift.
+
 Lemma subspace_continuous_restricted {T : topologicalType} (A : set T)
     (f : {fun A >-> A}) : 
   continuous (f : T -> T) -> continuous (f : subspace A -> subspace A).
@@ -82,11 +98,12 @@ rewrite eqEsubset; split=> x [] ? ?; split=> //; have: A (f x) by exact: funS.
   by move=> afx; have: (V `&` A) (f x) by []; rewrite VAUA=> [[]].
 by move=> afx; have: (U `&` A) (f x) by []; rewrite -VAUA=> [[]].
 Qed.
-
 
-Section Reverse.
+Section ReversePath.
 Context {R : realType} {T : topologicalType}.
+
 Definition path_rev (x : subspace `[(0:R),1]) : subspace `[0,1] := `1- x.
+
 Lemma path_rev_funS : @set_fun  _ _ `[0,1]%classic `[0,1]%classic path_rev.
 Proof.
 rewrite ?set_itvcc => x /= /andP [] xnng xle1; apply/andP. 
@@ -95,33 +112,21 @@ Qed.
 
 HB.instance Definition _ := 
   @IsFun.Build R R (`[0,1]%classic) (`[0,1]%classic) (path_rev) path_rev_funS.
-Section ReverseFun.
 
-Variable (B : set T) (f : {path R, B}).
-
-Definition reverse_path := [fun of (f : _ -> _)] \o [fun of path_rev].
-
-Local Lemma reverse_cts : {within `[0,1], continuous (reverse_path)}.
-Proof. 
-move=> x; apply: (@continuous_comp _ (subspace_topologicalType `[0,1]) _). 
-  move=> z; apply: subspace_continuous_restricted; rewrite /= /path_rev.
-  move=> ?; apply: (@continuousD R R R ); first exact: cst_continuous.
-  exact: opp_continuous.
-exact: path_continuous.
+Lemma rev_cts: continuous path_rev.
+Proof.
+move=> z; apply: subspace_continuous_restricted; rewrite /= /path_rev.
+move=> ?; apply: (@continuousD R R R ); first exact: cst_continuous.
+exact: opp_continuous.
 Qed.
 
-Local Lemma reverse_fun : set_fun `[0,1]%classic B reverse_path.
-Proof. 
+HB.instance Definition _ (B : set T) (f : {path R, B}) := 
+  @shift_path R T B f [fun of path_rev] rev_cts.
 
-HB.instance Definition _ := @IsPath.Build _ _ _ reverse_cts.
+Lemma rev_loop (B : set T) {f : @Loop.type R T B} : 
+  @IsClosed R T (f \o path_rev). 
+Proof. by split; rewrite /path_rev /= onem0 onem1 -endpointsE. Qed.
 
-Definition test1 := [the (@Path.type R T B) of reverse_path].
-@TheCanonical.put reverse_path reverse_path
-
-End ReversePath.
-
-Section ReversePathOn.
-Context (B : set T) (f : @PathOn.type R T B).
-Proof.
+HB.instance Definition _ (B : set T) (f : {loop R, B}) := @rev_loop B f.
 
-End Reverse.
+End ReversePath.