getting there on paths

theories/homotopy.v

@@ -28,7 +28,6 @@ Local Open Scope ring_scope.
 
 HB.mixin Record IsParametrization {R : realType} (f : R -> R) := 
   { 
-    parametrize_monotone : {in `[0, 1] &, {homo f : x y / x <= y}};
     parametrize_cts : {within `[0,1], continuous f};
     parametrize_init : f 0 = 0;
     parametrize_final : f 1 = 1;
@@ -47,16 +46,22 @@ Notation "[ 'parametrization' 'of' f ]" :=
 Section Parametrizations.
 Context {R : realType}.
 
-Section Identity.
-Local Lemma id_parametrize_monotone : 
-  {in `[0, 1] &, {homo (@idfun R) : x y / x <= y}}.
-Proof. by []. Qed.
+Lemma parametrize_monotone (f : {parametrization R}) : 
+  {in `[0,1] &, {mono f : x y / x <= y}}.
+Proof.
+apply: itv_continuous_inj_le.
+- exists 0; exists 1; rewrite ?bound_itvE ?parametrize_init.
+  by rewrite ?parametrize_final; split.
+- apply: parametrize_cts.
+- by move: (@inj _ _ _ f); rewrite mem_setE.
+Qed.
 
+Section Identity.
 Local Lemma id_parametrize_cts : {within `[0,1], continuous (@idfun R)}.
 Proof. exact: continuous_subspaceT. Qed.
 
 HB.instance Definition _ := @IsParametrization.Build
-  _ _ (id_parametrize_monotone) id_parametrize_cts erefl erefl.
+  _ _ id_parametrize_cts erefl erefl.
 
 Definition id_parametrization := [parametrization of (@idfun R)].
 End Identity. 
@@ -66,14 +71,6 @@ Variables (f g : {parametrization R}).
 Let h := (f \o g) : R -> R.
 HB.instance Definition _ := SplitInjFun.on h.
 
-Local Lemma h_monotone : {in `[0, 1] &, {homo h : x y / x <= y}}.
-Proof. 
-move=> x y ? ? ?; apply: parametrize_monotone.
-- exact: (@funS _ _ _ _ g) => /=.
-- exact: (@funS _ _ _ _ g) => /=.
-- exact: parametrize_monotone.
-Qed.
-
 Local Lemma h_continuous : {within `[0, 1], continuous h}.
 Proof. 
 move=> x; apply: (@continuous_comp
@@ -89,7 +86,7 @@ Local Lemma h_final : h 1 = 1.
 Proof. by rewrite /h /= parametrize_final parametrize_final. Qed.
 
 HB.instance Definition _ := @IsParametrization.Build
-  _ _ (h_monotone) h_continuous h_init h_final.
+  _ _ h_continuous h_init h_final.
 
 Definition comp_parametrization := [parametrization of h].
 End Composition. 
@@ -100,11 +97,170 @@ Variables (f : {parametrization R}).
 
 Let g := (f^-1).
 
-HB.mixin Record IsPath {R : realType} {T : topologicalType} (f : R -> T) := 
-  { path_continuous : {within `[0,1], continuous f} }.
+Local Lemma g_continuous : {within `[0,1], continuous g}.
+Proof. 
+rewrite -(@parametrize_init _ f) -(@parametrize_final _ f). 
+apply: segment_can_le_continuous => //; first exact: parametrize_cts.
+by move=> ? ?; apply/funK/mem_set.
+Qed.
+
+Local Lemma g_init : g 0 = 0.
+Proof. 
+rewrite -[x in g x](@parametrize_init _ f) [g (f _)]funK //. 
+by rewrite mem_setE /= bound_itvE.
+Qed.
+
+Local Lemma g_final : g 1 = 1.
+Proof. 
+rewrite -[x in g x](@parametrize_final _ f) [g (f _)]funK //. 
+by rewrite mem_setE /= bound_itvE.
+Qed.
+
+Local Lemma g_cancel : {in `[0,1]%classic, cancel g f}.
+Proof.
+rewrite mem_setE /= -(@parametrize_init _ f) -(@parametrize_final _ f). 
+apply: segment_continuous_le_can_sym => //; first exact: parametrize_cts.
+by move=> ? ?; apply/funK/mem_set.
+Qed.
+
+Local Lemma g_fun : set_fun `[0,1]%classic `[0,1]%classic g.
+Proof.
+have gle : {in `[0,1] &, {mono g : x y / x <= y}}.
+  apply: itv_continuous_inj_le.
+  - by exists 0; exists 1; rewrite ?bound_itvE ?g_init ?g_final; split.
+  - apply: g_continuous.
+  - by apply: can_in_inj => p q; exact/g_cancel/mem_set.
+move=> z; rewrite /= ?in_itv /= => /[dup] ? /andP [] ? ?.
+by rewrite -g_init -g_final; apply/andP; split; rewrite gle // ?bound_itvE.
+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.
+
+Definition inv_parametrization := [parametrization of g].
+
+Lemma inv_parametrization_can_r : {in `[0,1], cancel f inv_parametrization}.
+Proof.
+move=> z zI /=; rewrite (@segment_continuous_can_sym _ 0 1) //.
+- exact: parametrize_cts.
+- move=> w wI; move: (@funK _ _ _ inv_parametrization w).
+  by rewrite mem_setE invV => /(_ wI).
+- by rewrite g_init g_final /minr /maxr ltr01.
+Qed.
+
+Lemma inv_parametrization_can_l: {in `[0,1], cancel inv_parametrization f}.
+Proof.  by move=> z zI; apply: funK; rewrite mem_setE. Qed.
+
+End Inverses.
+End Parametrizations.
+
+HB.mixin Record IsContinuous {T U : topologicalType} (f : T -> U) :=
+  { continuous_fun : continuous f }.
+
+HB.structure Definition JustContinuous {T U : topologicalType} 
+  := {f of @IsContinuous T U f}.
+
+HB.structure Definition ContinuousFun {T U : topologicalType} 
+    (A : set T) (B : set U) := 
+  {f of 
+    @IsContinuous (subspace_topologicalType A) U f & 
+    @Fun (subspace_topologicalType A) U A B f
+  }.
+
+Notation "{ 'continuous' A >-> B }" := 
+  (@ContinuousFun.type _ _ A B) : form_scope.
+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 :=
+  `[<exists gamma : {parametrization R}, {in `[0,1], f \o gamma =1 g}>].
+
+Lemma reflexive_reparametrize : reflexive reparametrize.
+Proof. by move=> f; apply/asboolP; exists id_parametrization. Qed.
+
+Lemma symmetric_reparametrize : symmetric reparametrize.
+Proof.
+by move=> f g; apply/asbool_equiv_eq; split=> [][] gamma fgamg;
+    exists (inv_parametrization gamma) => z zI;
+    rewrite /comp -fgamg /comp ?inv_parametrization_can_l //;
+    apply: (@funS _ _ _ _ (inv_parametrization gamma)).
+Qed.
+
+Lemma transitive_reparametrize : transitive reparametrize.
+Proof.
+move=> f g h /asboolP [p pfg] /asboolP [q qgh]; apply/asboolP. 
+exists (comp_parametrization p q) => z zI /=. 
+by rewrite -qgh //= -pfg //; exact: (@funS _ _ _ _ q).
+Qed.
+
+Definition equiv_rel_reparametrize := EquivRel reparametrize 
+  reflexive_reparametrize symmetric_reparametrize transitive_reparametrize.
+
+Definition Path := {eq_quot equiv_rel_reparametrize}.
+
+Definition path_init := lift_fun1 Path (fun f => f 0).
+
+Lemma path_init_mono : {mono \pi_Path : f / f 0 >-> path_init f}.
+Proof.
+move=> f; unlock path_init.
+have : ((repr (\pi_(Path) f)) = f %[mod Path]) 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).
+
+Lemma path_final_mono : {mono \pi_Path : f / f 1 >-> path_final f}.
+Proof.
+move=> f; unlock path_final.
+have : ((repr (\pi_(Path) f)) = f %[mod Path]) 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] ).
+
+Lemma path_image_mono : {mono \pi_Path : 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]. 
+    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]. 
+  by rewrite reprK.
+(exists (gamma w); last exact: fg); exact: (@funS _ _ _ _ gamma).
+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 JustPath {R : realType} {T : topologicalType} 
-  := {f of @IsPath R T 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}.