reversing paths

theories/homotopy.v

@@ -25,6 +25,7 @@ Import numFieldNormedType.Exports.
 
 Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
+Local Open Scope quotient_scope.
 
 HB.mixin Record IsParametrization {R : realType} (f : R -> R) := 
   { 
@@ -136,7 +137,6 @@ Qed.
 
 HB.instance Definition _ := Can.Build _ _ _ g g_cancel.
 HB.instance Definition _ := IsFun.Build _ _ _ _ _ g_fun.
-HB.instance Definition _ := SplitInjFun.on g.
 
 HB.instance Definition _ := @IsParametrization.Build
   _ _ g_continuous g_init g_final.
@@ -177,7 +177,7 @@ Notation "[ 'continuous' 'of' f ]" :=
   ([the (@ContinuousFun.type _ _ _ _) of (f: _ -> _)]) : form_scope.
 
 Section Reparametrization.
-Open Scope quotient_scope.
+
 Context {R : realType} {T : topologicalType} (B : set T).
 
 Definition reparametrize (f g : {classic {continuous `[0,1] >-> B}}) : bool :=
@@ -245,93 +245,45 @@ Qed.
 
 Canonical pi_path_image_mono := PiMono1 path_image_mono.
 
-Section ConstantPath.
-Context (x : T).
-Hypothesis Bx : B x.
-Let f : (subspace `[(0:R),1]) -> T := fun=> x.
-
-Local Lemma cst_fun : set_fun `[0,1]%classic B f. 
-Proof. by []. Qed. 
-HB.instance Definition _ := @IsFun.Build _ _ _ _ _ cst_fun.
-
-Local Lemma cst_continuous : continuous f.
-Proof. by apply: continuous_subspaceT => ? ?; exact: cst_continuous. Qed.
-
-HB.instance Definition _ := @IsContinuous.Build _ _ _ cst_continuous.
-
-Definition cst_path : Path := \pi [continuous of f].
-
-
-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.
+Definition path_precompose (h : R -> R) := lift_op1 Path (fun f => f \o h).
 
-HB.mixin Record IsClosed {R : realType} {T : topologicalType}
-    (f : R -> T)  := { endpointsE : f 0 = f 1 }.
-HB.structure Definition JustClosed {R : realType} {T : topologicalType}
-   := {f of IsClosed R T f}.
+End Reparametrization.
 
-HB.structure Definition Loop {R : realType} {T : topologicalType}
-  (B : set T):= { f of @Path R _ B f & @IsClosed R T f}.
+Notation "{ 'path' R , B }" := (@Path R _ B) : form_scope.
 
-Notation "{ 'loop' R , B }" := (@Loop.type R _ B) : form_scope.
-Notation "[ 'loop' 'of' f ]" := ([the (@Loop.type _ _ _) of (f : _ -> _)]) : form_scope.
+Definition PathFrom {R : realType} {T : topologicalType} (B : set T) (x : T)
+    (f : @Path R _ B) := path_init f = x.
 
-HB.mixin Record IsBetween {R : realType} {T : topologicalType}
-    (init final : T) (f : R -> T) := 
-  { init_point : f 0 = init; final_point : f 1 = final; }.
-HB.structure Definition JustBetween {R : realType} {T : topologicalType}
-    (init final : T) := 
-  { f of @IsBetween R T init final f }.
+Definition PathTo {R : realType} {T : topologicalType} (B : set T) (x : T)
+    (f : @Path R _ B) := path_final f = x.
 
+Definition LoopAt {R : realType} {T : topologicalType} (B : set T) (x : T)
+    (f : @Path R _ B) := PathFrom x f /\ PathTo x f.
 
-HB.structure Definition PathBetween {R : realType} {T : topologicalType}
-    (init final : T) (B : set T) := 
-    { 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.
-
-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 '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} (B : set T).
 Section ConstantPath.
-Context (x : T).
+Context {R : realType} {T : topologicalType} (B : set T) (x : T).
 Hypothesis Bx : B x.
-Let f : R -> T := fun=> x.
+Let f : (subspace `[(0:R),1]) -> T := fun=> x.
 
 Local Lemma cst_fun : set_fun `[0,1]%classic B f. 
 Proof. by []. Qed. 
 HB.instance Definition _ := @IsFun.Build _ _ _ _ _ cst_fun.
 
-Local Lemma cst_path : {within `[0,1], continuous f}.
+Local Lemma cst_continuous : continuous f.
 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 _).
-HB.instance Definition _ := @IsBetween.Build R T x x f (erefl _) (erefl _).
+HB.instance Definition _ := @IsContinuous.Build _ _ _ cst_continuous.
+
+Definition cst_path : Path B := \pi_(Path B) [continuous of f].
+
+Lemma cst_path_closed : LoopAt x cst_path.
+Proof. by rewrite /LoopAt/PathFrom/PathTo path_final_mono path_init_mono. Qed.
 
-Definition constant_path := [loop at x of f].
 End ConstantPath.
 
-Lemma shift_path (f : {path R, B}) (shift : {fun `[(0:R),1]%classic >-> `[(0:R),1]%classic}) : 
- (continuous (shift : subspace `[0,1] -> subspace `[0,1])) ->
- {within `[0,1], continuous (f \o shift)}.
-Proof.
-move=> cts x.
-apply: (@continuous_comp
-  (subspace_topologicalType `[0,1]) (subspace_topologicalType `[0,1]) _).
-  exact: cts.
-exact: path_continuous.
-Qed.
+Section ReversePath.
+Context {R : realType} {T : topologicalType} (B : set T).
+Variables (f  : @Path R _ B).
 
 Let flip_f (x : subspace `[(0:R),1]) : subspace `[0,1] := `1- x.
 
@@ -348,13 +300,13 @@ Lemma rev_cts: continuous flip_f.
 Proof.
 move=> z; apply: subspaceT_continuous; rewrite /= /flip_f.
 move=> ?; apply: continuous_subspaceT.
-move=> ?; apply: (@continuousD R R R ); first exact: cst_continuous.
+move=> ?; apply: (@continuousD R R R ); first exact: cvg_cst.
 exact: opp_continuous.
 Qed.
 
-Section ReversePath.
-Variables (f : {path R, B}).
+HB.instance Definition _ := @IsContinuous.Build _ _ _ rev_cts.
 
+Section ReversePath.
 Definition flip_path := [fun of f] \o [fun of flip_f].
 
 Lemma flip_path_funS : @set_fun R T `[0,1]%classic B flip_path.