(** * Uniform Structures *)

Require Import Basics Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Truncations.Core.
Require Import Spaces.Nat.Core.

Local Open Scope nat_scope.

(** ** [nat]-graded uniform structures *)

(** A uniform structure on a type consists of an equivalence relation for every natural number, each one being stronger than its predecessor. *)
Class UStructure (us_type : Type) := {
  us_rel : nat -> Relation us_type;
  us_reflexive :: forall n : nat, Reflexive (us_rel n);
  us_symmetric :: forall n : nat, Symmetric (us_rel n);
  us_transitive :: forall n : nat, Transitive (us_rel n);
  us_pred : forall (n : nat) (x y : us_type), us_rel n.+1 x y -> us_rel n x y
}.

Notation "u =[ n ] v" := (us_rel n u v)
  (at level 70, format "u  =[ n ]  v").

Definition us_rel_leq {X : Type} {struct : UStructure X}
  {m n : nat} (hm : m <= n) {u v : X} (h : u =[n] v)
  : u =[m] v.
X: Type
struct: UStructure X
m, n: nat
hm: m <= n
u, v: X
h: u =[n] v
u =[m] v
Proof.
X: Type
struct: UStructure X
m, n: nat
hm: m <= n
u, v: X
h: u =[n] v
u =[m] v
  induction hm.
X: Type
struct: UStructure X
m: nat
u, v: X
h: u =[m] v
u =[m] v
X: Type
struct: UStructure X
m, m0: nat
hm: m <= m0
u, v: X
h: u =[m0.+1] v
IHhm: u =[m0] v -> u =[m] v
u =[m] v
  -
X: Type
struct: UStructure X
m: nat
u, v: X
h: u =[m] v
u =[m] v assumption.
  -
X: Type
struct: UStructure X
m, m0: nat
hm: m <= m0
u, v: X
h: u =[m0.+1] v
IHhm: u =[m0] v -> u =[m] v
u =[m] v apply IHhm.
X: Type
struct: UStructure X
m, m0: nat
hm: m <= m0
u, v: X
h: u =[m0.+1] v
IHhm: u =[m0] v -> u =[m] v
u =[m0] v
    by apply us_pred.
Defined.

(** Every type admits the trivial uniform structure with the standard identity type on every level. *)
Instance trivial_us {X : Type} : UStructure X | 100.
X: Type
UStructure X
Proof.
X: Type
UStructure X
  srapply (Build_UStructure _ (fun n x y => (x = y))).
X: Type
forall (n : nat) (x y : X),
(fun (_ : nat) (x0 y0 : X) => x0 = y0) n.+1 x y ->
(fun (_ : nat) (x0 y0 : X) => x0 = y0) n x y
  exact (fun _ _ _ => idmap).
Defined.

(** Example of a uniform structures based on truncations, with the relation being the [n-2]-truncation of the identity type. *)
Definition trunc_us {X : Type} : UStructure X.
X: Type
UStructure X
Proof.
X: Type
UStructure X
  srapply (Build_UStructure X
            (fun n x y => Tr (trunc_index_inc (-2) n) (x = y))).
X: Type
forall n : nat,
Reflexive
  ((fun (n0 : nat) (x y : X) =>
    Tr (trunc_index_inc (-2) n0) (x = y)) n)
X: Type
forall n : nat,
Symmetric
  ((fun (n0 : nat) (x y : X) =>
    Tr (trunc_index_inc (-2) n0) (x = y)) n)
X: Type
forall n : nat,
Transitive
  ((fun (n0 : nat) (x y : X) =>
    Tr (trunc_index_inc (-2) n0) (x = y)) n)
X: Type
forall (n : nat) (x y : X),
(fun (n0 : nat) (x0 y0 : X) =>
 Tr (trunc_index_inc (-2) n0) (x0 = y0)) n.+1 x y ->
(fun (n0 : nat) (x0 y0 : X) =>
 Tr (trunc_index_inc (-2) n0) (x0 = y0)) n x y
  -
X: Type
forall n : nat,
Reflexive
  ((fun (n0 : nat) (x y : X) =>
    Tr (trunc_index_inc (-2) n0) (x = y)) n) intros n x.
X: Type
n: nat
x: X
Tr (trunc_index_inc (-2) n) (x = x) exact (tr idpath).
  -
X: Type
forall n : nat,
Symmetric
  ((fun (n0 : nat) (x y : X) =>
    Tr (trunc_index_inc (-2) n0) (x = y)) n) intros n x y h; strip_truncations.
X: Type
n: nat
x, y: X
h: x = y
Tr (trunc_index_inc (-2) n) (y = x)
    exact (tr h^).
  -
X: Type
forall n : nat,
Transitive
  ((fun (n0 : nat) (x y : X) =>
    Tr (trunc_index_inc (-2) n0) (x = y)) n) intros n x y z h1 h2; strip_truncations.
X: Type
n: nat
x, y, z: X
h2: y = z
h1: x = y
Tr (trunc_index_inc (-2) n) (x = z)
    exact (tr (h1 @ h2)).
  -
X: Type
forall (n : nat) (x y : X),
(fun (n0 : nat) (x0 y0 : X) =>
 Tr (trunc_index_inc (-2) n0) (x0 = y0)) n.+1 x y ->
(fun (n0 : nat) (x0 y0 : X) =>
 Tr (trunc_index_inc (-2) n0) (x0 = y0)) n x y intros n x y h; strip_truncations.
X: Type
n: nat
x, y: X
h: x = y
Tr (trunc_index_inc (-2) n) (x = y)
    exact (tr h).
Defined.

(** ** Continuity *)

(** Definition of a continuous function depending on two uniform structures. *)
Definition IsContinuous
  {X Y : Type} {usX : UStructure X} {usY : UStructure Y} (p : X -> Y)
  := forall (u : X) (m : nat),
      {n : nat & forall v : X, u =[n] v -> p u =[m] p v}.

Definition uniformly_continuous {X Y : Type}
  {usX : UStructure X} {usY : UStructure Y} (p : X -> Y)
  := forall (m : nat),
      {n : nat & forall u v : X, u =[n] v -> p u =[m] p v}.

(** In the case that the target has the trivial uniform structure, it is useful to state uniform continuity by providing the specific modulus, which now only depends on the function. *)
Definition is_modulus_of_uniform_continuity {X Y : Type} {usX : UStructure X}
  (n : nat) (p : X -> Y)
  := forall u v : X, u =[n] v -> p u = p v.

Definition uniformly_continuous_has_modulus {X Y :Type} {usX : UStructure X}
  {p : X -> Y} {n : nat} (c : is_modulus_of_uniform_continuity n p)
  : uniformly_continuous p
  := fun m => (n; c).

Definition iscontinuous_uniformly_continuous {X Y : Type}
  {usX : UStructure X} {usY : UStructure Y} (p : X -> Y)
  : uniformly_continuous p -> IsContinuous p
  := fun uc u m => ((uc m).1 ; fun v => (uc m).2 u v).