Library HoTT.Misc.UStructures

Uniform Structures

Require Import Basics Types.
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 : ∀ n : nat , Reflexive (us_rel n);
  us_symmetric : ∀ n : nat , Symmetric (us_rel n);
  us_transitive : ∀ n : nat , Transitive (us_rel n);
  us_pred : ∀ (n : nat) (x y : us_type ), us_rel n .+1 x y → us_rel n x y
}.

Existing Instances us_reflexive us_symmetric us_transitive.

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.
Proof.
  induction hm.
  - assumption.
  - apply IHhm.
    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.
Proof.
srapply (Build_UStructure _ (fun n x y ⇒ (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.
Proof.
  srapply (Build_UStructure X
            (fun n x y ⇒ Tr (trunc_index_inc (-2) n) (x = y))).
  - intros n x. exact (tr idpath).
  - intros n x y h; strip_truncations.
    exact (tr h^).
  - intros n x y z h1 h2; strip_truncations.
    exact (tr (h1 @ h2)).
  - intros n x y h; strip_truncations.
    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)
  := ∀ (u : X) (m : nat ),
      {n : nat & ∀ 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)
  := ∀ (m : nat ),
      {n : nat & ∀ 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)
  := ∀ 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 ).