Require Import
  HoTT.Classes.interfaces.abstract_algebra
  HoTT.Classes.interfaces.rationals
  HoTT.Classes.interfaces.orders
  HoTT.Classes.implementations.peano_naturals
  HoTT.Classes.implementations.natpair_integers
  HoTT.Classes.theory.groups
  HoTT.Classes.theory.integers
  HoTT.Classes.theory.dec_fields
  HoTT.Classes.orders.dec_fields
  HoTT.Classes.orders.sum
  HoTT.Classes.theory.rationals
  HoTT.Classes.orders.lattices
  HoTT.Classes.implementations.assume_rationals
  HoTT.Classes.tactics.ring_quote
  HoTT.Classes.tactics.ring_tac.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

Import NatPair.Instances.
Import Quoting.Instances.
Generalizable Variables A B.

Local Set Universe Minimization ToSet.


Class Closeness@{i} (A : Type@{i}) := close : Q+ -> Relation@{i i} A.

Global Instance Q_close@{} : Closeness Q := fun e q r => - ' e < q - r < ' e.

Class Separated A `{Closeness A}
  := separated : forall x y, (forall e, close e x y) -> x = y :> A.

Class Triangular A `{Closeness A}
  := triangular : forall u v w e d, close e u v -> close d v w ->
  close (e+d) u w.

Class Rounded@{i j} (A:Type@{i}) `{Closeness A}
  := rounded : forall e u v, iff@{i j j} (close e u v)
    (merely@{j} (sig@{UQ j} (fun d => sig@{UQ j} (fun d' =>
      e = d + d' /\ close d u v)))).

Class PreMetric@{i j} (A:Type@{i}) {Aclose : Closeness A} :=
  { premetric_prop : forall e, is_mere_relation A (close e)
  ; premetric_refl : forall e, Reflexive (close (A:=A) e)
  ; premetric_symm : forall e, Symmetric (close (A:=A) e)
  ; premetric_separated : Separated A
  ; premetric_triangular : Triangular A
  ; premetric_rounded : Rounded@{i j} A }.
#[export] Existing Instances
  premetric_prop
  premetric_refl
  premetric_symm
  premetric_separated
  premetric_triangular
  premetric_rounded.

Global Instance premetric_hset@{i j} `{Funext}
  {A:Type@{i} } `{PreMetric@{i j} A} : IsHSet A.
H: Funext
A: Type
Aclose: Closeness A
H0: PreMetric A
IsHSet A
Proof.
H: Funext
A: Type
Aclose: Closeness A
H0: PreMetric A
IsHSet A
apply (@HSet.ishset_hrel_subpaths@{j i j} _ (fun x y => forall e, close e x y)).
H: Funext
A: Type
Aclose: Closeness A
H0: PreMetric A
Reflexive (fun x y : A => forall e : Q+, close e x y)
H: Funext
A: Type
Aclose: Closeness A
H0: PreMetric A
forall x y : A, IsHProp (forall e : Q+, close e x y)
H: Funext
A: Type
Aclose: Closeness A
H0: PreMetric A
forall x y : A, (forall e : Q+, close e x y) -> x = y
-
H: Funext
A: Type
Aclose: Closeness A
H0: PreMetric A
Reflexive (fun x y : A => forall e : Q+, close e x y) intros x;reflexivity.
-
H: Funext
A: Type
Aclose: Closeness A
H0: PreMetric A
forall x y : A, IsHProp (forall e : Q+, close e x y) apply _.
-
H: Funext
A: Type
Aclose: Closeness A
H0: PreMetric A
forall x y : A, (forall e : Q+, close e x y) -> x = y apply separated.
Qed.

Record Approximation@{i} (A:Type@{i}) {Aclose : Closeness A} :=
  { approximate :> Q+ -> A
  ; approx_equiv : forall d e, close (d+e) (approximate d) (approximate e) }.

Lemma approx_eq `{Funext} `{Closeness A} `{forall e x y, IsHProp (close e x y)}
  : forall x y : Approximation A,
  approximate _ x = approximate _ y -> x = y.
H: Funext
A: Type
H0: Closeness A
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
forall x y : Approximation A, x = y -> x = y
Proof.
H: Funext
A: Type
H0: Closeness A
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
forall x y : Approximation A, x = y -> x = y
intros [x Ex] [y Ey];simpl;intros E.
H: Funext
A: Type
H0: Closeness A
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
x: Q+ -> A
Ex: forall d e : Q+, close (d + e) (x d) (x e)
y: Q+ -> A
Ey: forall d e : Q+, close (d + e) (y d) (y e)
E: x = y
{| approximate := x; approx_equiv := Ex |} =
{| approximate := y; approx_equiv := Ey |}
destruct E.
H: Funext
A: Type
H0: Closeness A
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
x: Q+ -> A
Ex, Ey: forall d e : Q+, close (d + e) (x d) (x e)
{| approximate := x; approx_equiv := Ex |} =
{| approximate := x; approx_equiv := Ey |} apply ap.
H: Funext
A: Type
H0: Closeness A
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
x: Q+ -> A
Ex, Ey: forall d e : Q+, close (d + e) (x d) (x e)
Ex = Ey apply path_ishprop.
Qed.


Definition IsLimit@{i} {A:Type@{i} } {Aclose : Closeness A}
  (x : Approximation A) (l : A)
  := forall e d : Q+, close (e+d) (x d) l.

Class Lim@{i} (A:Type@{i}) {Aclose : Closeness A} := lim : Approximation A -> A.

Class CauchyComplete@{i} (A:Type@{i}) {Aclose : Closeness A} {Alim : Lim A}
  := cauchy_complete : forall x : Approximation A, IsLimit x (lim x).

Section contents.
Context {funext : Funext} {univalence : Univalence}.

Lemma rounded_plus `{Rounded A} : forall d d' u v, close d u v ->
  close (d+d') u v.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
H0: Rounded A
forall (d d' : Q+) (u v : A),
close d u v -> close (d + d') u v
Proof.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
H0: Rounded A
forall (d d' : Q+) (u v : A),
close d u v -> close (d + d') u v
intros d d' u v xi;apply rounded.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
H0: Rounded A
d, d': Q+
u, v: A
xi: close d u v
merely
  {d0 : Q+ &
  {d'0 : Q+ &
  (((d + d')%mc = (d0 + d'0)%mc) * close d0 u v)%type}}
apply tr;exists d,d';auto.
Qed.

Lemma rounded_le' `{Rounded A}
  : forall e u v, close e u v ->
  forall d, ' e <= ' d -> close d u v.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
H0: Rounded A
forall (e : Q+) (u v : A),
close e u v -> forall d : Q+, ' e ≤ ' d -> close d u v
Proof.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
H0: Rounded A
forall (e : Q+) (u v : A),
close e u v -> forall d : Q+, ' e ≤ ' d -> close d u v
intros e u v xi d E.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
H0: Rounded A
e: Q+
u, v: A
xi: close e u v
d: Q+
E: ' e ≤ ' d
close d u v
apply le_equiv_lt in E.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
H0: Rounded A
e: Q+
u, v: A
xi: close e u v
d: Q+
E: ((' e = ' d) + (' e < ' d))%type
close d u v destruct E as [E|E].
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
H0: Rounded A
e: Q+
u, v: A
xi: close e u v
d: Q+
E: ' e = ' d
close d u v
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
H0: Rounded A
e: Q+
u, v: A
xi: close e u v
d: Q+
E: ' e < ' d
close d u v
-
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
H0: Rounded A
e: Q+
u, v: A
xi: close e u v
d: Q+
E: ' e = ' d
close d u v apply pos_eq in E.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
H0: Rounded A
e: Q+
u, v: A
xi: close e u v
d: Q+
E: e = d
close d u v rewrite <-E;trivial.
-
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
H0: Rounded A
e: Q+
u, v: A
xi: close e u v
d: Q+
E: ' e < ' d
close d u v pose proof (pos_eq _ (_ + _) (Qpos_diff_pr _ _ E)) as E'.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
H0: Rounded A
e: Q+
u, v: A
xi: close e u v
d: Q+
E: ' e < ' d
E': d = e + Qpos_diff (' e) (' d) E
close d u v
  rewrite E'.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
H0: Rounded A
e: Q+
u, v: A
xi: close e u v
d: Q+
E: ' e < ' d
E': d = e + Qpos_diff (' e) (' d) E
close (e + Qpos_diff (' e) (' d) E) u v apply rounded_plus.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
H0: Rounded A
e: Q+
u, v: A
xi: close e u v
d: Q+
E: ' e < ' d
E': d = e + Qpos_diff (' e) (' d) E
close e u v trivial.
Qed.

(* Coq pre 8.8 produces phantom universes, see coq/coq#6483 **)
Definition rounded_le@{i j} := ltac:(first [exact @rounded_le'@{j i Ularge}|
                                            exact @rounded_le'@{j i Ularge j}|
                                            exact @rounded_le'@{i j}]).
Arguments rounded_le {A _ _} e u v _ d _.

Section close_prod.
Universe UA UB i.
Context (A:Type@{UA}) (B:Type@{UB}) `{Closeness A} `{Closeness B}
  `{forall e, is_mere_relation A (close e)}
  `{forall e, is_mere_relation B (close e)}.

Global Instance close_prod@{} : Closeness@{i} (A /\ B)
  := fun e x y => close e (fst x) (fst y) /\ close e (snd x) (snd y).

Global Instance close_prod_refl@{}
  `{forall e, Reflexive (close (A:=A) e)}
  `{forall e, Reflexive (close (A:=B) e)}
  : forall e, Reflexive (close (A:=A /\ B) e).
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
H3, H4: forall e : Q+, Reflexive (close e)
forall e : Q+, Reflexive (close e)
Proof.
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
H3, H4: forall e : Q+, Reflexive (close e)
forall e : Q+, Reflexive (close e)
intros e;split;reflexivity.
Qed.

Global Instance close_prod_symm@{}
  `{forall e, Symmetric (close (A:=A) e)}
  `{forall e, Symmetric (close (A:=B) e)}
  : forall e, Symmetric (close (A:=A /\ B) e).
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
H3, H4: forall e : Q+, Symmetric (close e)
forall e : Q+, Symmetric (close e)
Proof.
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
H3, H4: forall e : Q+, Symmetric (close e)
forall e : Q+, Symmetric (close e)
intros e u v xi;split;symmetry;apply xi.
Qed.

Global Instance close_prod_separated@{}
  `{!Separated A}
  `{!Separated B}
  : Separated (A /\ B).
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
Separated0: Separated A
Separated1: Separated B
Separated (A * B)
Proof.
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
Separated0: Separated A
Separated1: Separated B
Separated (A * B)
intros x y E.
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
Separated0: Separated A
Separated1: Separated B
x, y: (A * B)%type
E: forall e : Q+, close e x y
x = y
apply Prod.path_prod;apply separated;intros;apply E.
Qed.

Global Instance close_prod_triangular@{}
  `{!Triangular A}
  `{!Triangular B}
  : Triangular (A /\ B).
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
Triangular0: Triangular A
Triangular1: Triangular B
Triangular (A * B)
Proof.
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
Triangular0: Triangular A
Triangular1: Triangular B
Triangular (A * B)
intros u v w e d E1 E2;split;(eapply triangular;[apply E1|apply E2]).
Qed.

Lemma close_prod_rounded'
  `{!Rounded A} 
  `{!Rounded B}
  : Rounded (A /\ B).
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
Rounded0: Rounded A
Rounded1: Rounded B
Rounded (A * B)
Proof.
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
Rounded0: Rounded A
Rounded1: Rounded B
Rounded (A * B)
intros e u v.
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
Rounded0: Rounded A
Rounded1: Rounded B
e: Q+
u, v: (A * B)%type
close e u v <->
merely
  {d : Q+ &
  {d' : Q+ & ((e = (d + d')%mc) * close d u v)%type}} split.
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
Rounded0: Rounded A
Rounded1: Rounded B
e: Q+
u, v: (A * B)%type
close e u v ->
merely
  {d : Q+ &
  {d' : Q+ & ((e = (d + d')%mc) * close d u v)%type}}
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
Rounded0: Rounded A
Rounded1: Rounded B
e: Q+
u, v: (A * B)%type
merely
  {d : Q+ &
  {d' : Q+ & ((e = (d + d')%mc) * close d u v)%type}} ->
close e u v
-
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
Rounded0: Rounded A
Rounded1: Rounded B
e: Q+
u, v: (A * B)%type
close e u v ->
merely
  {d : Q+ &
  {d' : Q+ & ((e = (d + d')%mc) * close d u v)%type}} intros [E0 E0'];apply rounded in E0;apply rounded in E0'.
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
Rounded0: Rounded A
Rounded1: Rounded B
e: Q+
u, v: (A * B)%type
E0: merely
  {d : Q+ &
  {d' : Q+ &
  ((e = (d + d')%mc) * close d (fst u) (fst v))%type}}
E0': merely
  {d : Q+ &
  {d' : Q+ &
  ((e = (d + d')%mc) * close d (snd u) (snd v))%type}}
merely
  {d : Q+ &
  {d' : Q+ & ((e = (d + d')%mc) * close d u v)%type}}
  revert E0;apply (Trunc_ind _);intros [d1 [d1' [E1 E2]]].
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
Rounded0: Rounded A
Rounded1: Rounded B
e: Q+
u, v: (A * B)%type
E0': merely
  {d : Q+ &
  {d' : Q+ &
  ((e = (d + d')%mc) * close d (snd u) (snd v))%type}}
d1, d1': Q+
E1: e = d1 + d1'
E2: close d1 (fst u) (fst v)
merely
  {d : Q+ &
  {d' : Q+ & ((e = (d + d')%mc) * close d u v)%type}}
  revert E0';apply (Trunc_ind _);intros [d2 [d2' [E3 E4]]].
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
Rounded0: Rounded A
Rounded1: Rounded B
e: Q+
u, v: (A * B)%type
d1, d1': Q+
E1: e = d1 + d1'
E2: close d1 (fst u) (fst v)
d2, d2': Q+
E3: e = d2 + d2'
E4: close d2 (snd u) (snd v)
merely
  {d : Q+ &
  {d' : Q+ & ((e = (d + d')%mc) * close d u v)%type}}
  apply tr;exists (join d1 d2), (meet d1' d2');split.
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
Rounded0: Rounded A
Rounded1: Rounded B
e: Q+
u, v: (A * B)%type
d1, d1': Q+
E1: e = d1 + d1'
E2: close d1 (fst u) (fst v)
d2, d2': Q+
E3: e = d2 + d2'
E4: close d2 (snd u) (snd v)
e = d1 ⊔ d2 + (d1' ⊓ d2')
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
Rounded0: Rounded A
Rounded1: Rounded B
e: Q+
u, v: (A * B)%type
d1, d1': Q+
E1: e = d1 + d1'
E2: close d1 (fst u) (fst v)
d2, d2': Q+
E3: e = d2 + d2'
E4: close d2 (snd u) (snd v)
close (d1 ⊔ d2) u v
  +
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
Rounded0: Rounded A
Rounded1: Rounded B
e: Q+
u, v: (A * B)%type
d1, d1': Q+
E1: e = d1 + d1'
E2: close d1 (fst u) (fst v)
d2, d2': Q+
E3: e = d2 + d2'
E4: close d2 (snd u) (snd v)
e = d1 ⊔ d2 + (d1' ⊓ d2') rewrite E1.
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
Rounded0: Rounded A
Rounded1: Rounded B
e: Q+
u, v: (A * B)%type
d1, d1': Q+
E1: e = d1 + d1'
E2: close d1 (fst u) (fst v)
d2, d2': Q+
E3: e = d2 + d2'
E4: close d2 (snd u) (snd v)
d1 + d1' = d1 ⊔ d2 + (d1' ⊓ d2') apply Qpos_sum_eq_join_meet.
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
Rounded0: Rounded A
Rounded1: Rounded B
e: Q+
u, v: (A * B)%type
d1, d1': Q+
E1: e = d1 + d1'
E2: close d1 (fst u) (fst v)
d2, d2': Q+
E3: e = d2 + d2'
E4: close d2 (snd u) (snd v)
d1 + d1' = d2 + d2' rewrite <-E1;trivial.
  +
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
Rounded0: Rounded A
Rounded1: Rounded B
e: Q+
u, v: (A * B)%type
d1, d1': Q+
E1: e = d1 + d1'
E2: close d1 (fst u) (fst v)
d2, d2': Q+
E3: e = d2 + d2'
E4: close d2 (snd u) (snd v)
close (d1 ⊔ d2) u v split.
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
Rounded0: Rounded A
Rounded1: Rounded B
e: Q+
u, v: (A * B)%type
d1, d1': Q+
E1: e = d1 + d1'
E2: close d1 (fst u) (fst v)
d2, d2': Q+
E3: e = d2 + d2'
E4: close d2 (snd u) (snd v)
close (d1 ⊔ d2) (fst u) (fst v)
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
Rounded0: Rounded A
Rounded1: Rounded B
e: Q+
u, v: (A * B)%type
d1, d1': Q+
E1: e = d1 + d1'
E2: close d1 (fst u) (fst v)
d2, d2': Q+
E3: e = d2 + d2'
E4: close d2 (snd u) (snd v)
close (d1 ⊔ d2) (snd u) (snd v)
    *
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
Rounded0: Rounded A
Rounded1: Rounded B
e: Q+
u, v: (A * B)%type
d1, d1': Q+
E1: e = d1 + d1'
E2: close d1 (fst u) (fst v)
d2, d2': Q+
E3: e = d2 + d2'
E4: close d2 (snd u) (snd v)
close (d1 ⊔ d2) (fst u) (fst v) apply rounded_le with d1;trivial.
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
Rounded0: Rounded A
Rounded1: Rounded B
e: Q+
u, v: (A * B)%type
d1, d1': Q+
E1: e = d1 + d1'
E2: close d1 (fst u) (fst v)
d2, d2': Q+
E3: e = d2 + d2'
E4: close d2 (snd u) (snd v)
' d1 ≤ ' (d1 ⊔ d2)
      apply join_ub_l.
    *
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
Rounded0: Rounded A
Rounded1: Rounded B
e: Q+
u, v: (A * B)%type
d1, d1': Q+
E1: e = d1 + d1'
E2: close d1 (fst u) (fst v)
d2, d2': Q+
E3: e = d2 + d2'
E4: close d2 (snd u) (snd v)
close (d1 ⊔ d2) (snd u) (snd v) apply rounded_le with d2;trivial.
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
Rounded0: Rounded A
Rounded1: Rounded B
e: Q+
u, v: (A * B)%type
d1, d1': Q+
E1: e = d1 + d1'
E2: close d1 (fst u) (fst v)
d2, d2': Q+
E3: e = d2 + d2'
E4: close d2 (snd u) (snd v)
' d2 ≤ ' (d1 ⊔ d2)
      apply join_ub_r.
-
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
Rounded0: Rounded A
Rounded1: Rounded B
e: Q+
u, v: (A * B)%type
merely
  {d : Q+ &
  {d' : Q+ & ((e = (d + d')%mc) * close d u v)%type}} ->
close e u v apply (Trunc_ind _);intros [d [d' [E1 E2]]].
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
Rounded0: Rounded A
Rounded1: Rounded B
e: Q+
u, v: (A * B)%type
d, d': Q+
E1: e = d + d'
E2: close d u v
close e u v
  rewrite E1;split;apply rounded_plus,E2.
Qed.

(* Coq pre 8.8 produces phantom universes, see coq/coq#6483 **)
Definition close_prod_rounded@{j} := ltac:(first [exact @close_prod_rounded'@{j j j j j}|
                                                  exact @close_prod_rounded'@{j j}|
                                                  exact @close_prod_rounded'@{j j j}]).
Arguments close_prod_rounded {_ _} _ _ _.
Global Existing Instance close_prod_rounded.

Lemma prod_premetric@{j} `{!PreMetric@{UA j} A} `{!PreMetric@{UB j} B}
  : PreMetric@{i j} (A /\ B).
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
PreMetric0: PreMetric A
PreMetric1: PreMetric B
PreMetric (A * B)
Proof.
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
PreMetric0: PreMetric A
PreMetric1: PreMetric B
PreMetric (A * B)
split;try apply _.
Qed.
Global Existing Instance prod_premetric.

Context {Alim : Lim A} {Blim : Lim B}.

Global Instance prod_lim@{} : Lim (A /\ B).
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
Alim: Lim A
Blim: Lim B
Lim (A * B)
Proof.
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
Alim: Lim A
Blim: Lim B
Lim (A * B)
intros xy.
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
Alim: Lim A
Blim: Lim B
xy: Approximation (A * B)
(A * B)%type split;apply lim;
[exists (fun e => fst (xy e))|exists (fun e => snd (xy e))];intros;apply xy.
Defined.

Global Instance prod_cauchy_complete `{!CauchyComplete A} `{!CauchyComplete B}
  : CauchyComplete (A /\ B).
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
Alim: Lim A
Blim: Lim B
CauchyComplete0: CauchyComplete A
CauchyComplete1: CauchyComplete B
CauchyComplete (A * B)
Proof.
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
Alim: Lim A
Blim: Lim B
CauchyComplete0: CauchyComplete A
CauchyComplete1: CauchyComplete B
CauchyComplete (A * B)
intros xy e d;split.
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
Alim: Lim A
Blim: Lim B
CauchyComplete0: CauchyComplete A
CauchyComplete1: CauchyComplete B
xy: Approximation (A * B)
e, d: Q+
close (e + d) (fst (xy d)) (fst (lim xy))
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
Alim: Lim A
Blim: Lim B
CauchyComplete0: CauchyComplete A
CauchyComplete1: CauchyComplete B
xy: Approximation (A * B)
e, d: Q+
close (e + d) (snd (xy d)) (snd (lim xy))
-
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
Alim: Lim A
Blim: Lim B
CauchyComplete0: CauchyComplete A
CauchyComplete1: CauchyComplete B
xy: Approximation (A * B)
e, d: Q+
close (e + d) (fst (xy d)) (fst (lim xy)) apply (cauchy_complete
    {| approximate := fun e0 : Q+ => fst (xy e0); approx_equiv := _ |}).
-
funext: Funext
univalence: Univalence
A, B: Type
H: Closeness A
H0: Closeness B
H1: forall (e : Q+) (x y : A), IsHProp (close e x y)
H2: forall (e : Q+) (x y : B), IsHProp (close e x y)
Alim: Lim A
Blim: Lim B
CauchyComplete0: CauchyComplete A
CauchyComplete1: CauchyComplete B
xy: Approximation (A * B)
e, d: Q+
close (e + d) (snd (xy d)) (snd (lim xy)) apply (cauchy_complete
    {| approximate := fun e0 : Q+ => snd (xy e0); approx_equiv := _ |}).
Qed.

End close_prod.

Section close_arrow.
Context {A:Type} `{Bclose : Closeness B} `{!PreMetric B}.

(* Using [forall x, close e (f x) (g x)] works for closed balls, not open ones. *)
Global Instance close_arrow : Closeness (A -> B)
  := fun e f g => merely (exists d d', e = d + d' /\ forall x, close d (f x) (g x)).

Lemma close_arrow_apply : forall e (f g : A -> B), close e f g ->
  forall x, close e (f x) (g x).
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
forall (e : Q+) (f g : A -> B),
close e f g -> forall x : A, close e (f x) (g x)
Proof.
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
forall (e : Q+) (f g : A -> B),
close e f g -> forall x : A, close e (f x) (g x)
intros e f g E x;revert E;apply (Trunc_ind _);intros [d [d' [E1 E2]]].
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
e: Q+
f, g: A -> B
x: A
d, d': Q+
E1: e = d + d'
E2: forall x : A, close d (f x) (g x)
close e (f x) (g x)
rewrite E1;apply rounded_plus;trivial.
Qed.

Global Instance close_arrow_premetric : PreMetric (A -> B).
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
PreMetric (A -> B)
Proof.
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
PreMetric (A -> B)
split.
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
forall (e : Q+) (x y : A -> B), IsHProp (close e x y)
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
forall e : Q+, Reflexive (close e)
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
forall e : Q+, Symmetric (close e)
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
Separated (A -> B)
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
Triangular (A -> B)
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
Rounded (A -> B)
-
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
forall (e : Q+) (x y : A -> B), IsHProp (close e x y) apply _.
-
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
forall e : Q+, Reflexive (close e) intros e f;apply tr; exists (e/2), (e/2);split.
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
e: Q+
f: A -> B
e = e / 2 + e / 2
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
e: Q+
f: A -> B
forall x : A, close (e / 2) (f x) (f x)
  +
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
e: Q+
f: A -> B
e = e / 2 + e / 2 apply pos_split2.
  +
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
e: Q+
f: A -> B
forall x : A, close (e / 2) (f x) (f x) intros x;reflexivity.
-
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
forall e : Q+, Symmetric (close e) intros e f g;apply (Trunc_ind _);intros [d [d' [E1 E2]]].
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
e: Q+
f, g: A -> B
d, d': Q+
E1: e = d + d'
E2: forall x : A, close d (f x) (g x)
close e g f
  apply tr;exists d, d';split;trivial.
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
e: Q+
f, g: A -> B
d, d': Q+
E1: e = d + d'
E2: forall x : A, close d (f x) (g x)
forall x : A, close d (g x) (f x)
  intros x;symmetry;trivial.
-
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
Separated (A -> B) intros f g E.
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
f, g: A -> B
E: forall e : Q+, close e f g
f = g apply path_forall;intros x.
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
f, g: A -> B
E: forall e : Q+, close e f g
x: A
f x = g x
  apply separated.
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
f, g: A -> B
E: forall e : Q+, close e f g
x: A
forall e : Q+, close e (f x) (g x) intros e.
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
f, g: A -> B
E: forall e : Q+, close e f g
x: A
e: Q+
close e (f x) (g x)
  apply (merely_destruct (E e)).
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
f, g: A -> B
E: forall e : Q+, close e f g
x: A
e: Q+
{d : Q+ &
{d' : Q+ &
((e = (d + d')%mc) *
 (forall x : A, close d (f x) (g x)))%type}} ->
close e (f x) (g x) intros [d [d' [E1 E2]]].
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
f, g: A -> B
E: forall e : Q+, close e f g
x: A
e, d, d': Q+
E1: e = d + d'
E2: forall x : A, close d (f x) (g x)
close e (f x) (g x)
  rewrite E1.
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
f, g: A -> B
E: forall e : Q+, close e f g
x: A
e, d, d': Q+
E1: e = d + d'
E2: forall x : A, close d (f x) (g x)
close (d + d') (f x) (g x) apply rounded_plus.
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
f, g: A -> B
E: forall e : Q+, close e f g
x: A
e, d, d': Q+
E1: e = d + d'
E2: forall x : A, close d (f x) (g x)
close d (f x) (g x) trivial.
-
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
Triangular (A -> B) intros f g h e d E1 E2.
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
f, g, h: A -> B
e, d: Q+
E1: close e f g
E2: close d g h
close (e + d) f h
  apply (merely_destruct E1);intros [d1 [d1' [E3 E4]]].
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
f, g, h: A -> B
e, d: Q+
E1: close e f g
E2: close d g h
d1, d1': Q+
E3: e = d1 + d1'
E4: forall x : A, close d1 (f x) (g x)
close (e + d) f h
  apply (merely_destruct E2);intros [d2 [d2' [E5 E6]]].
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
f, g, h: A -> B
e, d: Q+
E1: close e f g
E2: close d g h
d1, d1': Q+
E3: e = d1 + d1'
E4: forall x : A, close d1 (f x) (g x)
d2, d2': Q+
E5: d = d2 + d2'
E6: forall x : A, close d2 (g x) (h x)
close (e + d) f h
  apply tr;exists (d1+d2),(d1'+d2').
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
f, g, h: A -> B
e, d: Q+
E1: close e f g
E2: close d g h
d1, d1': Q+
E3: e = d1 + d1'
E4: forall x : A, close d1 (f x) (g x)
d2, d2': Q+
E5: d = d2 + d2'
E6: forall x : A, close d2 (g x) (h x)
(((e + d)%mc = (d1 + d2 + (d1' + d2'))%mc) *
 (forall x : A, close (d1 + d2)%mc (f x) (h x)))%type split.
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
f, g, h: A -> B
e, d: Q+
E1: close e f g
E2: close d g h
d1, d1': Q+
E3: e = d1 + d1'
E4: forall x : A, close d1 (f x) (g x)
d2, d2': Q+
E5: d = d2 + d2'
E6: forall x : A, close d2 (g x) (h x)
e + d = d1 + d2 + (d1' + d2')
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
f, g, h: A -> B
e, d: Q+
E1: close e f g
E2: close d g h
d1, d1': Q+
E3: e = d1 + d1'
E4: forall x : A, close d1 (f x) (g x)
d2, d2': Q+
E5: d = d2 + d2'
E6: forall x : A, close d2 (g x) (h x)
forall x : A, close (d1 + d2) (f x) (h x)
  +
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
f, g, h: A -> B
e, d: Q+
E1: close e f g
E2: close d g h
d1, d1': Q+
E3: e = d1 + d1'
E4: forall x : A, close d1 (f x) (g x)
d2, d2': Q+
E5: d = d2 + d2'
E6: forall x : A, close d2 (g x) (h x)
e + d = d1 + d2 + (d1' + d2') rewrite E3,E5.
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
f, g, h: A -> B
e, d: Q+
E1: close e f g
E2: close d g h
d1, d1': Q+
E3: e = d1 + d1'
E4: forall x : A, close d1 (f x) (g x)
d2, d2': Q+
E5: d = d2 + d2'
E6: forall x : A, close d2 (g x) (h x)
d1 + d1' + (d2 + d2') = d1 + d2 + (d1' + d2')
   abstract (apply pos_eq; ring_tac.ring_with_nat).
  +
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
f, g, h: A -> B
e, d: Q+
E1: close e f g
E2: close d g h
d1, d1': Q+
E3: e = d1 + d1'
E4: forall x : A, close d1 (f x) (g x)
d2, d2': Q+
E5: d = d2 + d2'
E6: forall x : A, close d2 (g x) (h x)
forall x : A, close (d1 + d2) (f x) (h x) intros x.
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
f, g, h: A -> B
e, d: Q+
E1: close e f g
E2: close d g h
d1, d1': Q+
E3: e = d1 + d1'
E4: forall x : A, close d1 (f x) (g x)
d2, d2': Q+
E5: d = d2 + d2'
E6: forall x : A, close d2 (g x) (h x)
x: A
close (d1 + d2) (f x) (h x) apply triangular with (g x);trivial.
-
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
Rounded (A -> B) intros e f g.
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
e: Q+
f, g: A -> B
close e f g <->
merely
  {d : Q+ &
  {d' : Q+ & ((e = (d + d')%mc) * close d f g)%type}} split.
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
e: Q+
f, g: A -> B
close e f g ->
merely
  {d : Q+ &
  {d' : Q+ & ((e = (d + d')%mc) * close d f g)%type}}
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
e: Q+
f, g: A -> B
merely
  {d : Q+ &
  {d' : Q+ & ((e = (d + d')%mc) * close d f g)%type}} ->
close e f g
  +
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
e: Q+
f, g: A -> B
close e f g ->
merely
  {d : Q+ &
  {d' : Q+ & ((e = (d + d')%mc) * close d f g)%type}} apply (Trunc_ind _).
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
e: Q+
f, g: A -> B
{d : Q+ &
{d' : Q+ &
((e = (d + d')%mc) *
 (forall x : A, close d (f x) (g x)))%type}} ->
merely
  {d : Q+ &
  {d' : Q+ & ((e = (d + d')%mc) * close d f g)%type}} intros [d [d' [E1 E2]]].
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
e: Q+
f, g: A -> B
d, d': Q+
E1: e = d + d'
E2: forall x : A, close d (f x) (g x)
merely
  {d : Q+ &
  {d' : Q+ & ((e = (d + d')%mc) * close d f g)%type}}
    apply tr;exists (d+d'/2),(d'/2).
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
e: Q+
f, g: A -> B
d, d': Q+
E1: e = d + d'
E2: forall x : A, close d (f x) (g x)
((e = (d + d' / 2 + d' / 2)%mc) *
 close (d + d' / 2)%mc f g)%type split.
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
e: Q+
f, g: A -> B
d, d': Q+
E1: e = d + d'
E2: forall x : A, close d (f x) (g x)
e = d + d' / 2 + d' / 2
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
e: Q+
f, g: A -> B
d, d': Q+
E1: e = d + d'
E2: forall x : A, close d (f x) (g x)
close (d + d' / 2) f g
    *
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
e: Q+
f, g: A -> B
d, d': Q+
E1: e = d + d'
E2: forall x : A, close d (f x) (g x)
e = d + d' / 2 + d' / 2 rewrite <-Qpos_plus_assoc,<-pos_split2.
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
e: Q+
f, g: A -> B
d, d': Q+
E1: e = d + d'
E2: forall x : A, close d (f x) (g x)
e = d + d' exact E1.
    *
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
e: Q+
f, g: A -> B
d, d': Q+
E1: e = d + d'
E2: forall x : A, close d (f x) (g x)
close (d + d' / 2) f g apply tr.
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
e: Q+
f, g: A -> B
d, d': Q+
E1: e = d + d'
E2: forall x : A, close d (f x) (g x)
{d0 : Q+ &
{d'0 : Q+ &
(((d + d' / 2)%mc = (d0 + d'0)%mc) *
 (forall x : A, close d0 (f x) (g x)))%type}} exists d, (d'/2);split;trivial.
  +
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
e: Q+
f, g: A -> B
merely
  {d : Q+ &
  {d' : Q+ & ((e = (d + d')%mc) * close d f g)%type}} ->
close e f g apply (Trunc_ind _);intros [d [d' [E1 E2]]].
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
e: Q+
f, g: A -> B
d, d': Q+
E1: e = d + d'
E2: close d f g
close e f g
    apply tr;exists d,d';split;trivial.
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
e: Q+
f, g: A -> B
d, d': Q+
E1: e = d + d'
E2: close d f g
forall x : A, close d (f x) (g x)
    apply close_arrow_apply.
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
e: Q+
f, g: A -> B
d, d': Q+
E1: e = d + d'
E2: close d f g
close d f g trivial.
Qed.

Context {Blim : Lim B}.

Global Instance arrow_lim : Lim (A -> B).
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
Blim: Lim B
Lim (A -> B)
Proof.
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
Blim: Lim B
Lim (A -> B)
intros f x.
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
Blim: Lim B
f: Approximation (A -> B)
x: A
B apply lim.
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
Blim: Lim B
f: Approximation (A -> B)
x: A
Approximation B exists (fun e => f e x).
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
Blim: Lim B
f: Approximation (A -> B)
x: A
forall d e : Q+, close (d + e) (f d x) (f e x)
intros.
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
Blim: Lim B
f: Approximation (A -> B)
x: A
d, e: Q+
close (d + e) (f d x) (f e x) apply close_arrow_apply.
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
Blim: Lim B
f: Approximation (A -> B)
x: A
d, e: Q+
close (d + e) (f d) (f e) apply approx_equiv.
Defined.
Arguments arrow_lim _ / _.

Context `{!CauchyComplete B}.
Global Instance arrow_cauchy_complete : CauchyComplete (A -> B).
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
Blim: Lim B
CauchyComplete0: CauchyComplete B
CauchyComplete (A -> B)
Proof.
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
Blim: Lim B
CauchyComplete0: CauchyComplete B
CauchyComplete (A -> B)
intros f e d.
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
Blim: Lim B
CauchyComplete0: CauchyComplete B
f: Approximation (A -> B)
e, d: Q+
close (e + d) (f d) (lim f)
unfold lim;simpl.
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
Blim: Lim B
CauchyComplete0: CauchyComplete B
f: Approximation (A -> B)
e, d: Q+
close (e + d) (f d)
  (fun x : A =>
   lim
     {|
       approximate := fun e : Q+ => f e x;
       approx_equiv :=
         fun d e : Q+ =>
         close_arrow_apply (d + e) (f d) (f e)
           (approx_equiv (A -> B) f d e) x
     |})
apply tr.
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
Blim: Lim B
CauchyComplete0: CauchyComplete B
f: Approximation (A -> B)
e, d: Q+
{d0 : Q+ &
{d' : Q+ &
(((e + d)%mc = (d0 + d')%mc) *
 (forall x : A,
  close d0 (f d x)
    (lim
       {|
         approximate := fun e : Q+ => f e x;
         approx_equiv :=
           fun d e : Q+ =>
           close_arrow_apply (d + e)%mc (f d) (f e)
             (approx_equiv (A -> B) f d e) x
       |})))%type}} exists (e/2 + d), (e/2).
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
Blim: Lim B
CauchyComplete0: CauchyComplete B
f: Approximation (A -> B)
e, d: Q+
(((e + d)%mc = (e / 2 + d + e / 2)%mc) *
 (forall x : A,
  close (e / 2 + d)%mc (f d x)
    (lim
       {|
         approximate := fun e : Q+ => f e x;
         approx_equiv :=
           fun d e : Q+ =>
           close_arrow_apply (d + e)%mc (f d) (f e)
             (approx_equiv (A -> B) f d e) x
       |})))%type split.
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
Blim: Lim B
CauchyComplete0: CauchyComplete B
f: Approximation (A -> B)
e, d: Q+
e + d = e / 2 + d + e / 2
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
Blim: Lim B
CauchyComplete0: CauchyComplete B
f: Approximation (A -> B)
e, d: Q+
forall x : A,
close (e / 2 + d) (f d x)
  (lim
     {|
       approximate := fun e : Q+ => f e x;
       approx_equiv :=
         fun d e : Q+ =>
         close_arrow_apply 
           (d + e) (f d) 
           (f e) (approx_equiv (A -> B) f d e) x
     |})
+
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
Blim: Lim B
CauchyComplete0: CauchyComplete B
f: Approximation (A -> B)
e, d: Q+
e + d = e / 2 + d + e / 2 abstract (set (e' := e/2);rewrite (pos_split2 e);unfold e';
  apply pos_eq;ring_tac.ring_with_nat).
+
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
Blim: Lim B
CauchyComplete0: CauchyComplete B
f: Approximation (A -> B)
e, d: Q+
forall x : A,
close (e / 2 + d) (f d x)
  (lim
     {|
       approximate := fun e : Q+ => f e x;
       approx_equiv :=
         fun d e : Q+ =>
         close_arrow_apply (d + e) (f d) (f e)
           (approx_equiv (A -> B) f d e) x
     |}) intros x.
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
Blim: Lim B
CauchyComplete0: CauchyComplete B
f: Approximation (A -> B)
e, d: Q+
x: A
close (e / 2 + d) (f d x)
  (lim
     {|
       approximate := fun e : Q+ => f e x;
       approx_equiv :=
         fun d e : Q+ =>
         close_arrow_apply (d + e) (f d) (f e)
           (approx_equiv (A -> B) f d e) x
     |})
  set (S := {| approximate := fun e0 : Q+ => (f e0) x
            ;  approx_equiv := _ |}).
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
Blim: Lim B
CauchyComplete0: CauchyComplete B
f: Approximation (A -> B)
e, d: Q+
x: A
S:= {|
  approximate := fun e0 : Q+ => f e0 x;
  approx_equiv :=
    fun d e : Q+ =>
    close_arrow_apply (d + e) 
      (f d) (f e) (approx_equiv (A -> B) f d e) x
|}: Approximation B
close (e / 2 + d) (f d x) (lim S)
  pose proof (cauchy_complete S) as E;red in E.
funext: Funext
univalence: Univalence
A, B: Type
Bclose: Closeness B
PreMetric0: PreMetric B
Blim: Lim B
CauchyComplete0: CauchyComplete B
f: Approximation (A -> B)
e, d: Q+
x: A
S:= {|
  approximate := fun e0 : Q+ => f e0 x;
  approx_equiv :=
    fun d e : Q+ =>
    close_arrow_apply (d + e) 
      (f d) (f e) (approx_equiv (A -> B) f d e) x
|}: Approximation B
E: forall e d : Q+, close (e + d) (S d) (lim S)
close (e / 2 + d) (f d x) (lim S)
  apply E.
Qed.

End close_arrow.

Class NonExpanding `{Closeness A} `{Closeness B} (f : A -> B)
  := non_expanding : forall e x y, close e x y -> close e (f x) (f y).
Arguments non_expanding {A _ B _} f {_ e x y} _.

Class Lipschitz `{Closeness A} `{Closeness B} (f : A -> B) (L : Q+)
  := lipschitz : forall e x y, close e x y -> close (L * e) (f x) (f y).
Arguments lipschitz {A _ B _} f L {_ e x y} _.

Class Uniform `{Closeness A} `{Closeness B} (f : A -> B) (mu : Q+ -> Q+)
  := uniform : forall e x y, close (mu e) x y -> close e (f x) (f y).
Arguments uniform {A _ B _} f mu {_} _ _ _ _.

Class Continuous@{UA UB}
  {A:Type@{UA} } `{Closeness A}
  {B:Type@{UB} } `{Closeness B} (f : A -> B)
  := continuous : forall u e, merely@{Ularge} (sig@{UQ Ularge}
    (fun d => forall v, close d u v ->
    close e (f u) (f v))).
Arguments continuous {A _ B _} f {_} _ _.

Definition BinaryDup@{i} {A : Type@{i} } : A -> A /\ A := fun x => (x, x).
Definition uncurry {A B C} (f : A -> B -> C) : A /\ B -> C
  := fun x => f (fst x) (snd x).
Definition map2 {A B C D} (f : A -> C) (g : B -> D) : A /\ B -> C /\ D
  := fun x => (f (fst x), g (snd x)).

Section closeness.
Universe UA.
Context {A:Type@{UA} } `{Closeness A}.

Global Instance id_nonexpanding : NonExpanding (@id A).
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
NonExpanding id
Proof.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
NonExpanding id
hnf;trivial.
Qed.

Global Instance BinaryDup_nonexpanding@{} : NonExpanding (@BinaryDup A).
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
NonExpanding BinaryDup
Proof.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
NonExpanding BinaryDup
intros e x y E;split;exact E.
Qed.

Universe UB.
Context {B:Type@{UB} } `{Closeness B} (f : A -> B).

Lemma nonexpanding_lipschitz' `{!NonExpanding f}
  : Lipschitz f 1.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
f: A -> B
NonExpanding0: NonExpanding f
Lipschitz f 1
Proof.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
f: A -> B
NonExpanding0: NonExpanding f
Lipschitz f 1
red.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
f: A -> B
NonExpanding0: NonExpanding f
forall (e : Q+) (x y : A),
close e x y -> close (1 * e) (f x) (f y) intro;rewrite left_identity;apply non_expanding,_.
Qed.

Definition nonexpanding_lipschitz@{} `{!NonExpanding f}
  : Lipschitz f 1
  := ltac:(first [exact nonexpanding_lipschitz'@{Ularge}|
                  exact nonexpanding_lipschitz'@{}]).
Global Existing Instance nonexpanding_lipschitz.


Lemma lipschitz_nonexpanding@{} `{!Lipschitz f 1} : NonExpanding f.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
f: A -> B
Lipschitz0: Lipschitz f 1
NonExpanding f
Proof.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
f: A -> B
Lipschitz0: Lipschitz f 1
NonExpanding f
red.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
f: A -> B
Lipschitz0: Lipschitz f 1
forall (e : Q+) (x y : A),
close e x y -> close e (f x) (f y) intros e x y E;rewrite <-(left_identity e).
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
f: A -> B
Lipschitz0: Lipschitz f 1
e: Q+
x, y: A
E: close e x y
close (1 * e) (f x) (f y) apply (lipschitz f 1 E).
Qed.

Global Instance const_nonexpanding@{} `{forall e, Reflexive (close (A:=B) e)}
  (b : B) : NonExpanding (fun _ : A => b).
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
f: A -> B
H1: forall e : Q+, Reflexive (close e)
b: B
NonExpanding (fun _ : A => b)
Proof.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
f: A -> B
H1: forall e : Q+, Reflexive (close e)
b: B
NonExpanding (fun _ : A => b)
hnf.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
f: A -> B
H1: forall e : Q+, Reflexive (close e)
b: B
forall (e : Q+) (x y : A), close e x y -> close e b b intros;reflexivity.
Qed.

Global Instance lipschitz_const@{} `{forall e, Reflexive (close (A:=B) e)}
  : forall (b:B) (L:Q+), Lipschitz (fun _ : A => b) L.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
f: A -> B
H1: forall e : Q+, Reflexive (close e)
forall (b : B) (L : Q+), Lipschitz (fun _ : A => b) L
Proof.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
f: A -> B
H1: forall e : Q+, Reflexive (close e)
forall (b : B) (L : Q+), Lipschitz (fun _ : A => b) L
intros;hnf.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
f: A -> B
H1: forall e : Q+, Reflexive (close e)
b: B
L: Q+
forall (e : Q+) (x y : A),
close e x y -> close (L * e) b b
intros e _ _ _.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
f: A -> B
H1: forall e : Q+, Reflexive (close e)
b: B
L, e: Q+
close (L * e) b b reflexivity.
Qed.

Global Instance lipschitz_uniform@{} (L:Q+) `{!Lipschitz f L}
  : Uniform f (fun e => e / L) | 5.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
f: A -> B
L: Q+
Lipschitz0: Lipschitz f L
Uniform f (fun e : Q+ => e / L)
Proof.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
f: A -> B
L: Q+
Lipschitz0: Lipschitz f L
Uniform f (fun e : Q+ => e / L)
intros e u v xi.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
f: A -> B
L: Q+
Lipschitz0: Lipschitz f L
e: Q+
u, v: A
xi: close (e / L) u v
close e (f u) (f v)
rewrite <-(pos_unconjugate L e),<-Qpos_mult_assoc.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
f: A -> B
L: Q+
Lipschitz0: Lipschitz f L
e: Q+
u, v: A
xi: close (e / L) u v
close (L * (e / L)) (f u) (f v)
apply (lipschitz f L),xi.
Qed.

Lemma uniform_continuous@{} mu `{!Uniform@{UA UB} f mu} : Continuous f.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
f: A -> B
mu: Q+ -> Q+
Uniform0: Uniform f mu
Continuous f
Proof.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
f: A -> B
mu: Q+ -> Q+
Uniform0: Uniform f mu
Continuous f
hnf.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
f: A -> B
mu: Q+ -> Q+
Uniform0: Uniform f mu
forall (u : A) (e : Q+),
merely
  {d : Q+ &
  forall v : A, close d u v -> close e (f u) (f v)}
intros u e;apply tr;exists (mu e).
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
f: A -> B
mu: Q+ -> Q+
Uniform0: Uniform f mu
u: A
e: Q+
forall v : A, close (mu e) u v -> close e (f u) (f v)
apply (uniform f mu).
Qed.
Global Existing Instance uniform_continuous | 5.

Definition lipschitz_continuous@{} (L:Q+) `{!Lipschitz f L} : Continuous f
  := _.

Definition nonexpanding_continuous@{} `{!NonExpanding f} : Continuous f
  := _.

End closeness.

Section compositions.
Universe UA.
Context {A:Type@{UA} } `{Closeness A}.
Universe UB.
Context {B:Type@{UB} } `{Closeness B}.
Universe UC.
Context {C:Type@{UC} } `{Closeness C} (g : B -> C) (f : A -> B).

Global Instance nonexpanding_compose@{}
  {Eg : NonExpanding g} {Ef : NonExpanding f}
  : NonExpanding (Compose g f).
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
g: B -> C
f: A -> B
Eg: NonExpanding g
Ef: NonExpanding f
NonExpanding (g ∘ f)
Proof.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
g: B -> C
f: A -> B
Eg: NonExpanding g
Ef: NonExpanding f
NonExpanding (g ∘ f)
hnf.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
g: B -> C
f: A -> B
Eg: NonExpanding g
Ef: NonExpanding f
forall (e : Q+) (x y : A),
close e x y -> close e ((g ∘ f) x) ((g ∘ f) y) intros e x y xi;exact (non_expanding g (non_expanding f xi)).
Qed.

Global Instance lipschitz_compose@{}
  Lg {Eg : Lipschitz g Lg} Lf {Ef : Lipschitz f Lf}
  : Lipschitz (Compose g f) (Lg * Lf).
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
g: B -> C
f: A -> B
Lg: Q+
Eg: Lipschitz g Lg
Lf: Q+
Ef: Lipschitz f Lf
Lipschitz (g ∘ f) (Lg * Lf)
Proof.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
g: B -> C
f: A -> B
Lg: Q+
Eg: Lipschitz g Lg
Lf: Q+
Ef: Lipschitz f Lf
Lipschitz (g ∘ f) (Lg * Lf)
intros ??? He.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
g: B -> C
f: A -> B
Lg: Q+
Eg: Lipschitz g Lg
Lf: Q+
Ef: Lipschitz f Lf
e: Q+
x, y: A
He: close e x y
close (Lg * Lf * e) ((g ∘ f) x) ((g ∘ f) y)
unfold Compose;apply Ef,Eg in He.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
g: B -> C
f: A -> B
Lg: Q+
Eg: Lipschitz g Lg
Lf: Q+
Ef: Lipschitz f Lf
e: Q+
x, y: A
He: close (Lg * (Lf * e)) (g (f x)) (g (f y))
close (Lg * Lf * e) (g (f x)) (g (f y))
pattern (Lg * Lf * e).
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
g: B -> C
f: A -> B
Lg: Q+
Eg: Lipschitz g Lg
Lf: Q+
Ef: Lipschitz f Lf
e: Q+
x, y: A
He: close (Lg * (Lf * e)) (g (f x)) (g (f y))
(fun q : Q+ => close q (g (f x)) (g (f y)))
  (Lg * Lf * e)
eapply transport;[|exact He].
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
g: B -> C
f: A -> B
Lg: Q+
Eg: Lipschitz g Lg
Lf: Q+
Ef: Lipschitz f Lf
e: Q+
x, y: A
He: close (Lg * (Lf * e)) (g (f x)) (g (f y))
Lg * (Lf * e) = Lg * Lf * e
apply associativity.
Qed.

Lemma lipschitz_compose_nonexpanding_r'
  L {Eg : Lipschitz g L} {Ef : NonExpanding f}
  : Lipschitz (Compose g f) L.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
g: B -> C
f: A -> B
L: Q+
Eg: Lipschitz g L
Ef: NonExpanding f
Lipschitz (g ∘ f) L
Proof.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
g: B -> C
f: A -> B
L: Q+
Eg: Lipschitz g L
Ef: NonExpanding f
Lipschitz (g ∘ f) L
rewrite <-(left_identity L),commutativity.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
g: B -> C
f: A -> B
L: Q+
Eg: Lipschitz g L
Ef: NonExpanding f
Lipschitz (g ∘ f) (L * 1) apply _.
Qed.

Global Instance lipschitz_compose_nonexpanding_r@{}
  L {Eg : Lipschitz g L} {Ef : NonExpanding f}
  : Lipschitz (Compose g f) L
  := ltac:(first [exact (lipschitz_compose_nonexpanding_r'@{Ularge} L)|
                  exact (lipschitz_compose_nonexpanding_r'@{} L)]).

Lemma lipschitz_compose_nonexpanding_l'
  L {Eg : NonExpanding g} {Ef : Lipschitz f L}
  : Lipschitz (Compose g f) L.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
g: B -> C
f: A -> B
L: Q+
Eg: NonExpanding g
Ef: Lipschitz f L
Lipschitz (g ∘ f) L
Proof.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
g: B -> C
f: A -> B
L: Q+
Eg: NonExpanding g
Ef: Lipschitz f L
Lipschitz (g ∘ f) L
rewrite <-(left_identity L).
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
g: B -> C
f: A -> B
L: Q+
Eg: NonExpanding g
Ef: Lipschitz f L
Lipschitz (g ∘ f) (1 * L) apply _.
Qed.

Global Instance lipschitz_compose_nonexpanding_l@{}
  L {Eg : NonExpanding g} {Ef : Lipschitz f L}
  : Lipschitz (Compose g f) L
  := ltac:(first [exact (lipschitz_compose_nonexpanding_l'@{Ularge} L)|
                  exact (lipschitz_compose_nonexpanding_l'@{} L)]).

Lemma uniform_compose@{} mu {Eg : Uniform g mu} mu' {Ef : Uniform f mu'}
  : Uniform (Compose g f) (Compose mu' mu).
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
g: B -> C
f: A -> B
mu: Q+ -> Q+
Eg: Uniform g mu
mu': Q+ -> Q+
Ef: Uniform f mu'
Uniform (g ∘ f) (mu' ∘ mu)
Proof.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
g: B -> C
f: A -> B
mu: Q+ -> Q+
Eg: Uniform g mu
mu': Q+ -> Q+
Ef: Uniform f mu'
Uniform (g ∘ f) (mu' ∘ mu)
intros e u v xi.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
g: B -> C
f: A -> B
mu: Q+ -> Q+
Eg: Uniform g mu
mu': Q+ -> Q+
Ef: Uniform f mu'
e: Q+
u, v: A
xi: close ((mu' ∘ mu) e) u v
close e ((g ∘ f) u) ((g ∘ f) v) unfold Compose.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
g: B -> C
f: A -> B
mu: Q+ -> Q+
Eg: Uniform g mu
mu': Q+ -> Q+
Ef: Uniform f mu'
e: Q+
u, v: A
xi: close ((mu' ∘ mu) e) u v
close e (g (f u)) (g (f v))
apply (uniform g _),(uniform f _),xi.
Qed.
Global Existing Instance uniform_compose.

Global Instance continuous_compose@{} {Eg : Continuous g} {Ef : Continuous f}
  : Continuous (Compose g f).
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
g: B -> C
f: A -> B
Eg: Continuous g
Ef: Continuous f
Continuous (g ∘ f)
Proof.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
g: B -> C
f: A -> B
Eg: Continuous g
Ef: Continuous f
Continuous (g ∘ f)
intros u e.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
g: B -> C
f: A -> B
Eg: Continuous g
Ef: Continuous f
u: A
e: Q+
merely
  {d : Q+ &
  forall v : A,
  close d u v -> close e ((g ∘ f) u) ((g ∘ f) v)}
apply (merely_destruct (continuous g (f u) e)).
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
g: B -> C
f: A -> B
Eg: Continuous g
Ef: Continuous f
u: A
e: Q+
{d : Q+ &
forall v : B,
close d (f u) v -> close e (g (f u)) (g v)} ->
merely
  {d : Q+ &
  forall v : A,
  close d u v -> close e ((g ∘ f) u) ((g ∘ f) v)}
intros [d E].
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
g: B -> C
f: A -> B
Eg: Continuous g
Ef: Continuous f
u: A
e, d: Q+
E: forall v : B,
close d (f u) v -> close e (g (f u)) (g v)
merely
  {d : Q+ &
  forall v : A,
  close d u v -> close e ((g ∘ f) u) ((g ∘ f) v)}
apply (merely_destruct (continuous f u d)).
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
g: B -> C
f: A -> B
Eg: Continuous g
Ef: Continuous f
u: A
e, d: Q+
E: forall v : B,
close d (f u) v -> close e (g (f u)) (g v)
{d0 : Q+ &
forall v : A, close d0 u v -> close d (f u) (f v)} ->
merely
  {d : Q+ &
  forall v : A,
  close d u v -> close e ((g ∘ f) u) ((g ∘ f) v)}
intros [d' E'].
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
g: B -> C
f: A -> B
Eg: Continuous g
Ef: Continuous f
u: A
e, d: Q+
E: forall v : B,
close d (f u) v -> close e (g (f u)) (g v)
d': Q+
E': forall v : A, close d' u v -> close d (f u) (f v)
merely
  {d : Q+ &
  forall v : A,
  close d u v -> close e ((g ∘ f) u) ((g ∘ f) v)}
apply tr;exists d';intros v xi.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
g: B -> C
f: A -> B
Eg: Continuous g
Ef: Continuous f
u: A
e, d: Q+
E: forall v : B,
close d (f u) v -> close e (g (f u)) (g v)
d': Q+
E': forall v : A, close d' u v -> close d (f u) (f v)
v: A
xi: close d' u v
close e ((g ∘ f) u) ((g ∘ f) v)
apply E,E',xi.
Qed.

End compositions.

Section currying.
Universe UA.
Context {A:Type@{UA} } `{Closeness A}.
Universe UB.
Context {B:Type@{UB} } `{Closeness B}.
Universe UC.
Context {C:Type@{UC} } `{Closeness C} `{!Triangular C}.

Global Instance uncurry_lipschitz (f : A -> B -> C) L1 L2
  `{!forall x, Lipschitz (f x) L1}
  `{!forall y, Lipschitz (fun x => f x y) L2}
  : Lipschitz (uncurry f) (L1 + L2).
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
Triangular0: Triangular C
f: A -> B -> C
L1, L2: Q+
H2: forall x : A, Lipschitz (f x) L1
H3: forall y : B, Lipschitz (fun x : A => f x y) L2
Lipschitz (uncurry f) (L1 + L2)
Proof.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
Triangular0: Triangular C
f: A -> B -> C
L1, L2: Q+
H2: forall x : A, Lipschitz (f x) L1
H3: forall y : B, Lipschitz (fun x : A => f x y) L2
Lipschitz (uncurry f) (L1 + L2)
intros e [u1 u2] [v1 v2] [xi1 xi2].
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
Triangular0: Triangular C
f: A -> B -> C
L1, L2: Q+
H2: forall x : A, Lipschitz (f x) L1
H3: forall y : B, Lipschitz (fun x : A => f x y) L2
e: Q+
u1: A
u2: B
v1: A
v2: B
xi1: close e (fst (u1, u2)) (fst (v1, v2))
xi2: close e (snd (u1, u2)) (snd (v1, v2))
close ((L1 + L2) * e) (uncurry f (u1, u2))
  (uncurry f (v1, v2)) simpl in xi1,xi2.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
Triangular0: Triangular C
f: A -> B -> C
L1, L2: Q+
H2: forall x : A, Lipschitz (f x) L1
H3: forall y : B, Lipschitz (fun x : A => f x y) L2
e: Q+
u1: A
u2: B
v1: A
v2: B
xi1: close e u1 v1
xi2: close e u2 v2
close ((L1 + L2) * e) (uncurry f (u1, u2))
  (uncurry f (v1, v2))
unfold uncurry;simpl.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
Triangular0: Triangular C
f: A -> B -> C
L1, L2: Q+
H2: forall x : A, Lipschitz (f x) L1
H3: forall y : B, Lipschitz (fun x : A => f x y) L2
e: Q+
u1: A
u2: B
v1: A
v2: B
xi1: close e u1 v1
xi2: close e u2 v2
close ((L1 + L2) * e) (f u1 u2) (f v1 v2)
assert (Hrw : (L1 + L2) * e = L1 * e + L2 * e)
by abstract (apply pos_eq;ring_tac.ring_with_nat);
rewrite Hrw;clear Hrw.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
Triangular0: Triangular C
f: A -> B -> C
L1, L2: Q+
H2: forall x : A, Lipschitz (f x) L1
H3: forall y : B, Lipschitz (fun x : A => f x y) L2
e: Q+
u1: A
u2: B
v1: A
v2: B
xi1: close e u1 v1
xi2: close e u2 v2
close (L1 * e + L2 * e) (f u1 u2) (f v1 v2)
apply (triangular _ (f u1 v2)).
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
Triangular0: Triangular C
f: A -> B -> C
L1, L2: Q+
H2: forall x : A, Lipschitz (f x) L1
H3: forall y : B, Lipschitz (fun x : A => f x y) L2
e: Q+
u1: A
u2: B
v1: A
v2: B
xi1: close e u1 v1
xi2: close e u2 v2
close (L1 * e) (f u1 u2) (f u1 v2)
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
Triangular0: Triangular C
f: A -> B -> C
L1, L2: Q+
H2: forall x : A, Lipschitz (f x) L1
H3: forall y : B, Lipschitz (fun x : A => f x y) L2
e: Q+
u1: A
u2: B
v1: A
v2: B
xi1: close e u1 v1
xi2: close e u2 v2
close (L2 * e) (f u1 v2) (f v1 v2)
-
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
Triangular0: Triangular C
f: A -> B -> C
L1, L2: Q+
H2: forall x : A, Lipschitz (f x) L1
H3: forall y : B, Lipschitz (fun x : A => f x y) L2
e: Q+
u1: A
u2: B
v1: A
v2: B
xi1: close e u1 v1
xi2: close e u2 v2
close (L1 * e) (f u1 u2) (f u1 v2) apply (lipschitz _ L1).
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
Triangular0: Triangular C
f: A -> B -> C
L1, L2: Q+
H2: forall x : A, Lipschitz (f x) L1
H3: forall y : B, Lipschitz (fun x : A => f x y) L2
e: Q+
u1: A
u2: B
v1: A
v2: B
xi1: close e u1 v1
xi2: close e u2 v2
close e u2 v2 trivial.
-
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
Triangular0: Triangular C
f: A -> B -> C
L1, L2: Q+
H2: forall x : A, Lipschitz (f x) L1
H3: forall y : B, Lipschitz (fun x : A => f x y) L2
e: Q+
u1: A
u2: B
v1: A
v2: B
xi1: close e u1 v1
xi2: close e u2 v2
close (L2 * e) (f u1 v2) (f v1 v2) apply (lipschitz (fun u => f u v2) L2).
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
Triangular0: Triangular C
f: A -> B -> C
L1, L2: Q+
H2: forall x : A, Lipschitz (f x) L1
H3: forall y : B, Lipschitz (fun x : A => f x y) L2
e: Q+
u1: A
u2: B
v1: A
v2: B
xi1: close e u1 v1
xi2: close e u2 v2
close e u1 v1 trivial.
Qed.

Lemma uncurry_uniform
  `{!Rounded A} `{!Rounded B} (f : A -> B -> C) mu mu'
  `{!forall x, Uniform (f x) mu}
  `{!forall y, Uniform (fun x => f x y) mu'}
  : Uniform (uncurry f) (fun e => meet (mu (e/2)) (mu' (e/2))).
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
Triangular0: Triangular C
Rounded0: Rounded A
Rounded1: Rounded B
f: A -> B -> C
mu, mu': Q+ -> Q+
H2: forall x : A, Uniform (f x) mu
H3: forall y : B, Uniform (fun x : A => f x y) mu'
Uniform (uncurry f)
  (fun e : Q+ => mu (e / 2) ⊓ mu' (e / 2))
Proof.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
Triangular0: Triangular C
Rounded0: Rounded A
Rounded1: Rounded B
f: A -> B -> C
mu, mu': Q+ -> Q+
H2: forall x : A, Uniform (f x) mu
H3: forall y : B, Uniform (fun x : A => f x y) mu'
Uniform (uncurry f)
  (fun e : Q+ => mu (e / 2) ⊓ mu' (e / 2))
intros e [u1 u2] [v1 v2] [xi1 xi2].
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
Triangular0: Triangular C
Rounded0: Rounded A
Rounded1: Rounded B
f: A -> B -> C
mu, mu': Q+ -> Q+
H2: forall x : A, Uniform (f x) mu
H3: forall y : B, Uniform (fun x : A => f x y) mu'
e: Q+
u1: A
u2: B
v1: A
v2: B
xi1: close (mu (e / 2) ⊓ mu' (e / 2)) 
  (fst (u1, u2)) (fst (v1, v2))
xi2: close (mu (e / 2) ⊓ mu' (e / 2)) 
  (snd (u1, u2)) (snd (v1, v2))
close e (uncurry f (u1, u2)) (uncurry f (v1, v2))
simpl in *.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
Triangular0: Triangular C
Rounded0: Rounded A
Rounded1: Rounded B
f: A -> B -> C
mu, mu': Q+ -> Q+
H2: forall x : A, Uniform (f x) mu
H3: forall y : B, Uniform (fun x : A => f x y) mu'
e: Q+
u1: A
u2: B
v1: A
v2: B
xi1: close (mu (e / 2) ⊓ mu' (e / 2)) u1 v1
xi2: close (mu (e / 2) ⊓ mu' (e / 2)) u2 v2
close e (uncurry f (u1, u2)) (uncurry f (v1, v2))
rewrite (pos_split2 e).
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
Triangular0: Triangular C
Rounded0: Rounded A
Rounded1: Rounded B
f: A -> B -> C
mu, mu': Q+ -> Q+
H2: forall x : A, Uniform (f x) mu
H3: forall y : B, Uniform (fun x : A => f x y) mu'
e: Q+
u1: A
u2: B
v1: A
v2: B
xi1: close (mu (e / 2) ⊓ mu' (e / 2)) u1 v1
xi2: close (mu (e / 2) ⊓ mu' (e / 2)) u2 v2
close (e / 2 + e / 2) (uncurry f (u1, u2))
  (uncurry f (v1, v2))
apply (triangular _ (f u1 v2)).
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
Triangular0: Triangular C
Rounded0: Rounded A
Rounded1: Rounded B
f: A -> B -> C
mu, mu': Q+ -> Q+
H2: forall x : A, Uniform (f x) mu
H3: forall y : B, Uniform (fun x : A => f x y) mu'
e: Q+
u1: A
u2: B
v1: A
v2: B
xi1: close (mu (e / 2) ⊓ mu' (e / 2)) u1 v1
xi2: close (mu (e / 2) ⊓ mu' (e / 2)) u2 v2
close (e / 2) (uncurry f (u1, u2)) (f u1 v2)
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
Triangular0: Triangular C
Rounded0: Rounded A
Rounded1: Rounded B
f: A -> B -> C
mu, mu': Q+ -> Q+
H2: forall x : A, Uniform (f x) mu
H3: forall y : B, Uniform (fun x : A => f x y) mu'
e: Q+
u1: A
u2: B
v1: A
v2: B
xi1: close (mu (e / 2) ⊓ mu' (e / 2)) u1 v1
xi2: close (mu (e / 2) ⊓ mu' (e / 2)) u2 v2
close (e / 2) (f u1 v2) (uncurry f (v1, v2))
-
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
Triangular0: Triangular C
Rounded0: Rounded A
Rounded1: Rounded B
f: A -> B -> C
mu, mu': Q+ -> Q+
H2: forall x : A, Uniform (f x) mu
H3: forall y : B, Uniform (fun x : A => f x y) mu'
e: Q+
u1: A
u2: B
v1: A
v2: B
xi1: close (mu (e / 2) ⊓ mu' (e / 2)) u1 v1
xi2: close (mu (e / 2) ⊓ mu' (e / 2)) u2 v2
close (e / 2) (uncurry f (u1, u2)) (f u1 v2) apply (uniform (f u1) _).
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
Triangular0: Triangular C
Rounded0: Rounded A
Rounded1: Rounded B
f: A -> B -> C
mu, mu': Q+ -> Q+
H2: forall x : A, Uniform (f x) mu
H3: forall y : B, Uniform (fun x : A => f x y) mu'
e: Q+
u1: A
u2: B
v1: A
v2: B
xi1: close (mu (e / 2) ⊓ mu' (e / 2)) u1 v1
xi2: close (mu (e / 2) ⊓ mu' (e / 2)) u2 v2
close (mu (e / 2)) (snd (u1, u2)) v2
  eapply rounded_le.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
Triangular0: Triangular C
Rounded0: Rounded A
Rounded1: Rounded B
f: A -> B -> C
mu, mu': Q+ -> Q+
H2: forall x : A, Uniform (f x) mu
H3: forall y : B, Uniform (fun x : A => f x y) mu'
e: Q+
u1: A
u2: B
v1: A
v2: B
xi1: close (mu (e / 2) ⊓ mu' (e / 2)) u1 v1
xi2: close (mu (e / 2) ⊓ mu' (e / 2)) u2 v2
close ?e (snd (u1, u2)) v2
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
Triangular0: Triangular C
Rounded0: Rounded A
Rounded1: Rounded B
f: A -> B -> C
mu, mu': Q+ -> Q+
H2: forall x : A, Uniform (f x) mu
H3: forall y : B, Uniform (fun x : A => f x y) mu'
e: Q+
u1: A
u2: B
v1: A
v2: B
xi1: close (mu (e / 2) ⊓ mu' (e / 2)) u1 v1
xi2: close (mu (e / 2) ⊓ mu' (e / 2)) u2 v2
' ?e ≤ ' mu (e / 2)
  +
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
Triangular0: Triangular C
Rounded0: Rounded A
Rounded1: Rounded B
f: A -> B -> C
mu, mu': Q+ -> Q+
H2: forall x : A, Uniform (f x) mu
H3: forall y : B, Uniform (fun x : A => f x y) mu'
e: Q+
u1: A
u2: B
v1: A
v2: B
xi1: close (mu (e / 2) ⊓ mu' (e / 2)) u1 v1
xi2: close (mu (e / 2) ⊓ mu' (e / 2)) u2 v2
close ?e (snd (u1, u2)) v2 exact xi2.
  +
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
Triangular0: Triangular C
Rounded0: Rounded A
Rounded1: Rounded B
f: A -> B -> C
mu, mu': Q+ -> Q+
H2: forall x : A, Uniform (f x) mu
H3: forall y : B, Uniform (fun x : A => f x y) mu'
e: Q+
u1: A
u2: B
v1: A
v2: B
xi1: close (mu (e / 2) ⊓ mu' (e / 2)) u1 v1
xi2: close (mu (e / 2) ⊓ mu' (e / 2)) u2 v2
' (mu (e / 2) ⊓ mu' (e / 2)) ≤ ' mu (e / 2) apply meet_lb_l.
-
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
Triangular0: Triangular C
Rounded0: Rounded A
Rounded1: Rounded B
f: A -> B -> C
mu, mu': Q+ -> Q+
H2: forall x : A, Uniform (f x) mu
H3: forall y : B, Uniform (fun x : A => f x y) mu'
e: Q+
u1: A
u2: B
v1: A
v2: B
xi1: close (mu (e / 2) ⊓ mu' (e / 2)) u1 v1
xi2: close (mu (e / 2) ⊓ mu' (e / 2)) u2 v2
close (e / 2) (f u1 v2) (uncurry f (v1, v2)) apply (uniform (fun v => f v v2) _).
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
Triangular0: Triangular C
Rounded0: Rounded A
Rounded1: Rounded B
f: A -> B -> C
mu, mu': Q+ -> Q+
H2: forall x : A, Uniform (f x) mu
H3: forall y : B, Uniform (fun x : A => f x y) mu'
e: Q+
u1: A
u2: B
v1: A
v2: B
xi1: close (mu (e / 2) ⊓ mu' (e / 2)) u1 v1
xi2: close (mu (e / 2) ⊓ mu' (e / 2)) u2 v2
close (mu' (e / 2)) u1 (fst (v1, v2))
  eapply rounded_le.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
Triangular0: Triangular C
Rounded0: Rounded A
Rounded1: Rounded B
f: A -> B -> C
mu, mu': Q+ -> Q+
H2: forall x : A, Uniform (f x) mu
H3: forall y : B, Uniform (fun x : A => f x y) mu'
e: Q+
u1: A
u2: B
v1: A
v2: B
xi1: close (mu (e / 2) ⊓ mu' (e / 2)) u1 v1
xi2: close (mu (e / 2) ⊓ mu' (e / 2)) u2 v2
close ?e u1 (fst (v1, v2))
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
Triangular0: Triangular C
Rounded0: Rounded A
Rounded1: Rounded B
f: A -> B -> C
mu, mu': Q+ -> Q+
H2: forall x : A, Uniform (f x) mu
H3: forall y : B, Uniform (fun x : A => f x y) mu'
e: Q+
u1: A
u2: B
v1: A
v2: B
xi1: close (mu (e / 2) ⊓ mu' (e / 2)) u1 v1
xi2: close (mu (e / 2) ⊓ mu' (e / 2)) u2 v2
' ?e ≤ ' mu' (e / 2)
  +
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
Triangular0: Triangular C
Rounded0: Rounded A
Rounded1: Rounded B
f: A -> B -> C
mu, mu': Q+ -> Q+
H2: forall x : A, Uniform (f x) mu
H3: forall y : B, Uniform (fun x : A => f x y) mu'
e: Q+
u1: A
u2: B
v1: A
v2: B
xi1: close (mu (e / 2) ⊓ mu' (e / 2)) u1 v1
xi2: close (mu (e / 2) ⊓ mu' (e / 2)) u2 v2
close ?e u1 (fst (v1, v2)) exact xi1.
  +
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
Triangular0: Triangular C
Rounded0: Rounded A
Rounded1: Rounded B
f: A -> B -> C
mu, mu': Q+ -> Q+
H2: forall x : A, Uniform (f x) mu
H3: forall y : B, Uniform (fun x : A => f x y) mu'
e: Q+
u1: A
u2: B
v1: A
v2: B
xi1: close (mu (e / 2) ⊓ mu' (e / 2)) u1 v1
xi2: close (mu (e / 2) ⊓ mu' (e / 2)) u2 v2
' (mu (e / 2) ⊓ mu' (e / 2)) ≤ ' mu' (e / 2) apply meet_lb_r.
Qed.

End currying.

Section pair.
Universe UA.
Context {A:Type@{UA} } `{Closeness A} `{forall e, Reflexive (close (A:=A) e)}.
Universe UB.
Context {B:Type@{UB} } `{Closeness B} `{forall e, Reflexive (close (A:=B) e)}.

Global Instance pair_nonexpanding_l : forall x, NonExpanding (@pair A B x).
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
H0: forall e : Q+, Reflexive (close e)
B: Type
H1: Closeness B
H2: forall e : Q+, Reflexive (close e)
forall x : A, NonExpanding (pair x)
Proof.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
H0: forall e : Q+, Reflexive (close e)
B: Type
H1: Closeness B
H2: forall e : Q+, Reflexive (close e)
forall x : A, NonExpanding (pair x)
intros x e u v xi;split;simpl.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
H0: forall e : Q+, Reflexive (close e)
B: Type
H1: Closeness B
H2: forall e : Q+, Reflexive (close e)
x: A
e: Q+
u, v: B
xi: close e u v
close e x x
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
H0: forall e : Q+, Reflexive (close e)
B: Type
H1: Closeness B
H2: forall e : Q+, Reflexive (close e)
x: A
e: Q+
u, v: B
xi: close e u v
close e u v
-
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
H0: forall e : Q+, Reflexive (close e)
B: Type
H1: Closeness B
H2: forall e : Q+, Reflexive (close e)
x: A
e: Q+
u, v: B
xi: close e u v
close e x x reflexivity.
-
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
H0: forall e : Q+, Reflexive (close e)
B: Type
H1: Closeness B
H2: forall e : Q+, Reflexive (close e)
x: A
e: Q+
u, v: B
xi: close e u v
close e u v exact xi.
Qed.

Global Instance pair_nonexpanding_r : forall y,
  NonExpanding (fun x => @pair A B x y).
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
H0: forall e : Q+, Reflexive (close e)
B: Type
H1: Closeness B
H2: forall e : Q+, Reflexive (close e)
forall y : B, NonExpanding (fun x : A => (x, y))
Proof.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
H0: forall e : Q+, Reflexive (close e)
B: Type
H1: Closeness B
H2: forall e : Q+, Reflexive (close e)
forall y : B, NonExpanding (fun x : A => (x, y))
intros x e u v xi;split;simpl.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
H0: forall e : Q+, Reflexive (close e)
B: Type
H1: Closeness B
H2: forall e : Q+, Reflexive (close e)
x: B
e: Q+
u, v: A
xi: close e u v
close e u v
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
H0: forall e : Q+, Reflexive (close e)
B: Type
H1: Closeness B
H2: forall e : Q+, Reflexive (close e)
x: B
e: Q+
u, v: A
xi: close e u v
close e x x
-
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
H0: forall e : Q+, Reflexive (close e)
B: Type
H1: Closeness B
H2: forall e : Q+, Reflexive (close e)
x: B
e: Q+
u, v: A
xi: close e u v
close e u v exact xi.
-
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
H0: forall e : Q+, Reflexive (close e)
B: Type
H1: Closeness B
H2: forall e : Q+, Reflexive (close e)
x: B
e: Q+
u, v: A
xi: close e u v
close e x x reflexivity.
Qed.

Global Instance fst_nonexpanding : NonExpanding (@fst A B).
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
H0: forall e : Q+, Reflexive (close e)
B: Type
H1: Closeness B
H2: forall e : Q+, Reflexive (close e)
NonExpanding fst
Proof.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
H0: forall e : Q+, Reflexive (close e)
B: Type
H1: Closeness B
H2: forall e : Q+, Reflexive (close e)
NonExpanding fst
intros e u v xi;apply xi.
Qed.

Global Instance snd_nonexpanding : NonExpanding (@snd A B).
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
H0: forall e : Q+, Reflexive (close e)
B: Type
H1: Closeness B
H2: forall e : Q+, Reflexive (close e)
NonExpanding snd
Proof.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
H0: forall e : Q+, Reflexive (close e)
B: Type
H1: Closeness B
H2: forall e : Q+, Reflexive (close e)
NonExpanding snd
intros e u v xi;apply xi.
Qed.

End pair.

Section prod_equiv.
Universe UA.
Context {A:Type@{UA} } `{Closeness A}.
Universe UB.
Context {B:Type@{UB} } `{Closeness B}.

Global Instance equiv_prod_symm_nonexpanding
  : NonExpanding (@Prod.equiv_prod_symm A B).
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
NonExpanding (equiv_prod_symm A B)
Proof.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
NonExpanding (equiv_prod_symm A B)
intros e u v xi;split;apply xi.
Qed.

Global Instance equiv_prod_symm_inv_nonexpanding
  : NonExpanding ((@Prod.equiv_prod_symm A B)^-1).
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
NonExpanding (equiv_prod_symm A B)^-1
Proof.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
NonExpanding (equiv_prod_symm A B)^-1
intros e u v xi;split;apply xi.
Qed.

Universe UC.
Context {C:Type@{UC} } `{Closeness C}.

Global Instance equiv_prod_assoc_nonexpanding
  : NonExpanding (@Prod.equiv_prod_assoc A B C).
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
NonExpanding (equiv_prod_assoc A B C)
Proof.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
NonExpanding (equiv_prod_assoc A B C)
intros e u v xi;repeat split;apply xi.
Qed.

Global Instance equiv_prod_assoc_inc_nonexpanding
  : NonExpanding ((@Prod.equiv_prod_assoc A B C)^-1).
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
NonExpanding (equiv_prod_assoc A B C)^-1
Proof.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
NonExpanding (equiv_prod_assoc A B C)^-1
intros e u v xi;repeat split;apply xi.
Qed.

End prod_equiv.

Section map2.
Universe UA.
Context {A:Type@{UA} } `{Closeness A}.
Universe UB.
Context {B:Type@{UB} } `{Closeness B}.
Universe UC.
Context {C:Type@{UC} } `{Closeness C}.
Universe UD.
Context {D:Type@{UD} } `{Closeness D}.
Variables (f : A -> C) (g : B -> D).

Lemma map2_nonexpanding'
  `{!NonExpanding f} `{!NonExpanding g}
  : NonExpanding (map2 f g).
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
D: Type
H2: Closeness D
f: A -> C
g: B -> D
NonExpanding0: NonExpanding f
NonExpanding1: NonExpanding g
NonExpanding (map2 f g)
Proof.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
D: Type
H2: Closeness D
f: A -> C
g: B -> D
NonExpanding0: NonExpanding f
NonExpanding1: NonExpanding g
NonExpanding (map2 f g)
intros e u v xi;split;simpl; apply (non_expanding _),xi.
Qed.

Definition map2_nonexpanding@{i} := @map2_nonexpanding'@{i i}.
Arguments map2_nonexpanding {_ _} e x y xi.
Global Existing Instance map2_nonexpanding.

Lemma map2_lipschitz' `{!Rounded C} `{!Rounded D} Lf Lg
  `{!Lipschitz f Lf} `{!Lipschitz g Lg}
  : Lipschitz (map2 f g) (join Lf Lg).
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
D: Type
H2: Closeness D
f: A -> C
g: B -> D
Rounded0: Rounded C
Rounded1: Rounded D
Lf, Lg: Q+
Lipschitz0: Lipschitz f Lf
Lipschitz1: Lipschitz g Lg
Lipschitz (map2 f g) (Lf ⊔ Lg)
Proof.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
D: Type
H2: Closeness D
f: A -> C
g: B -> D
Rounded0: Rounded C
Rounded1: Rounded D
Lf, Lg: Q+
Lipschitz0: Lipschitz f Lf
Lipschitz1: Lipschitz g Lg
Lipschitz (map2 f g) (Lf ⊔ Lg)
intros e u v xi.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
D: Type
H2: Closeness D
f: A -> C
g: B -> D
Rounded0: Rounded C
Rounded1: Rounded D
Lf, Lg: Q+
Lipschitz0: Lipschitz f Lf
Lipschitz1: Lipschitz g Lg
e: Q+
u, v: (A * B)%type
xi: close e u v
close ((Lf ⊔ Lg) * e) (map2 f g u) (map2 f g v) split;simpl.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
D: Type
H2: Closeness D
f: A -> C
g: B -> D
Rounded0: Rounded C
Rounded1: Rounded D
Lf, Lg: Q+
Lipschitz0: Lipschitz f Lf
Lipschitz1: Lipschitz g Lg
e: Q+
u, v: (A * B)%type
xi: close e u v
close ((Lf ⊔ Lg) * e) (f (fst u)) (f (fst v))
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
D: Type
H2: Closeness D
f: A -> C
g: B -> D
Rounded0: Rounded C
Rounded1: Rounded D
Lf, Lg: Q+
Lipschitz0: Lipschitz f Lf
Lipschitz1: Lipschitz g Lg
e: Q+
u, v: (A * B)%type
xi: close e u v
close ((Lf ⊔ Lg) * e) (g (snd u)) (g (snd v))
-
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
D: Type
H2: Closeness D
f: A -> C
g: B -> D
Rounded0: Rounded C
Rounded1: Rounded D
Lf, Lg: Q+
Lipschitz0: Lipschitz f Lf
Lipschitz1: Lipschitz g Lg
e: Q+
u, v: (A * B)%type
xi: close e u v
close ((Lf ⊔ Lg) * e) (f (fst u)) (f (fst v)) apply rounded_le with (Lf * e).
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
D: Type
H2: Closeness D
f: A -> C
g: B -> D
Rounded0: Rounded C
Rounded1: Rounded D
Lf, Lg: Q+
Lipschitz0: Lipschitz f Lf
Lipschitz1: Lipschitz g Lg
e: Q+
u, v: (A * B)%type
xi: close e u v
close (Lf * e) (f (fst u)) (f (fst v))
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
D: Type
H2: Closeness D
f: A -> C
g: B -> D
Rounded0: Rounded C
Rounded1: Rounded D
Lf, Lg: Q+
Lipschitz0: Lipschitz f Lf
Lipschitz1: Lipschitz g Lg
e: Q+
u, v: (A * B)%type
xi: close e u v
' (Lf * e) ≤ ' ((Lf ⊔ Lg) * e)
  +
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
D: Type
H2: Closeness D
f: A -> C
g: B -> D
Rounded0: Rounded C
Rounded1: Rounded D
Lf, Lg: Q+
Lipschitz0: Lipschitz f Lf
Lipschitz1: Lipschitz g Lg
e: Q+
u, v: (A * B)%type
xi: close e u v
close (Lf * e) (f (fst u)) (f (fst v)) apply (lipschitz _ _),xi.
  +
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
D: Type
H2: Closeness D
f: A -> C
g: B -> D
Rounded0: Rounded C
Rounded1: Rounded D
Lf, Lg: Q+
Lipschitz0: Lipschitz f Lf
Lipschitz1: Lipschitz g Lg
e: Q+
u, v: (A * B)%type
xi: close e u v
' (Lf * e) ≤ ' ((Lf ⊔ Lg) * e) apply (order_preserving (.* ' e)).
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
D: Type
H2: Closeness D
f: A -> C
g: B -> D
Rounded0: Rounded C
Rounded1: Rounded D
Lf, Lg: Q+
Lipschitz0: Lipschitz f Lf
Lipschitz1: Lipschitz g Lg
e: Q+
u, v: (A * B)%type
xi: close e u v
' Lf ≤ ' (Lf ⊔ Lg)
    apply join_ub_l.
-
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
D: Type
H2: Closeness D
f: A -> C
g: B -> D
Rounded0: Rounded C
Rounded1: Rounded D
Lf, Lg: Q+
Lipschitz0: Lipschitz f Lf
Lipschitz1: Lipschitz g Lg
e: Q+
u, v: (A * B)%type
xi: close e u v
close ((Lf ⊔ Lg) * e) (g (snd u)) (g (snd v)) apply rounded_le with (Lg * e).
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
D: Type
H2: Closeness D
f: A -> C
g: B -> D
Rounded0: Rounded C
Rounded1: Rounded D
Lf, Lg: Q+
Lipschitz0: Lipschitz f Lf
Lipschitz1: Lipschitz g Lg
e: Q+
u, v: (A * B)%type
xi: close e u v
close (Lg * e) (g (snd u)) (g (snd v))
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
D: Type
H2: Closeness D
f: A -> C
g: B -> D
Rounded0: Rounded C
Rounded1: Rounded D
Lf, Lg: Q+
Lipschitz0: Lipschitz f Lf
Lipschitz1: Lipschitz g Lg
e: Q+
u, v: (A * B)%type
xi: close e u v
' (Lg * e) ≤ ' ((Lf ⊔ Lg) * e)
  +
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
D: Type
H2: Closeness D
f: A -> C
g: B -> D
Rounded0: Rounded C
Rounded1: Rounded D
Lf, Lg: Q+
Lipschitz0: Lipschitz f Lf
Lipschitz1: Lipschitz g Lg
e: Q+
u, v: (A * B)%type
xi: close e u v
close (Lg * e) (g (snd u)) (g (snd v)) apply (lipschitz _ _),xi.
  +
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
D: Type
H2: Closeness D
f: A -> C
g: B -> D
Rounded0: Rounded C
Rounded1: Rounded D
Lf, Lg: Q+
Lipschitz0: Lipschitz f Lf
Lipschitz1: Lipschitz g Lg
e: Q+
u, v: (A * B)%type
xi: close e u v
' (Lg * e) ≤ ' ((Lf ⊔ Lg) * e) apply (order_preserving (.* ' e)).
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
D: Type
H2: Closeness D
f: A -> C
g: B -> D
Rounded0: Rounded C
Rounded1: Rounded D
Lf, Lg: Q+
Lipschitz0: Lipschitz f Lf
Lipschitz1: Lipschitz g Lg
e: Q+
u, v: (A * B)%type
xi: close e u v
' Lg ≤ ' (Lf ⊔ Lg)
    apply join_ub_r.
Qed.

(* Coq pre 8.8 produces phantom universes, see coq/coq#6483 **)
Definition map2_lipschitz@{i} := ltac:(first [exact @map2_lipschitz'@{i i i}|exact @map2_lipschitz'@{i i i i}]).
Arguments map2_lipschitz {_ _} Lf Lg {_ _} e x y xi.
Global Existing Instance map2_lipschitz.

Lemma map2_continuous' `{!Rounded A} `{!Rounded B}
  `{!Continuous f} `{!Continuous g}
  : Continuous (map2 f g).
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
D: Type
H2: Closeness D
f: A -> C
g: B -> D
Rounded0: Rounded A
Rounded1: Rounded B
Continuous0: Continuous f
Continuous1: Continuous g
Continuous (map2 f g)
Proof.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
D: Type
H2: Closeness D
f: A -> C
g: B -> D
Rounded0: Rounded A
Rounded1: Rounded B
Continuous0: Continuous f
Continuous1: Continuous g
Continuous (map2 f g)
intros u e.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
D: Type
H2: Closeness D
f: A -> C
g: B -> D
Rounded0: Rounded A
Rounded1: Rounded B
Continuous0: Continuous f
Continuous1: Continuous g
u: (A * B)%type
e: Q+
merely
  {d : Q+ &
  forall v : A * B,
  close d u v -> close e (map2 f g u) (map2 f g v)}
apply (merely_destruct (continuous f (fst u) e));intros [d1 E1].
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
D: Type
H2: Closeness D
f: A -> C
g: B -> D
Rounded0: Rounded A
Rounded1: Rounded B
Continuous0: Continuous f
Continuous1: Continuous g
u: (A * B)%type
e, d1: Q+
E1: forall v : A,
close d1 (fst u) v -> close e (f (fst u)) (f v)
merely
  {d : Q+ &
  forall v : A * B,
  close d u v -> close e (map2 f g u) (map2 f g v)}
apply (merely_destruct (continuous g (snd u) e));intros [d2 E2].
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
D: Type
H2: Closeness D
f: A -> C
g: B -> D
Rounded0: Rounded A
Rounded1: Rounded B
Continuous0: Continuous f
Continuous1: Continuous g
u: (A * B)%type
e, d1: Q+
E1: forall v : A,
close d1 (fst u) v -> close e (f (fst u)) (f v)
d2: Q+
E2: forall v : B,
close d2 (snd u) v -> close e (g (snd u)) (g v)
merely
  {d : Q+ &
  forall v : A * B,
  close d u v -> close e (map2 f g u) (map2 f g v)}
apply tr;exists (meet d1 d2).
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
D: Type
H2: Closeness D
f: A -> C
g: B -> D
Rounded0: Rounded A
Rounded1: Rounded B
Continuous0: Continuous f
Continuous1: Continuous g
u: (A * B)%type
e, d1: Q+
E1: forall v : A,
close d1 (fst u) v -> close e (f (fst u)) (f v)
d2: Q+
E2: forall v : B,
close d2 (snd u) v -> close e (g (snd u)) (g v)
forall v : A * B,
close (d1 ⊓ d2) u v ->
close e (map2 f g u) (map2 f g v) intros v xi.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
D: Type
H2: Closeness D
f: A -> C
g: B -> D
Rounded0: Rounded A
Rounded1: Rounded B
Continuous0: Continuous f
Continuous1: Continuous g
u: (A * B)%type
e, d1: Q+
E1: forall v : A,
close d1 (fst u) v -> close e (f (fst u)) (f v)
d2: Q+
E2: forall v : B,
close d2 (snd u) v -> close e (g (snd u)) (g v)
v: (A * B)%type
xi: close (d1 ⊓ d2) u v
close e (map2 f g u) (map2 f g v)
split;simpl.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
D: Type
H2: Closeness D
f: A -> C
g: B -> D
Rounded0: Rounded A
Rounded1: Rounded B
Continuous0: Continuous f
Continuous1: Continuous g
u: (A * B)%type
e, d1: Q+
E1: forall v : A,
close d1 (fst u) v -> close e (f (fst u)) (f v)
d2: Q+
E2: forall v : B,
close d2 (snd u) v -> close e (g (snd u)) (g v)
v: (A * B)%type
xi: close (d1 ⊓ d2) u v
close e (f (fst u)) (f (fst v))
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
D: Type
H2: Closeness D
f: A -> C
g: B -> D
Rounded0: Rounded A
Rounded1: Rounded B
Continuous0: Continuous f
Continuous1: Continuous g
u: (A * B)%type
e, d1: Q+
E1: forall v : A,
close d1 (fst u) v -> close e (f (fst u)) (f v)
d2: Q+
E2: forall v : B,
close d2 (snd u) v -> close e (g (snd u)) (g v)
v: (A * B)%type
xi: close (d1 ⊓ d2) u v
close e (g (snd u)) (g (snd v))
-
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
D: Type
H2: Closeness D
f: A -> C
g: B -> D
Rounded0: Rounded A
Rounded1: Rounded B
Continuous0: Continuous f
Continuous1: Continuous g
u: (A * B)%type
e, d1: Q+
E1: forall v : A,
close d1 (fst u) v -> close e (f (fst u)) (f v)
d2: Q+
E2: forall v : B,
close d2 (snd u) v -> close e (g (snd u)) (g v)
v: (A * B)%type
xi: close (d1 ⊓ d2) u v
close e (f (fst u)) (f (fst v)) apply E1.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
D: Type
H2: Closeness D
f: A -> C
g: B -> D
Rounded0: Rounded A
Rounded1: Rounded B
Continuous0: Continuous f
Continuous1: Continuous g
u: (A * B)%type
e, d1: Q+
E1: forall v : A,
close d1 (fst u) v -> close e (f (fst u)) (f v)
d2: Q+
E2: forall v : B,
close d2 (snd u) v -> close e (g (snd u)) (g v)
v: (A * B)%type
xi: close (d1 ⊓ d2) u v
close d1 (fst u) (fst v) apply rounded_le with (meet d1 d2).
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
D: Type
H2: Closeness D
f: A -> C
g: B -> D
Rounded0: Rounded A
Rounded1: Rounded B
Continuous0: Continuous f
Continuous1: Continuous g
u: (A * B)%type
e, d1: Q+
E1: forall v : A,
close d1 (fst u) v -> close e (f (fst u)) (f v)
d2: Q+
E2: forall v : B,
close d2 (snd u) v -> close e (g (snd u)) (g v)
v: (A * B)%type
xi: close (d1 ⊓ d2) u v
close (d1 ⊓ d2) (fst u) (fst v)
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
D: Type
H2: Closeness D
f: A -> C
g: B -> D
Rounded0: Rounded A
Rounded1: Rounded B
Continuous0: Continuous f
Continuous1: Continuous g
u: (A * B)%type
e, d1: Q+
E1: forall v : A,
close d1 (fst u) v -> close e (f (fst u)) (f v)
d2: Q+
E2: forall v : B,
close d2 (snd u) v -> close e (g (snd u)) (g v)
v: (A * B)%type
xi: close (d1 ⊓ d2) u v
' (d1 ⊓ d2) ≤ ' d1
  +
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
D: Type
H2: Closeness D
f: A -> C
g: B -> D
Rounded0: Rounded A
Rounded1: Rounded B
Continuous0: Continuous f
Continuous1: Continuous g
u: (A * B)%type
e, d1: Q+
E1: forall v : A,
close d1 (fst u) v -> close e (f (fst u)) (f v)
d2: Q+
E2: forall v : B,
close d2 (snd u) v -> close e (g (snd u)) (g v)
v: (A * B)%type
xi: close (d1 ⊓ d2) u v
close (d1 ⊓ d2) (fst u) (fst v) apply xi.
  +
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
D: Type
H2: Closeness D
f: A -> C
g: B -> D
Rounded0: Rounded A
Rounded1: Rounded B
Continuous0: Continuous f
Continuous1: Continuous g
u: (A * B)%type
e, d1: Q+
E1: forall v : A,
close d1 (fst u) v -> close e (f (fst u)) (f v)
d2: Q+
E2: forall v : B,
close d2 (snd u) v -> close e (g (snd u)) (g v)
v: (A * B)%type
xi: close (d1 ⊓ d2) u v
' (d1 ⊓ d2) ≤ ' d1 apply meet_lb_l.
-
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
D: Type
H2: Closeness D
f: A -> C
g: B -> D
Rounded0: Rounded A
Rounded1: Rounded B
Continuous0: Continuous f
Continuous1: Continuous g
u: (A * B)%type
e, d1: Q+
E1: forall v : A,
close d1 (fst u) v -> close e (f (fst u)) (f v)
d2: Q+
E2: forall v : B,
close d2 (snd u) v -> close e (g (snd u)) (g v)
v: (A * B)%type
xi: close (d1 ⊓ d2) u v
close e (g (snd u)) (g (snd v)) apply E2.
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
D: Type
H2: Closeness D
f: A -> C
g: B -> D
Rounded0: Rounded A
Rounded1: Rounded B
Continuous0: Continuous f
Continuous1: Continuous g
u: (A * B)%type
e, d1: Q+
E1: forall v : A,
close d1 (fst u) v -> close e (f (fst u)) (f v)
d2: Q+
E2: forall v : B,
close d2 (snd u) v -> close e (g (snd u)) (g v)
v: (A * B)%type
xi: close (d1 ⊓ d2) u v
close d2 (snd u) (snd v) apply rounded_le with (meet d1 d2).
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
D: Type
H2: Closeness D
f: A -> C
g: B -> D
Rounded0: Rounded A
Rounded1: Rounded B
Continuous0: Continuous f
Continuous1: Continuous g
u: (A * B)%type
e, d1: Q+
E1: forall v : A,
close d1 (fst u) v -> close e (f (fst u)) (f v)
d2: Q+
E2: forall v : B,
close d2 (snd u) v -> close e (g (snd u)) (g v)
v: (A * B)%type
xi: close (d1 ⊓ d2) u v
close (d1 ⊓ d2) (snd u) (snd v)
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
D: Type
H2: Closeness D
f: A -> C
g: B -> D
Rounded0: Rounded A
Rounded1: Rounded B
Continuous0: Continuous f
Continuous1: Continuous g
u: (A * B)%type
e, d1: Q+
E1: forall v : A,
close d1 (fst u) v -> close e (f (fst u)) (f v)
d2: Q+
E2: forall v : B,
close d2 (snd u) v -> close e (g (snd u)) (g v)
v: (A * B)%type
xi: close (d1 ⊓ d2) u v
' (d1 ⊓ d2) ≤ ' d2
  +
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
D: Type
H2: Closeness D
f: A -> C
g: B -> D
Rounded0: Rounded A
Rounded1: Rounded B
Continuous0: Continuous f
Continuous1: Continuous g
u: (A * B)%type
e, d1: Q+
E1: forall v : A,
close d1 (fst u) v -> close e (f (fst u)) (f v)
d2: Q+
E2: forall v : B,
close d2 (snd u) v -> close e (g (snd u)) (g v)
v: (A * B)%type
xi: close (d1 ⊓ d2) u v
close (d1 ⊓ d2) (snd u) (snd v) apply xi.
  +
funext: Funext
univalence: Univalence
A: Type
H: Closeness A
B: Type
H0: Closeness B
C: Type
H1: Closeness C
D: Type
H2: Closeness D
f: A -> C
g: B -> D
Rounded0: Rounded A
Rounded1: Rounded B
Continuous0: Continuous f
Continuous1: Continuous g
u: (A * B)%type
e, d1: Q+
E1: forall v : A,
close d1 (fst u) v -> close e (f (fst u)) (f v)
d2: Q+
E2: forall v : B,
close d2 (snd u) v -> close e (g (snd u)) (g v)
v: (A * B)%type
xi: close (d1 ⊓ d2) u v
' (d1 ⊓ d2) ≤ ' d2 apply meet_lb_r.
Qed.

(* Coq pre 8.8 produces phantom universes, see coq/coq#6483 **)
Definition map2_continuous@{i} := ltac:(first [exact @map2_continuous'@{i i i}|exact @map2_continuous'@{i i i i}]).
Arguments map2_continuous {_ _ _ _} u e.
Global Existing Instance map2_continuous.

End map2.

Section interval.
Universe UA UALE.
Context {A:Type@{UA} } {Ale : Le@{UA UALE} A}.

Definition Interval a b := sig (fun x : A => a <= x /\ x <= b).

Definition interval_proj a b : Interval a b -> A := pr1.

Context {Ameet : Meet A} {Ajoin : Join A}
  `{!LatticeOrder@{UA UALE} Ale}.

Definition Interval_restrict@{} (a b : A) (E : a <= b) : A -> Interval a b.
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
a, b: A
E: a ≤ b
A -> Interval a b
Proof.
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
a, b: A
E: a ≤ b
A -> Interval a b
intros x.
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
a, b: A
E: a ≤ b
x: A
Interval a b
exists (join a (meet x b)).
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
a, b: A
E: a ≤ b
x: A
a ≤ a ⊔ (x ⊓ b) ≤ b
split.
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
a, b: A
E: a ≤ b
x: A
a ≤ a ⊔ (x ⊓ b)
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
a, b: A
E: a ≤ b
x: A
a ⊔ (x ⊓ b) ≤ b
-
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
a, b: A
E: a ≤ b
x: A
a ≤ a ⊔ (x ⊓ b) apply join_ub_l.
-
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
a, b: A
E: a ≤ b
x: A
a ⊔ (x ⊓ b) ≤ b apply join_le.
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
a, b: A
E: a ≤ b
x: A
a ≤ b
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
a, b: A
E: a ≤ b
x: A
x ⊓ b ≤ b
  +
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
a, b: A
E: a ≤ b
x: A
a ≤ b exact E.
  +
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
a, b: A
E: a ≤ b
x: A
x ⊓ b ≤ b apply meet_lb_r.
Defined.

Lemma Interval_restrict_pr : forall a b E x (E': a <= x /\ x <= b),
  Interval_restrict a b E x = exist _ x E'.
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
forall (a b : A) (E : a ≤ b) (x : A) (E' : a ≤ x ≤ b),
Interval_restrict a b E x = (x; E')
Proof.
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
forall (a b : A) (E : a ≤ b) (x : A) (E' : a ≤ x ≤ b),
Interval_restrict a b E x = (x; E')
intros a b E x E'.
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
a, b: A
E: a ≤ b
x: A
E': a ≤ x ≤ b
Interval_restrict a b E x = (x; E')
unfold Interval_restrict.
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
a, b: A
E: a ≤ b
x: A
E': a ≤ x ≤ b
(a ⊔ (x ⊓ b);
(join_ub_l a (x ⊓ b),
join_le a (x ⊓ b) b E (meet_lb_r x b))) = (x; E')
apply Sigma.path_sigma_hprop.
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
a, b: A
E: a ≤ b
x: A
E': a ≤ x ≤ b
(a ⊔ (x ⊓ b);
(join_ub_l a (x ⊓ b),
join_le a (x ⊓ b) b E (meet_lb_r x b))).1 = (x; E').1
simpl.
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
a, b: A
E: a ≤ b
x: A
E': a ≤ x ≤ b
a ⊔ (x ⊓ b) = x rewrite meet_l;[apply join_r|];apply E'.
Qed.

Context `{Closeness A}.

Global Instance Interval_close (a b : A) : Closeness (Interval a b)
  := fun e x y => close e (interval_proj a b x) (interval_proj a b y).
Arguments Interval_close _ _ _ _ _ /.

(* NB: for some reason this forces UALE <= UA *)
Lemma Interval_premetric@{i} `{!PreMetric@{UA i} A} a b
  : PreMetric@{UA i} (Interval a b).
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
H: Closeness A
PreMetric0: PreMetric A
a, b: A
PreMetric (Interval a b)
Proof.
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
H: Closeness A
PreMetric0: PreMetric A
a, b: A
PreMetric (Interval a b)
split.
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
H: Closeness A
PreMetric0: PreMetric A
a, b: A
forall (e : Q+) (x y : Interval a b),
IsHProp (close e x y)
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
H: Closeness A
PreMetric0: PreMetric A
a, b: A
forall e : Q+, Reflexive (close e)
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
H: Closeness A
PreMetric0: PreMetric A
a, b: A
forall e : Q+, Symmetric (close e)
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
H: Closeness A
PreMetric0: PreMetric A
a, b: A
Separated (Interval a b)
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
H: Closeness A
PreMetric0: PreMetric A
a, b: A
Triangular (Interval a b)
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
H: Closeness A
PreMetric0: PreMetric A
a, b: A
Rounded (Interval a b)
-
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
H: Closeness A
PreMetric0: PreMetric A
a, b: A
forall (e : Q+) (x y : Interval a b),
IsHProp (close e x y) unfold close;simpl.
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
H: Closeness A
PreMetric0: PreMetric A
a, b: A
forall (e : Q+) (x y : Interval a b),
IsHProp
  (close e (interval_proj a b x) (interval_proj a b y)) apply _.
-
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
H: Closeness A
PreMetric0: PreMetric A
a, b: A
forall e : Q+, Reflexive (close e) intros e u.
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
H: Closeness A
PreMetric0: PreMetric A
a, b: A
e: Q+
u: Interval a b
close e u u red;red.
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
H: Closeness A
PreMetric0: PreMetric A
a, b: A
e: Q+
u: Interval a b
close e (interval_proj a b u) (interval_proj a b u) reflexivity.
-
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
H: Closeness A
PreMetric0: PreMetric A
a, b: A
forall e : Q+, Symmetric (close e) intros e u v xi;red;red;symmetry;apply xi.
-
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
H: Closeness A
PreMetric0: PreMetric A
a, b: A
Separated (Interval a b) intros u v E.
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
H: Closeness A
PreMetric0: PreMetric A
a, b: A
u, v: Interval a b
E: forall e : Q+, close e u v
u = v
  apply Sigma.path_sigma_hprop.
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
H: Closeness A
PreMetric0: PreMetric A
a, b: A
u, v: Interval a b
E: forall e : Q+, close e u v
u.1 = v.1 apply separated,E.
-
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
H: Closeness A
PreMetric0: PreMetric A
a, b: A
Triangular (Interval a b) intros u v w e d xi1 xi2.
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
H: Closeness A
PreMetric0: PreMetric A
a, b: A
u, v, w: Interval a b
e, d: Q+
xi1: close e u v
xi2: close d v w
close (e + d) u w
  red;red.
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
H: Closeness A
PreMetric0: PreMetric A
a, b: A
u, v, w: Interval a b
e, d: Q+
xi1: close e u v
xi2: close d v w
close (e + d) (interval_proj a b u)
  (interval_proj a b w) apply (triangular _ (interval_proj a b v)).
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
H: Closeness A
PreMetric0: PreMetric A
a, b: A
u, v, w: Interval a b
e, d: Q+
xi1: close e u v
xi2: close d v w
close e (interval_proj a b u) (interval_proj a b v)
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
H: Closeness A
PreMetric0: PreMetric A
a, b: A
u, v, w: Interval a b
e, d: Q+
xi1: close e u v
xi2: close d v w
close d (interval_proj a b v) (interval_proj a b w)
  +
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
H: Closeness A
PreMetric0: PreMetric A
a, b: A
u, v, w: Interval a b
e, d: Q+
xi1: close e u v
xi2: close d v w
close e (interval_proj a b u) (interval_proj a b v) exact xi1.
  +
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
H: Closeness A
PreMetric0: PreMetric A
a, b: A
u, v, w: Interval a b
e, d: Q+
xi1: close e u v
xi2: close d v w
close d (interval_proj a b v) (interval_proj a b w) exact xi2.
-
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
H: Closeness A
PreMetric0: PreMetric A
a, b: A
Rounded (Interval a b) intros e u v.
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
H: Closeness A
PreMetric0: PreMetric A
a, b: A
e: Q+
u, v: Interval a b
close e u v <->
merely
  {d : Q+ &
  {d' : Q+ & ((e = (d + d')%mc) * close d u v)%type}} split.
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
H: Closeness A
PreMetric0: PreMetric A
a, b: A
e: Q+
u, v: Interval a b
close e u v ->
merely
  {d : Q+ &
  {d' : Q+ & ((e = (d + d')%mc) * close d u v)%type}}
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
H: Closeness A
PreMetric0: PreMetric A
a, b: A
e: Q+
u, v: Interval a b
merely
  {d : Q+ &
  {d' : Q+ & ((e = (d + d')%mc) * close d u v)%type}} ->
close e u v
  +
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
H: Closeness A
PreMetric0: PreMetric A
a, b: A
e: Q+
u, v: Interval a b
close e u v ->
merely
  {d : Q+ &
  {d' : Q+ & ((e = (d + d')%mc) * close d u v)%type}} intros xi.
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
H: Closeness A
PreMetric0: PreMetric A
a, b: A
e: Q+
u, v: Interval a b
xi: close e u v
merely
  {d : Q+ &
  {d' : Q+ & ((e = (d + d')%mc) * close d u v)%type}} do 2 red in xi.
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
H: Closeness A
PreMetric0: PreMetric A
a, b: A
e: Q+
u, v: Interval a b
xi: close e (interval_proj a b u)
  (interval_proj a b v)
merely
  {d : Q+ &
  {d' : Q+ & ((e = (d + d')%mc) * close d u v)%type}} apply (fst (rounded _ _ _)) in xi.
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
H: Closeness A
PreMetric0: PreMetric A
a, b: A
e: Q+
u, v: Interval a b
xi: merely
  {d : Q+ &
  {d' : Q+ &
  ((e = (d + d')%mc) *
   close d (interval_proj a b u)
     (interval_proj a b v))%type}}
merely
  {d : Q+ &
  {d' : Q+ & ((e = (d + d')%mc) * close d u v)%type}}
    exact xi.
  +
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
H: Closeness A
PreMetric0: PreMetric A
a, b: A
e: Q+
u, v: Interval a b
merely
  {d : Q+ &
  {d' : Q+ & ((e = (d + d')%mc) * close d u v)%type}} ->
close e u v intros E.
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
H: Closeness A
PreMetric0: PreMetric A
a, b: A
e: Q+
u, v: Interval a b
E: merely
  {d : Q+ &
  {d' : Q+ &
  ((e = (d + d')%mc) * close d u v)%type}}
close e u v unfold close,Interval_close in E.
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
H: Closeness A
PreMetric0: PreMetric A
a, b: A
e: Q+
u, v: Interval a b
E: merely
  {d : Q+ &
  {d' : Q+ &
  ((e = (d + d')%mc) *
   close d (interval_proj a b u)
     (interval_proj a b v))%type}}
close e u v apply (snd (rounded _ _ _)) in E.
funext: Funext
univalence: Univalence
A: Type
Ale: Le A
Ameet: Meet A
Ajoin: Join A
LatticeOrder0: LatticeOrder Ale
H: Closeness A
PreMetric0: PreMetric A
a, b: A
e: Q+
u, v: Interval a b
E: close e (interval_proj a b u)
  (interval_proj a b v)
close e u v
    exact E.
Qed.
Global Existing Instance Interval_premetric.

Global Instance interval_proj_nonexpanding (a b : A)
  : NonExpanding (interval_proj a b)
  := fun _ _ _ xi => xi.

End interval.

Section rationals.

Lemma Qclose_alt : forall e (q r : Q), close e q r <-> abs (q - r) < ' e.
funext: Funext
univalence: Univalence
forall (e : Q+) (q r : Q),
close e q r <-> abs (q - r) < ' e
Proof.
funext: Funext
univalence: Univalence
forall (e : Q+) (q r : Q),
close e q r <-> abs (q - r) < ' e
intros e q r;split.
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
close e q r -> abs (q - r) < ' e
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
abs (q - r) < ' e -> close e q r
-
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
close e q r -> abs (q - r) < ' e intros [E1 E2].
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
E1: - ' e < q - r
E2: q - r < ' e
abs (q - r) < ' e
  destruct (total le 0 (q - r)) as [E|E].
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
E1: - ' e < q - r
E2: q - r < ' e
E: 0 ≤ q - r
abs (q - r) < ' e
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
E1: - ' e < q - r
E2: q - r < ' e
E: q - r ≤ 0
abs (q - r) < ' e
  +
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
E1: - ' e < q - r
E2: q - r < ' e
E: 0 ≤ q - r
abs (q - r) < ' e rewrite (Qabs_of_nonneg _ E).
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
E1: - ' e < q - r
E2: q - r < ' e
E: 0 ≤ q - r
q - r < ' e
    trivial.
  +
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
E1: - ' e < q - r
E2: q - r < ' e
E: q - r ≤ 0
abs (q - r) < ' e rewrite (Qabs_of_nonpos _ E).
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
E1: - ' e < q - r
E2: q - r < ' e
E: q - r ≤ 0
- (q - r) < ' e
    apply flip_lt_negate.
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
E1: - ' e < q - r
E2: q - r < ' e
E: q - r ≤ 0
- ' e < - - (q - r) rewrite involutive.
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
E1: - ' e < q - r
E2: q - r < ' e
E: q - r ≤ 0
- ' e < q - r trivial.
-
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
abs (q - r) < ' e -> close e q r intros E.
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
E: abs (q - r) < ' e
close e q r split;[apply flip_lt_negate;rewrite involutive|];
  apply le_lt_trans with (abs (q - r));trivial.
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
E: abs (q - r) < ' e
- (q - r) ≤ abs (q - r)
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
E: abs (q - r) < ' e
q - r ≤ abs (q - r)
  +
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
E: abs (q - r) < ' e
- (q - r) ≤ abs (q - r) apply Qabs_le_neg_raw.
  +
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
E: abs (q - r) < ' e
q - r ≤ abs (q - r) apply Qabs_le_raw.
Qed.

Lemma Qclose_neg@{} : forall e (x y : Q), close e x y <-> close e (- x) (- y).
funext: Funext
univalence: Univalence
forall (e : Q+) (x y : Q),
close e x y <-> close e (- x) (- y)
Proof.
funext: Funext
univalence: Univalence
forall (e : Q+) (x y : Q),
close e x y <-> close e (- x) (- y)
intros e x y;split;intros E;apply Qclose_alt in E;apply Qclose_alt.
funext: Funext
univalence: Univalence
e: Q+
x, y: Q
E: abs (x - y) < ' e
abs (- x - - y) < ' e
funext: Funext
univalence: Univalence
e: Q+
x, y: Q
E: abs (- x - - y) < ' e
abs (x - y) < ' e
-
funext: Funext
univalence: Univalence
e: Q+
x, y: Q
E: abs (x - y) < ' e
abs (- x - - y) < ' e rewrite <-(negate_plus_distr),Qabs_neg.
funext: Funext
univalence: Univalence
e: Q+
x, y: Q
E: abs (x - y) < ' e
abs (x - y) < ' e trivial.
-
funext: Funext
univalence: Univalence
e: Q+
x, y: Q
E: abs (- x - - y) < ' e
abs (x - y) < ' e rewrite <-(negate_plus_distr),Qabs_neg in E.
funext: Funext
univalence: Univalence
e: Q+
x, y: Q
E: abs (x - y) < ' e
abs (x - y) < ' e trivial.
Qed.

Instance Q_close_symm@{} : forall e, Symmetric (@close Q _ e).
funext: Funext
univalence: Univalence
forall e : Q+, Symmetric (close e)
Proof.
funext: Funext
univalence: Univalence
forall e : Q+, Symmetric (close e)
red;unfold close;simpl.
funext: Funext
univalence: Univalence
forall (e : Q+) (x y : Q),
Q_close e x y -> Q_close e y x
intros e x y [E1 E2];split.
funext: Funext
univalence: Univalence
e: Q+
x, y: Q
E1: - ' e < x - y
E2: x - y < ' e
- ' e < y - x
funext: Funext
univalence: Univalence
e: Q+
x, y: Q
E1: - ' e < x - y
E2: x - y < ' e
y - x < ' e
-
funext: Funext
univalence: Univalence
e: Q+
x, y: Q
E1: - ' e < x - y
E2: x - y < ' e
- ' e < y - x apply flip_lt_negate.
funext: Funext
univalence: Univalence
e: Q+
x, y: Q
E1: - ' e < x - y
E2: x - y < ' e
- (y - x) < - - ' e rewrite <-negate_swap_r,involutive.
funext: Funext
univalence: Univalence
e: Q+
x, y: Q
E1: - ' e < x - y
E2: x - y < ' e
x - y < ' e
  trivial.
-
funext: Funext
univalence: Univalence
e: Q+
x, y: Q
E1: - ' e < x - y
E2: x - y < ' e
y - x < ' e apply flip_lt_negate.
funext: Funext
univalence: Univalence
e: Q+
x, y: Q
E1: - ' e < x - y
E2: x - y < ' e
- ' e < - (y - x)
  rewrite negate_swap_r,involutive.
funext: Funext
univalence: Univalence
e: Q+
x, y: Q
E1: - ' e < x - y
E2: x - y < ' e
- ' e < x - y trivial.
Qed.

Lemma Q_triangular_one@{} : forall (q r : Q)
(e : Q+) (Hqr : close e q r)
(q0 : Q) (n : Q+),
  (close n q q0 -> close (e + n) r q0).
funext: Funext
univalence: Univalence
forall (q r : Q) (e : Q+),
close e q r ->
forall (q0 : Q) (n : Q+),
close n q q0 -> close (e + n) r q0
Proof.
funext: Funext
univalence: Univalence
forall (q r : Q) (e : Q+),
close e q r ->
forall (q0 : Q) (n : Q+),
close n q q0 -> close (e + n) r q0
unfold close;simpl.
funext: Funext
univalence: Univalence
forall (q r : Q) (e : Q+),
Q_close e q r ->
forall (q0 : Q) (n : Q+),
Q_close n q q0 -> Q_close (e + n) r q0
intros q r e [E1 E1'] s n [E2 E2'].
funext: Funext
univalence: Univalence
q, r: Q
e: Q+
E1: - ' e < q - r
E1': q - r < ' e
s: Q
n: Q+
E2: - ' n < q - s
E2': q - s < ' n
Q_close (e + n) r s
split.
funext: Funext
univalence: Univalence
q, r: Q
e: Q+
E1: - ' e < q - r
E1': q - r < ' e
s: Q
n: Q+
E2: - ' n < q - s
E2': q - s < ' n
- ' (e + n) < r - s
funext: Funext
univalence: Univalence
q, r: Q
e: Q+
E1: - ' e < q - r
E1': q - r < ' e
s: Q
n: Q+
E2: - ' n < q - s
E2': q - s < ' n
r - s < ' (e + n)
-
funext: Funext
univalence: Univalence
q, r: Q
e: Q+
E1: - ' e < q - r
E1': q - r < ' e
s: Q
n: Q+
E2: - ' n < q - s
E2': q - s < ' n
- ' (e + n) < r - s apply flip_lt_negate.
funext: Funext
univalence: Univalence
q, r: Q
e: Q+
E1: - ' e < q - r
E1': q - r < ' e
s: Q
n: Q+
E2: - ' n < q - s
E2': q - s < ' n
- (r - s) < - - ' (e + n) rewrite negate_swap_r,!involutive.
funext: Funext
univalence: Univalence
q, r: Q
e: Q+
E1: - ' e < q - r
E1': q - r < ' e
s: Q
n: Q+
E2: - ' n < q - s
E2': q - s < ' n
s - r < ' (e + n)
  apply flip_lt_negate in E2.
funext: Funext
univalence: Univalence
q, r: Q
e: Q+
E1: - ' e < q - r
E1': q - r < ' e
s: Q
n: Q+
E2: - (q - s) < - - ' n
E2': q - s < ' n
s - r < ' (e + n)
  rewrite negate_swap_r,!involutive in E2.
funext: Funext
univalence: Univalence
q, r: Q
e: Q+
E1: - ' e < q - r
E1': q - r < ' e
s: Q
n: Q+
E2: s - q < ' n
E2': q - s < ' n
s - r < ' (e + n)
  pose proof (plus_lt_compat _ _ _ _ E1' E2) as E.
funext: Funext
univalence: Univalence
q, r: Q
e: Q+
E1: - ' e < q - r
E1': q - r < ' e
s: Q
n: Q+
E2: s - q < ' n
E2': q - s < ' n
E: q - r + (s - q) < ' e + ' n
s - r < ' (e + n)
  assert (Hrw : s - r = q - r + (s - q))
    by abstract ring_tac.ring_with_integers (NatPair.Z nat).
funext: Funext
univalence: Univalence
q, r: Q
e: Q+
E1: - ' e < q - r
E1': q - r < ' e
s: Q
n: Q+
E2: s - q < ' n
E2': q - s < ' n
E: q - r + (s - q) < ' e + ' n
Hrw: s - r = q - r + (s - q)
s - r < ' (e + n)
  rewrite Hrw;trivial.
-
funext: Funext
univalence: Univalence
q, r: Q
e: Q+
E1: - ' e < q - r
E1': q - r < ' e
s: Q
n: Q+
E2: - ' n < q - s
E2': q - s < ' n
r - s < ' (e + n) apply flip_lt_negate in E1.
funext: Funext
univalence: Univalence
q, r: Q
e: Q+
E1: - (q - r) < - - ' e
E1': q - r < ' e
s: Q
n: Q+
E2: - ' n < q - s
E2': q - s < ' n
r - s < ' (e + n)
  rewrite negate_swap_r,!involutive in E1.
funext: Funext
univalence: Univalence
q, r: Q
e: Q+
E1: r - q < ' e
E1': q - r < ' e
s: Q
n: Q+
E2: - ' n < q - s
E2': q - s < ' n
r - s < ' (e + n)
  pose proof (plus_lt_compat _ _ _ _ E1 E2') as E.
funext: Funext
univalence: Univalence
q, r: Q
e: Q+
E1: r - q < ' e
E1': q - r < ' e
s: Q
n: Q+
E2: - ' n < q - s
E2': q - s < ' n
E: r - q + (q - s) < ' e + ' n
r - s < ' (e + n)
  assert (Hrw : r - s = r - q + (q - s))
    by abstract ring_tac.ring_with_integers (NatPair.Z nat).
funext: Funext
univalence: Univalence
q, r: Q
e: Q+
E1: r - q < ' e
E1': q - r < ' e
s: Q
n: Q+
E2: - ' n < q - s
E2': q - s < ' n
E: r - q + (q - s) < ' e + ' n
Hrw: r - s = r - q + (q - s)
r - s < ' (e + n)
  rewrite Hrw;trivial.
Qed.

Instance Q_triangular@{} : Triangular Q.
funext: Funext
univalence: Univalence
Triangular Q
Proof.
funext: Funext
univalence: Univalence
Triangular Q
hnf.
funext: Funext
univalence: Univalence
forall (u v w : Q) (e d : Q+),
close e u v -> close d v w -> close (e + d) u w intros u v w e d E1 E2.
funext: Funext
univalence: Univalence
u, v, w: Q
e, d: Q+
E1: close e u v
E2: close d v w
close (e + d) u w
apply Q_triangular_one with v.
funext: Funext
univalence: Univalence
u, v, w: Q
e, d: Q+
E1: close e u v
E2: close d v w
close e v u
funext: Funext
univalence: Univalence
u, v, w: Q
e, d: Q+
E1: close e u v
E2: close d v w
close d v w
-
funext: Funext
univalence: Univalence
u, v, w: Q
e, d: Q+
E1: close e u v
E2: close d v w
close e v u symmetry;trivial.
-
funext: Funext
univalence: Univalence
u, v, w: Q
e, d: Q+
E1: close e u v
E2: close d v w
close d v w trivial.
Qed.

Lemma Qclose_separating_not_lt : forall q r : Q, (forall e, close e q r) ->
  ~ (q < r).
funext: Funext
univalence: Univalence
forall q r : Q,
(forall e : Q+, close e q r) -> ~ (q < r)
Proof.
funext: Funext
univalence: Univalence
forall q r : Q,
(forall e : Q+, close e q r) -> ~ (q < r)
intros q r E1 E2.
funext: Funext
univalence: Univalence
q, r: Q
E1: forall e : Q+, close e q r
E2: q < r
Empty
pose proof (E1 (Qpos_diff _ _ E2)) as E3.
funext: Funext
univalence: Univalence
q, r: Q
E1: forall e : Q+, close e q r
E2: q < r
E3: close (Qpos_diff q r E2) q r
Empty
apply symmetry in E3;apply Qclose_alt in E3.
funext: Funext
univalence: Univalence
q, r: Q
E1: forall e : Q+, close e q r
E2: q < r
E3: abs (r - q) < ' Qpos_diff q r E2
Empty
unfold cast in E3;simpl in E3.
funext: Funext
univalence: Univalence
q, r: Q
E1: forall e : Q+, close e q r
E2: q < r
E3: abs (r - q) < r - q
Empty
apply (irreflexivity lt (r - q)).
funext: Funext
univalence: Univalence
q, r: Q
E1: forall e : Q+, close e q r
E2: q < r
E3: abs (r - q) < r - q
r - q < r - q
apply le_lt_trans with (abs (r - q));trivial.
funext: Funext
univalence: Univalence
q, r: Q
E1: forall e : Q+, close e q r
E2: q < r
E3: abs (r - q) < r - q
r - q ≤ abs (r - q)
apply Qabs_le_raw.
Qed.

Instance Qclose_separating : Separated Q.
funext: Funext
univalence: Univalence
Separated Q
Proof.
funext: Funext
univalence: Univalence
Separated Q
hnf.
funext: Funext
univalence: Univalence
forall x y : Q, (forall e : Q+, close e x y) -> x = y intros q r E1.
funext: Funext
univalence: Univalence
q, r: Q
E1: forall e : Q+, close e q r
q = r
apply tight_apart.
funext: Funext
univalence: Univalence
q, r: Q
E1: forall e : Q+, close e q r
~ (q ≶ r) intros E2.
funext: Funext
univalence: Univalence
q, r: Q
E1: forall e : Q+, close e q r
E2: q ≶ r
Empty
apply apart_iff_total_lt in E2.
funext: Funext
univalence: Univalence
q, r: Q
E1: forall e : Q+, close e q r
E2: ((q < r) + (r < q))%type
Empty destruct E2 as [E2|E2].
funext: Funext
univalence: Univalence
q, r: Q
E1: forall e : Q+, close e q r
E2: q < r
Empty
funext: Funext
univalence: Univalence
q, r: Q
E1: forall e : Q+, close e q r
E2: r < q
Empty
-
funext: Funext
univalence: Univalence
q, r: Q
E1: forall e : Q+, close e q r
E2: q < r
Empty exact (Qclose_separating_not_lt _ _ E1 E2).
-
funext: Funext
univalence: Univalence
q, r: Q
E1: forall e : Q+, close e q r
E2: r < q
Empty refine (Qclose_separating_not_lt _ _ _ E2).
funext: Funext
univalence: Univalence
q, r: Q
E1: forall e : Q+, close e q r
E2: r < q
forall e : Q+, close e r q
  intros;symmetry;trivial.
Qed.

Instance Qclose_rounded@{} : Rounded Q.
funext: Funext
univalence: Univalence
Rounded Q
Proof.
funext: Funext
univalence: Univalence
Rounded Q
intros e q r;split.
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
close e q r ->
merely
  {d : Q+ &
  {d' : Q+ & ((e = (d + d')%mc) * close d q r)%type}}
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
merely
  {d : Q+ &
  {d' : Q+ & ((e = (d + d')%mc) * close d q r)%type}} ->
close e q r
-
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
close e q r ->
merely
  {d : Q+ &
  {d' : Q+ & ((e = (d + d')%mc) * close d q r)%type}} intros E;apply Qclose_alt in E.
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
E: abs (q - r) < ' e
merely
  {d : Q+ &
  {d' : Q+ & ((e = (d + d')%mc) * close d q r)%type}}
  pose proof (Q_average_between _ _ E) as [E1 E2].
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
E: abs (q - r) < ' e
E1: abs (q - r) < (abs (q - r) + ' e) / 2
E2: (abs (q - r) + ' e) / 2 < ' e
merely
  {d : Q+ &
  {d' : Q+ & ((e = (d + d')%mc) * close d q r)%type}}
  apply tr;simple refine (exist _ (mkQpos ((abs (q - r) + ' e) / 2) _) _).
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
E: abs (q - r) < ' e
E1: abs (q - r) < (abs (q - r) + ' e) / 2
E2: (abs (q - r) + ' e) / 2 < ' e
0 < (abs (q - r) + ' e) / 2
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
E: abs (q - r) < ' e
E1: abs (q - r) < (abs (q - r) + ' e) / 2
E2: (abs (q - r) + ' e) / 2 < ' e
(fun d : Q+ =>
 {d' : Q+ & ((e = (d + d')%mc) * close d q r)%type})
  {|
    pos := (abs (q - r) + ' e) / 2; is_pos := ?is_pos
  |}
  {
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
E: abs (q - r) < ' e
E1: abs (q - r) < (abs (q - r) + ' e) / 2
E2: (abs (q - r) + ' e) / 2 < ' e
0 < (abs (q - r) + ' e) / 2 apply pos_mult_compat;[|solve_propholds].
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
E: abs (q - r) < ' e
E1: abs (q - r) < (abs (q - r) + ' e) / 2
E2: (abs (q - r) + ' e) / 2 < ' e
PropHolds (0 < abs (q - r) + ' e)
    red.
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
E: abs (q - r) < ' e
E1: abs (q - r) < (abs (q - r) + ' e) / 2
E2: (abs (q - r) + ' e) / 2 < ' e
0 < abs (q - r) + ' e apply pos_plus_le_lt_compat_r;[solve_propholds|apply Qabs_nonneg].
  }
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
E: abs (q - r) < ' e
E1: abs (q - r) < (abs (q - r) + ' e) / 2
E2: (abs (q - r) + ' e) / 2 < ' e
(fun d : Q+ =>
 {d' : Q+ & ((e = (d + d')%mc) * close d q r)%type})
  {|
    pos := (abs (q - r) + ' e) / 2;
    is_pos :=
      pos_mult_compat (abs (q - r) + ' e) (/ 2)
        (pos_plus_le_lt_compat_r 0 (abs (q - r)) (' e)
           (pos_is_pos e) (Qabs_nonneg (q - r))
         :
         PropHolds (0 < abs (q - r) + ' e))
        (pos_dec_recip_compat 2 lt_0_2)
  |}
  simpl.
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
E: abs (q - r) < ' e
E1: abs (q - r) < (abs (q - r) + ' e) / 2
E2: (abs (q - r) + ' e) / 2 < ' e
{d' : Q+ &
((e =
  ({|
     pos := (abs (q - r) + ' e) / 2;
     is_pos :=
       pos_mult_compat (abs (q - r) + ' e) (/ 2)
         (pos_plus_le_lt_compat_r 0 (abs (q - r))
            (' e) (pos_is_pos e) (Qabs_nonneg (q - r)))
         (pos_dec_recip_compat 2 lt_0_2)
   |} + d')%mc) *
 close
   {|
     pos := (abs (q - r) + ' e)%mc / 2;
     is_pos :=
       pos_mult_compat (abs (q - r) + ' e)%mc (/ 2)
         (pos_plus_le_lt_compat_r 0 (abs (q - r))
            (' e) (pos_is_pos e) (Qabs_nonneg (q - r)))
         (pos_dec_recip_compat 2 lt_0_2)
   |} q r)%type} exists (Qpos_diff _ _ E2).
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
E: abs (q - r) < ' e
E1: abs (q - r) < (abs (q - r) + ' e) / 2
E2: (abs (q - r) + ' e) / 2 < ' e
((e =
  ({|
     pos := (abs (q - r) + ' e) / 2;
     is_pos :=
       pos_mult_compat (abs (q - r) + ' e) (/ 2)
         (pos_plus_le_lt_compat_r 0 (abs (q - r))
            (' e) (pos_is_pos e) (Qabs_nonneg (q - r)))
         (pos_dec_recip_compat 2 lt_0_2)
   |} + Qpos_diff ((abs (q - r) + ' e) / 2) (' e) E2)%mc) *
 close
   {|
     pos := (abs (q - r) + ' e)%mc / 2;
     is_pos :=
       pos_mult_compat (abs (q - r) + ' e)%mc (/ 2)
         (pos_plus_le_lt_compat_r 0 (abs (q - r))
            (' e) (pos_is_pos e) (Qabs_nonneg (q - r)))
         (pos_dec_recip_compat 2 lt_0_2)
   |} q r)%type
  split.
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
E: abs (q - r) < ' e
E1: abs (q - r) < (abs (q - r) + ' e) / 2
E2: (abs (q - r) + ' e) / 2 < ' e
e =
{|
  pos := (abs (q - r) + ' e) / 2;
  is_pos :=
    pos_mult_compat (abs (q - r) + ' e) (/ 2)
      (pos_plus_le_lt_compat_r 0 (abs (q - r)) (' e)
         (pos_is_pos e) (Qabs_nonneg (q - r)))
      (pos_dec_recip_compat 2 lt_0_2)
|} + Qpos_diff ((abs (q - r) + ' e) / 2) (' e) E2
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
E: abs (q - r) < ' e
E1: abs (q - r) < (abs (q - r) + ' e) / 2
E2: (abs (q - r) + ' e) / 2 < ' e
close
  {|
    pos := (abs (q - r) + ' e) / 2;
    is_pos :=
      pos_mult_compat (abs (q - r) + ' e) 
        (/ 2)
        (pos_plus_le_lt_compat_r 0 
           (abs (q - r)) 
           (' e) (pos_is_pos e) 
           (Qabs_nonneg (q - r)))
        (pos_dec_recip_compat 2 lt_0_2)
  |} q r
  +
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
E: abs (q - r) < ' e
E1: abs (q - r) < (abs (q - r) + ' e) / 2
E2: (abs (q - r) + ' e) / 2 < ' e
e =
{|
  pos := (abs (q - r) + ' e) / 2;
  is_pos :=
    pos_mult_compat (abs (q - r) + ' e) (/ 2)
      (pos_plus_le_lt_compat_r 0 (abs (q - r)) (' e)
         (pos_is_pos e) (Qabs_nonneg (q - r)))
      (pos_dec_recip_compat 2 lt_0_2)
|} + Qpos_diff ((abs (q - r) + ' e) / 2) (' e) E2 apply pos_eq.
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
E: abs (q - r) < ' e
E1: abs (q - r) < (abs (q - r) + ' e) / 2
E2: (abs (q - r) + ' e) / 2 < ' e
' e =
' ({|
     pos := (abs (q - r) + ' e) / 2;
     is_pos :=
       pos_mult_compat (abs (q - r) + ' e) (/ 2)
         (pos_plus_le_lt_compat_r 0 (abs (q - r))
            (' e) (pos_is_pos e) (Qabs_nonneg (q - r)))
         (pos_dec_recip_compat 2 lt_0_2)
   |} + Qpos_diff ((abs (q - r) + ' e) / 2) (' e) E2) exact (Qpos_diff_pr _ _ E2).
  +
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
E: abs (q - r) < ' e
E1: abs (q - r) < (abs (q - r) + ' e) / 2
E2: (abs (q - r) + ' e) / 2 < ' e
close
  {|
    pos := (abs (q - r) + ' e) / 2;
    is_pos :=
      pos_mult_compat (abs (q - r) + ' e) (/ 2)
        (pos_plus_le_lt_compat_r 0 (abs (q - r)) (' e)
           (pos_is_pos e) (Qabs_nonneg (q - r)))
        (pos_dec_recip_compat 2 lt_0_2)
  |} q r apply Qclose_alt.
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
E: abs (q - r) < ' e
E1: abs (q - r) < (abs (q - r) + ' e) / 2
E2: (abs (q - r) + ' e) / 2 < ' e
abs (q - r) <
' {|
    pos := (abs (q - r) + ' e) / 2;
    is_pos :=
      pos_mult_compat (abs (q - r) + ' e) (/ 2)
        (pos_plus_le_lt_compat_r 0 (abs (q - r)) (' e)
           (pos_is_pos e) (Qabs_nonneg (q - r)))
        (pos_dec_recip_compat 2 lt_0_2)
  |} exact E1.
-
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
merely
  {d : Q+ &
  {d' : Q+ & ((e = (d + d')%mc) * close d q r)%type}} ->
close e q r apply (Trunc_ind _).
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
{d : Q+ &
{d' : Q+ & ((e = (d + d')%mc) * close d q r)%type}} ->
close e q r intros [d [d' [He xi]]].
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
d, d': Q+
He: e = d + d'
xi: close d q r
close e q r
  apply Qclose_alt;rewrite He.
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
d, d': Q+
He: e = d + d'
xi: close d q r
abs (q - r) < ' (d + d')
  apply Qclose_alt in xi.
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
d, d': Q+
He: e = d + d'
xi: abs (q - r) < ' d
abs (q - r) < ' (d + d')
  apply lt_le_trans with (' d);trivial.
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
d, d': Q+
He: e = d + d'
xi: abs (q - r) < ' d
' d ≤ ' (d + d')
  apply nonneg_plus_le_compat_r.
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
d, d': Q+
He: e = d + d'
xi: abs (q - r) < ' d
0 ≤ ' d' solve_propholds.
Qed.

Global Instance Q_premetric@{} : PreMetric Q.
funext: Funext
univalence: Univalence
PreMetric Q
Proof.
funext: Funext
univalence: Univalence
PreMetric Q
split;try apply _.
funext: Funext
univalence: Univalence
forall e : Q+, Reflexive (close e)
intros e u;apply Qclose_alt.
funext: Funext
univalence: Univalence
e: Q+
u: Q
abs (u - u) < ' e rewrite plus_negate_r.
funext: Funext
univalence: Univalence
e: Q+
u: Q
abs 0 < ' e
unfold abs.
funext: Funext
univalence: Univalence
e: Q+
u: Q
(abs_sig 0).1 < ' e rewrite (fst (abs_sig 0).2).
funext: Funext
univalence: Univalence
e: Q+
u: Q
0 < ' e
funext: Funext
univalence: Univalence
e: Q+
u: Q
0 ≤ 0
-
funext: Funext
univalence: Univalence
e: Q+
u: Q
0 < ' e solve_propholds.
-
funext: Funext
univalence: Univalence
e: Q+
u: Q
0 ≤ 0 reflexivity.
Qed.

Global Instance Qneg_nonexpanding@{} : NonExpanding ((-) : Negate Q).
funext: Funext
univalence: Univalence
NonExpanding (negate : Negate Q)
Proof.
funext: Funext
univalence: Univalence
NonExpanding (negate : Negate Q)
intros e x y.
funext: Funext
univalence: Univalence
e: Q+
x, y: Q
close e x y -> close e (- x) (- y)
apply Qclose_neg.
Defined.


Global Instance Qplus_nonexpanding_l@{} : forall s : Q, NonExpanding (+ s).
funext: Funext
univalence: Univalence
forall s : Q, NonExpanding (fun y : Q => y + s)
Proof.
funext: Funext
univalence: Univalence
forall s : Q, NonExpanding (fun y : Q => y + s)
red.
funext: Funext
univalence: Univalence
forall (s : Q) (e : Q+) (x y : Q),
close e x y -> close e (x + s) (y + s) unfold close,Q_close;simpl.
funext: Funext
univalence: Univalence
forall (s : Q) (e : Q+) (x y : Q),
- ' e < x - y < ' e -> - ' e < x + s - (y + s) < ' e intros s e q r E.
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
E: - ' e < q - r < ' e
- ' e < q + s - (r + s) < ' e
assert (Hrw : q + s - (r + s) = q - r)
  by abstract ring_tac.ring_with_integers (NatPair.Z nat).
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
E: - ' e < q - r < ' e
Hrw: q + s - (r + s) = q - r
- ' e < q + s - (r + s) < ' e
rewrite Hrw;trivial.
Qed.

Global Instance Qplus_nonexpanding_r@{} : forall s : Q, NonExpanding (s +).
funext: Funext
univalence: Univalence
forall s : Q, NonExpanding (plus s)
Proof.
funext: Funext
univalence: Univalence
forall s : Q, NonExpanding (plus s)
red;unfold close,Q_close;simpl.
funext: Funext
univalence: Univalence
forall (s : Q) (e : Q+) (x y : Q),
- ' e < x - y < ' e -> - ' e < s + x - (s + y) < ' e intros s e q r E.
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
E: - ' e < q - r < ' e
- ' e < s + q - (s + r) < ' e
assert (Hrw : s + q - (s + r) = q - r)
  by abstract ring_tac.ring_with_integers (NatPair.Z nat).
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
E: - ' e < q - r < ' e
Hrw: s + q - (s + r) = q - r
- ' e < s + q - (s + r) < ' e
rewrite Hrw;trivial.
Qed.

Global Instance Qabs_nonexpanding : NonExpanding (abs (A:=Q)).
funext: Funext
univalence: Univalence
NonExpanding abs
Proof.
funext: Funext
univalence: Univalence
NonExpanding abs
intros e q r xi.
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
xi: close e q r
close e (abs q) (abs r)
apply Qclose_alt in xi;apply Qclose_alt.
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
xi: abs (q - r) < ' e
abs (abs q - abs r) < ' e
apply le_lt_trans with (abs (q - r));trivial.
funext: Funext
univalence: Univalence
e: Q+
q, r: Q
xi: abs (q - r) < ' e
abs (abs q - abs r) ≤ abs (q - r)
apply Qabs_triangle_alt.
Qed.

Global Instance Qmeet_nonexpanding_l : forall s : Q, NonExpanding (⊓ s).
funext: Funext
univalence: Univalence
forall s : Q, NonExpanding (fun Y : Q => Y ⊓ s)
Proof.
funext: Funext
univalence: Univalence
forall s : Q, NonExpanding (fun Y : Q => Y ⊓ s)
intros s e q r xi.
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
xi: close e q r
close e (q ⊓ s) (r ⊓ s)
apply Qclose_alt;apply Qclose_alt in xi.
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
xi: abs (q - r) < ' e
abs (q ⊓ s - (r ⊓ s)) < ' e
apply le_lt_trans with (abs (q - r));trivial.
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
xi: abs (q - r) < ' e
abs (q ⊓ s - (r ⊓ s)) ≤ abs (q - r) clear xi.
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
abs (q ⊓ s - (r ⊓ s)) ≤ abs (q - r)
destruct (total le q s) as [E1|E1], (total le r s) as [E2|E2];
rewrite ?(meet_l _ _ E1), ?(meet_r _ _ E1), ?(meet_l _ _ E2), ?(meet_r _ _ E2).
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
E1: q ≤ s
E2: r ≤ s
abs (q - r) ≤ abs (q - r)
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
E1: q ≤ s
E2: s ≤ r
abs (q - s) ≤ abs (q - r)
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
E1: s ≤ q
E2: r ≤ s
abs (s - r) ≤ abs (q - r)
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
E1: s ≤ q
E2: s ≤ r
abs (s - s) ≤ abs (q - r)
-
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
E1: q ≤ s
E2: r ≤ s
abs (q - r) ≤ abs (q - r) reflexivity.
-
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
E1: q ≤ s
E2: s ≤ r
abs (q - s) ≤ abs (q - r) rewrite (Qabs_of_nonpos (q - r))
  by (apply (snd (flip_nonpos_minus _ _)); transitivity s;trivial).
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
E1: q ≤ s
E2: s ≤ r
abs (q - s) ≤ - (q - r)
  rewrite <-negate_swap_r.
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
E1: q ≤ s
E2: s ≤ r
abs (q - s) ≤ r - q
  rewrite (Qabs_of_nonpos _ (snd (flip_nonpos_minus _ _) E1)).
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
E1: q ≤ s
E2: s ≤ r
- (q - s) ≤ r - q
  rewrite <-negate_swap_r.
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
E1: q ≤ s
E2: s ≤ r
s - q ≤ r - q
  apply (order_preserving (+ (- q))).
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
E1: q ≤ s
E2: s ≤ r
s ≤ r
  trivial.
-
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
E1: s ≤ q
E2: r ≤ s
abs (s - r) ≤ abs (q - r) rewrite (Qabs_of_nonneg (q - r))
  by (apply (snd (flip_nonneg_minus _ _)); transitivity s;trivial).
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
E1: s ≤ q
E2: r ≤ s
abs (s - r) ≤ q - r
  rewrite (Qabs_of_nonneg _ (snd (flip_nonneg_minus _ _) E2)).
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
E1: s ≤ q
E2: r ≤ s
s - r ≤ q - r
  apply (order_preserving (+ (- r))).
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
E1: s ≤ q
E2: r ≤ s
s ≤ q trivial.
-
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
E1: s ≤ q
E2: s ≤ r
abs (s - s) ≤ abs (q - r) rewrite plus_negate_r,Qabs_of_nonneg by reflexivity.
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
E1: s ≤ q
E2: s ≤ r
0 ≤ abs (q - r)
  apply Qabs_nonneg.
Qed.

Global Instance Qmeet_nonexpanding_r : forall s : Q, NonExpanding (s ⊓).
funext: Funext
univalence: Univalence
forall s : Q, NonExpanding (meet s)
Proof.
funext: Funext
univalence: Univalence
forall s : Q, NonExpanding (meet s)
intros s e q r xi.
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
xi: close e q r
close e (s ⊓ q) (s ⊓ r)
pose proof meet_sl_order_meet_sl.
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
xi: close e q r
X: IsMeetSemiLattice Q
close e (s ⊓ q) (s ⊓ r)
rewrite !(commutativity s).
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
xi: close e q r
X: IsMeetSemiLattice Q
close e (q ⊓ s) (r ⊓ s)
apply (non_expanding (fun x => meet x s)).
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
xi: close e q r
X: IsMeetSemiLattice Q
close e q r trivial.
Qed.

Global Instance Qjoin_nonexpanding_l : forall s : Q, NonExpanding (⊔ s).
funext: Funext
univalence: Univalence
forall s : Q, NonExpanding (fun Y : Q => Y ⊔ s)
Proof.
funext: Funext
univalence: Univalence
forall s : Q, NonExpanding (fun Y : Q => Y ⊔ s)
intros s e q r xi.
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
xi: close e q r
close e (q ⊔ s) (r ⊔ s)
apply Qclose_alt;apply Qclose_alt in xi.
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
xi: abs (q - r) < ' e
abs (q ⊔ s - (r ⊔ s)) < ' e
apply le_lt_trans with (abs (q - r));trivial.
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
xi: abs (q - r) < ' e
abs (q ⊔ s - (r ⊔ s)) ≤ abs (q - r) clear xi.
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
abs (q ⊔ s - (r ⊔ s)) ≤ abs (q - r)
destruct (total le q s) as [E1|E1], (total le r s) as [E2|E2];
rewrite ?(join_l _ _ E1), ?(join_r _ _ E1), ?(join_l _ _ E2), ?(join_r _ _ E2).
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
E1: q ≤ s
E2: r ≤ s
abs (s - s) ≤ abs (q - r)
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
E1: q ≤ s
E2: s ≤ r
abs (s - r) ≤ abs (q - r)
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
E1: s ≤ q
E2: r ≤ s
abs (q - s) ≤ abs (q - r)
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
E1: s ≤ q
E2: s ≤ r
abs (q - r) ≤ abs (q - r)
-
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
E1: q ≤ s
E2: r ≤ s
abs (s - s) ≤ abs (q - r) rewrite plus_negate_r,Qabs_of_nonneg by reflexivity.
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
E1: q ≤ s
E2: r ≤ s
0 ≤ abs (q - r)
  apply Qabs_nonneg.
-
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
E1: q ≤ s
E2: s ≤ r
abs (s - r) ≤ abs (q - r) rewrite (Qabs_of_nonpos (q - r))
  by (apply (snd (flip_nonpos_minus _ _)); transitivity s;trivial).
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
E1: q ≤ s
E2: s ≤ r
abs (s - r) ≤ - (q - r)
  rewrite <-negate_swap_r.
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
E1: q ≤ s
E2: s ≤ r
abs (s - r) ≤ r - q
  rewrite (Qabs_of_nonpos _ (snd (flip_nonpos_minus _ _) E2)).
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
E1: q ≤ s
E2: s ≤ r
- (s - r) ≤ r - q
  rewrite <-negate_swap_r.
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
E1: q ≤ s
E2: s ≤ r
r - s ≤ r - q
  apply (order_preserving (r +)).
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
E1: q ≤ s
E2: s ≤ r
- s ≤ - q
  apply (snd (flip_le_negate _ _)).
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
E1: q ≤ s
E2: s ≤ r
q ≤ s trivial.
-
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
E1: s ≤ q
E2: r ≤ s
abs (q - s) ≤ abs (q - r) rewrite (Qabs_of_nonneg (q - r))
  by (apply (snd (flip_nonneg_minus _ _)); transitivity s;trivial).
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
E1: s ≤ q
E2: r ≤ s
abs (q - s) ≤ q - r
  rewrite (Qabs_of_nonneg _ (snd (flip_nonneg_minus _ _) E1)).
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
E1: s ≤ q
E2: r ≤ s
q - s ≤ q - r
  apply (order_preserving (q +)).
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
E1: s ≤ q
E2: r ≤ s
- s ≤ - r
  apply (snd (flip_le_negate _ _)).
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
E1: s ≤ q
E2: r ≤ s
r ≤ s trivial.
-
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
E1: s ≤ q
E2: s ≤ r
abs (q - r) ≤ abs (q - r) reflexivity.
Qed.

Global Instance Qjoin_nonexpanding_r : forall s : Q, NonExpanding (s ⊔).
funext: Funext
univalence: Univalence
forall s : Q, NonExpanding (join s)
Proof.
funext: Funext
univalence: Univalence
forall s : Q, NonExpanding (join s)
intros s e q r xi.
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
xi: close e q r
close e (s ⊔ q) (s ⊔ r)
pose proof join_sl_order_join_sl.
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
xi: close e q r
X: IsJoinSemiLattice Q
close e (s ⊔ q) (s ⊔ r)
rewrite !(commutativity s).
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
xi: close e q r
X: IsJoinSemiLattice Q
close e (q ⊔ s) (r ⊔ s)
apply (non_expanding (fun x => join x s)).
funext: Funext
univalence: Univalence
s: Q
e: Q+
q, r: Q
xi: close e q r
X: IsJoinSemiLattice Q
close e q r trivial.
Qed.

Global Instance Qmult_lipschitz@{} : forall q : Q, Lipschitz (q *.) (pos_of_Q q).
funext: Funext
univalence: Univalence
forall q : Q, Lipschitz (mult q) (pos_of_Q q)
Proof.
funext: Funext
univalence: Univalence
forall q : Q, Lipschitz (mult q) (pos_of_Q q)
intros q e x y xi.
funext: Funext
univalence: Univalence
q: Q
e: Q+
x, y: Q
xi: close e x y
close (pos_of_Q q * e) (q * x) (q * y)
apply Qclose_alt.
funext: Funext
univalence: Univalence
q: Q
e: Q+
x, y: Q
xi: close e x y
abs (q * x - q * y) < ' (pos_of_Q q * e)
rewrite negate_mult_distr_r,<-plus_mult_distr_l,Qabs_mult.
funext: Funext
univalence: Univalence
q: Q
e: Q+
x, y: Q
xi: close e x y
abs q * abs (x - y) < ' (pos_of_Q q * e)
apply pos_mult_le_lt_compat;try split.
funext: Funext
univalence: Univalence
q: Q
e: Q+
x, y: Q
xi: close e x y
0 ≤ abs q
funext: Funext
univalence: Univalence
q: Q
e: Q+
x, y: Q
xi: close e x y
abs q ≤ ' pos_of_Q q
funext: Funext
univalence: Univalence
q: Q
e: Q+
x, y: Q
xi: close e x y
0 < ' pos_of_Q q
funext: Funext
univalence: Univalence
q: Q
e: Q+
x, y: Q
xi: close e x y
0 ≤ abs (x - y)
funext: Funext
univalence: Univalence
q: Q
e: Q+
x, y: Q
xi: close e x y
abs (x - y) < ' e
-
funext: Funext
univalence: Univalence
q: Q
e: Q+
x, y: Q
xi: close e x y
0 ≤ abs q apply Qabs_nonneg.
-
funext: Funext
univalence: Univalence
q: Q
e: Q+
x, y: Q
xi: close e x y
abs q ≤ ' pos_of_Q q rewrite Qabs_is_join.
funext: Funext
univalence: Univalence
q: Q
e: Q+
x, y: Q
xi: close e x y
- q ⊔ q ≤ ' pos_of_Q q apply join_le.
funext: Funext
univalence: Univalence
q: Q
e: Q+
x, y: Q
xi: close e x y
- q ≤ ' pos_of_Q q
funext: Funext
univalence: Univalence
q: Q
e: Q+
x, y: Q
xi: close e x y
q ≤ ' pos_of_Q q
  +
funext: Funext
univalence: Univalence
q: Q
e: Q+
x, y: Q
xi: close e x y
- q ≤ ' pos_of_Q q apply flip_le_negate;rewrite involutive; apply Q_abs_plus_1_bounds.
  +
funext: Funext
univalence: Univalence
q: Q
e: Q+
x, y: Q
xi: close e x y
q ≤ ' pos_of_Q q apply Q_abs_plus_1_bounds.
-
funext: Funext
univalence: Univalence
q: Q
e: Q+
x, y: Q
xi: close e x y
0 < ' pos_of_Q q solve_propholds.
-
funext: Funext
univalence: Univalence
q: Q
e: Q+
x, y: Q
xi: close e x y
0 ≤ abs (x - y) apply Qabs_nonneg.
-
funext: Funext
univalence: Univalence
q: Q
e: Q+
x, y: Q
xi: close e x y
abs (x - y) < ' e apply Qclose_alt,xi.
Qed.

Global Instance Qpos_upper_close e : Closeness (Qpos_upper e)
  := fun n x y => close n x.1 y.1.
Arguments Qpos_upper_close _ _ _ _ /.

Global Instance Q_recip_lipschitz (e : Q+)
  : Lipschitz ((/) ∘ pr1 ∘ (Qpos_upper_inject e)) (/ (e * e)).
funext: Funext
univalence: Univalence
e: Q+
Lipschitz (dec_recip ∘ pr1 ∘ Qpos_upper_inject e)
  (/ (e * e))
Proof.
funext: Funext
univalence: Univalence
e: Q+
Lipschitz (dec_recip ∘ pr1 ∘ Qpos_upper_inject e)
  (/ (e * e))
intros n q r xi.
funext: Funext
univalence: Univalence
e, n: Q+
q, r: Q
xi: close n q r
close (/ (e * e) * n)
  ((dec_recip ∘ pr1 ∘ Qpos_upper_inject e) q)
  ((dec_recip ∘ pr1 ∘ Qpos_upper_inject e) r)
unfold Compose;simpl.
funext: Funext
univalence: Univalence
e, n: Q+
q, r: Q
xi: close n q r
close (/ (e * e) * n) (/ (q ⊔ ' e)) (/ (r ⊔ ' e)) apply Qclose_alt.
funext: Funext
univalence: Univalence
e, n: Q+
q, r: Q
xi: close n q r
abs (/ (q ⊔ ' e) - / (r ⊔ ' e)) < ' (/ (e * e) * n)
assert (PropHolds (0 < join q (' e))) as E
  by (apply lt_le_trans with (' e);[solve_propholds|apply join_ub_r]).
funext: Funext
univalence: Univalence
e, n: Q+
q, r: Q
xi: close n q r
E: PropHolds (0 < q ⊔ ' e)
abs (/ (q ⊔ ' e) - / (r ⊔ ' e)) < ' (/ (e * e) * n)
apply (strictly_order_reflecting ((join q (' e)) *.)).
funext: Funext
univalence: Univalence
e, n: Q+
q, r: Q
xi: close n q r
E: PropHolds (0 < q ⊔ ' e)
(q ⊔ ' e) * abs (/ (q ⊔ ' e) - / (r ⊔ ' e)) <
(q ⊔ ' e) * ' (/ (e * e) * n)
assert (PropHolds (0 < join r (' e))) as E'
  by (apply lt_le_trans with (' e);[solve_propholds|apply join_ub_r]).
funext: Funext
univalence: Univalence
e, n: Q+
q, r: Q
xi: close n q r
E: PropHolds (0 < q ⊔ ' e)
E': PropHolds (0 < r ⊔ ' e)
(q ⊔ ' e) * abs (/ (q ⊔ ' e) - / (r ⊔ ' e)) <
(q ⊔ ' e) * ' (/ (e * e) * n)
apply (strictly_order_reflecting ((join r (' e)) *.)).
funext: Funext
univalence: Univalence
e, n: Q+
q, r: Q
xi: close n q r
E: PropHolds (0 < q ⊔ ' e)
E': PropHolds (0 < r ⊔ ' e)
(r ⊔ ' e) *
((q ⊔ ' e) * abs (/ (q ⊔ ' e) - / (r ⊔ ' e))) <
(r ⊔ ' e) * ((q ⊔ ' e) * ' (/ (e * e) * n))
set (X := join r (' e)) at 2 3.
funext: Funext
univalence: Univalence
e, n: Q+
q, r: Q
xi: close n q r
E: PropHolds (0 < q ⊔ ' e)
E': PropHolds (0 < r ⊔ ' e)
X:= r ⊔ ' e: Q
(r ⊔ ' e) * ((q ⊔ ' e) * abs (/ (q ⊔ ' e) - / X)) <
X * ((q ⊔ ' e) * ' (/ (e * e) * n))
rewrite <-(Qabs_of_nonneg (join r _)) by solve_propholds.
funext: Funext
univalence: Univalence
e, n: Q+
q, r: Q
xi: close n q r
E: PropHolds (0 < q ⊔ ' e)
E': PropHolds (0 < r ⊔ ' e)
X:= r ⊔ ' e: Q
abs (r ⊔ ' e) * ((q ⊔ ' e) * abs (/ (q ⊔ ' e) - / X)) <
X * ((q ⊔ ' e) * ' (/ (e * e) * n))
set (Y := join q (' e)) at 2 3.
funext: Funext
univalence: Univalence
e, n: Q+
q, r: Q
xi: close n q r
E: PropHolds (0 < q ⊔ ' e)
E': PropHolds (0 < r ⊔ ' e)
X:= r ⊔ ' e: Q
Y:= q ⊔ ' e: Q
abs (r ⊔ ' e) * ((q ⊔ ' e) * abs (/ Y - / X)) <
X * (Y * ' (/ (e * e) * n))
rewrite <-(Qabs_of_nonneg (join q _)) by solve_propholds.
funext: Funext
univalence: Univalence
e, n: Q+
q, r: Q
xi: close n q r
E: PropHolds (0 < q ⊔ ' e)
E': PropHolds (0 < r ⊔ ' e)
X:= r ⊔ ' e: Q
Y:= q ⊔ ' e: Q
abs (r ⊔ ' e) * (abs (q ⊔ ' e) * abs (/ Y - / X)) <
X * (Y * ' (/ (e * e) * n))
rewrite <-!Qabs_mult.
funext: Funext
univalence: Univalence
e, n: Q+
q, r: Q
xi: close n q r
E: PropHolds (0 < q ⊔ ' e)
E': PropHolds (0 < r ⊔ ' e)
X:= r ⊔ ' e: Q
Y:= q ⊔ ' e: Q
abs ((r ⊔ ' e) * ((q ⊔ ' e) * (/ Y - / X))) <
X * (Y * ' (/ (e * e) * n))
rewrite !(plus_mult_distr_l (Aplus:=Qplus)).
funext: Funext
univalence: Univalence
e, n: Q+
q, r: Q
xi: close n q r
E: PropHolds (0 < q ⊔ ' e)
E': PropHolds (0 < r ⊔ ' e)
X:= r ⊔ ' e: Q
Y:= q ⊔ ' e: Q
abs
  ((r ⊔ ' e) * ((q ⊔ ' e) / Y) +
   (r ⊔ ' e) * ((q ⊔ ' e) * - / X)) <
X * (Y * ' (/ (e * e) * n))
rewrite dec_recip_inverse by (apply irrefl_neq,symmetric_neq in E;trivial).
funext: Funext
univalence: Univalence
e, n: Q+
q, r: Q
xi: close n q r
E: PropHolds (0 < q ⊔ ' e)
E': PropHolds (0 < r ⊔ ' e)
X:= r ⊔ ' e: Q
Y:= q ⊔ ' e: Q
abs ((r ⊔ ' e) * 1 + (r ⊔ ' e) * ((q ⊔ ' e) * - / X)) <
X * (Y * ' (/ (e * e) * n))
rewrite mult_1_r.
funext: Funext
univalence: Univalence
e, n: Q+
q, r: Q
xi: close n q r
E: PropHolds (0 < q ⊔ ' e)
E': PropHolds (0 < r ⊔ ' e)
X:= r ⊔ ' e: Q
Y:= q ⊔ ' e: Q
abs (r ⊔ ' e + (r ⊔ ' e) * ((q ⊔ ' e) * - / X)) <
X * (Y * ' (/ (e * e) * n))
assert (Hrw :  (r ⊔ ' e) * ((q ⊔ ' e) * - / (r ⊔ ' e)) = - Y * (X / X))
  by ring_tac.ring_with_integers (NatPair.Z nat).
funext: Funext
univalence: Univalence
e, n: Q+
q, r: Q
xi: close n q r
E: PropHolds (0 < q ⊔ ' e)
E': PropHolds (0 < r ⊔ ' e)
X:= r ⊔ ' e: Q
Y:= q ⊔ ' e: Q
Hrw: (r ⊔ ' e) * ((q ⊔ ' e) * - / (r ⊔ ' e)) =
- Y * (X / X)
abs (r ⊔ ' e + (r ⊔ ' e) * ((q ⊔ ' e) * - / X)) <
X * (Y * ' (/ (e * e) * n))
rewrite Hrw;clear Hrw.
funext: Funext
univalence: Univalence
e, n: Q+
q, r: Q
xi: close n q r
E: PropHolds (0 < q ⊔ ' e)
E': PropHolds (0 < r ⊔ ' e)
X:= r ⊔ ' e: Q
Y:= q ⊔ ' e: Q
abs (r ⊔ ' e + - Y * (X / X)) <
X * (Y * ' (/ (e * e) * n))
rewrite dec_recip_inverse by (apply irrefl_neq,symmetric_neq in E';trivial).
funext: Funext
univalence: Univalence
e, n: Q+
q, r: Q
xi: close n q r
E: PropHolds (0 < q ⊔ ' e)
E': PropHolds (0 < r ⊔ ' e)
X:= r ⊔ ' e: Q
Y:= q ⊔ ' e: Q
abs (r ⊔ ' e + - Y * 1) < X * (Y * ' (/ (e * e) * n))
rewrite mult_1_r.
funext: Funext
univalence: Univalence
e, n: Q+
q, r: Q
xi: close n q r
E: PropHolds (0 < q ⊔ ' e)
E': PropHolds (0 < r ⊔ ' e)
X:= r ⊔ ' e: Q
Y:= q ⊔ ' e: Q
abs (r ⊔ ' e - Y) < X * (Y * ' (/ (e * e) * n)) unfold X, Y.
funext: Funext
univalence: Univalence
e, n: Q+
q, r: Q
xi: close n q r
E: PropHolds (0 < q ⊔ ' e)
E': PropHolds (0 < r ⊔ ' e)
X:= r ⊔ ' e: Q
Y:= q ⊔ ' e: Q
abs (r ⊔ ' e - (q ⊔ ' e)) <
(r ⊔ ' e) * ((q ⊔ ' e) * ' (/ (e * e) * n))
eapply lt_le_trans.
funext: Funext
univalence: Univalence
e, n: Q+
q, r: Q
xi: close n q r
E: PropHolds (0 < q ⊔ ' e)
E': PropHolds (0 < r ⊔ ' e)
X:= r ⊔ ' e: Q
Y:= q ⊔ ' e: Q
abs (r ⊔ ' e - (q ⊔ ' e)) < ?y
funext: Funext
univalence: Univalence
e, n: Q+
q, r: Q
xi: close n q r
E: PropHolds (0 < q ⊔ ' e)
E': PropHolds (0 < r ⊔ ' e)
X:= r ⊔ ' e: Q
Y:= q ⊔ ' e: Q
?y ≤ (r ⊔ ' e) * ((q ⊔ ' e) * ' (/ (e * e) * n))
-
funext: Funext
univalence: Univalence
e, n: Q+
q, r: Q
xi: close n q r
E: PropHolds (0 < q ⊔ ' e)
E': PropHolds (0 < r ⊔ ' e)
X:= r ⊔ ' e: Q
Y:= q ⊔ ' e: Q
abs (r ⊔ ' e - (q ⊔ ' e)) < ?y apply Qclose_alt.
funext: Funext
univalence: Univalence
e, n: Q+
q, r: Q
xi: close n q r
E: PropHolds (0 < q ⊔ ' e)
E': PropHolds (0 < r ⊔ ' e)
X:= r ⊔ ' e: Q
Y:= q ⊔ ' e: Q
close ?e (r ⊔ ' e) (q ⊔ ' e) eapply (non_expanding (⊔ ' e)).
funext: Funext
univalence: Univalence
e, n: Q+
q, r: Q
xi: close n q r
E: PropHolds (0 < q ⊔ ' e)
E': PropHolds (0 < r ⊔ ' e)
X:= r ⊔ ' e: Q
Y:= q ⊔ ' e: Q
close ?e r q symmetry.
funext: Funext
univalence: Univalence
e, n: Q+
q, r: Q
xi: close n q r
E: PropHolds (0 < q ⊔ ' e)
E': PropHolds (0 < r ⊔ ' e)
X:= r ⊔ ' e: Q
Y:= q ⊔ ' e: Q
close ?e q r apply xi.
-
funext: Funext
univalence: Univalence
e, n: Q+
q, r: Q
xi: close n q r
E: PropHolds (0 < q ⊔ ' e)
E': PropHolds (0 < r ⊔ ' e)
X:= r ⊔ ' e: Q
Y:= q ⊔ ' e: Q
' n ≤ (r ⊔ ' e) * ((q ⊔ ' e) * ' (/ (e * e) * n)) transitivity (' (((e * e) / (e * e)) * n)).
funext: Funext
univalence: Univalence
e, n: Q+
q, r: Q
xi: close n q r
E: PropHolds (0 < q ⊔ ' e)
E': PropHolds (0 < r ⊔ ' e)
X:= r ⊔ ' e: Q
Y:= q ⊔ ' e: Q
' n ≤ ' (e * e / (e * e) * n)
funext: Funext
univalence: Univalence
e, n: Q+
q, r: Q
xi: close n q r
E: PropHolds (0 < q ⊔ ' e)
E': PropHolds (0 < r ⊔ ' e)
X:= r ⊔ ' e: Q
Y:= q ⊔ ' e: Q
' (e * e / (e * e) * n)
≤ (r ⊔ ' e) * ((q ⊔ ' e) * ' (/ (e * e) * n))
  +
funext: Funext
univalence: Univalence
e, n: Q+
q, r: Q
xi: close n q r
E: PropHolds (0 < q ⊔ ' e)
E': PropHolds (0 < r ⊔ ' e)
X:= r ⊔ ' e: Q
Y:= q ⊔ ' e: Q
' n ≤ ' (e * e / (e * e) * n) rewrite pos_recip_r,Qpos_mult_1_l;reflexivity.
  +
funext: Funext
univalence: Univalence
e, n: Q+
q, r: Q
xi: close n q r
E: PropHolds (0 < q ⊔ ' e)
E': PropHolds (0 < r ⊔ ' e)
X:= r ⊔ ' e: Q
Y:= q ⊔ ' e: Q
' (e * e / (e * e) * n)
≤ (r ⊔ ' e) * ((q ⊔ ' e) * ' (/ (e * e) * n)) rewrite <-!Qpos_mult_assoc.
funext: Funext
univalence: Univalence
e, n: Q+
q, r: Q
xi: close n q r
E: PropHolds (0 < q ⊔ ' e)
E': PropHolds (0 < r ⊔ ' e)
X:= r ⊔ ' e: Q
Y:= q ⊔ ' e: Q
' (e * (e * (/ (e * e) * n)))
≤ (r ⊔ ' e) * ((q ⊔ ' e) * ' (/ (e * e) * n))
    change (' (e * (e * (/ (e * e) * n)))) with (' e * (' e * ' (/ (e * e) * n))).
funext: Funext
univalence: Univalence
e, n: Q+
q, r: Q
xi: close n q r
E: PropHolds (0 < q ⊔ ' e)
E': PropHolds (0 < r ⊔ ' e)
X:= r ⊔ ' e: Q
Y:= q ⊔ ' e: Q
' e * (' e * ' (/ (e * e) * n))
≤ (r ⊔ ' e) * ((q ⊔ ' e) * ' (/ (e * e) * n))
    apply mult_le_compat;try solve_propholds;[apply join_ub_r|].
funext: Funext
univalence: Univalence
e, n: Q+
q, r: Q
xi: close n q r
E: PropHolds (0 < q ⊔ ' e)
E': PropHolds (0 < r ⊔ ' e)
X:= r ⊔ ' e: Q
Y:= q ⊔ ' e: Q
' e * ' (/ (e * e) * n)
≤ (q ⊔ ' e) * ' (/ (e * e) * n)
    apply mult_le_compat;try solve_propholds;[apply join_ub_r|].
funext: Funext
univalence: Univalence
e, n: Q+
q, r: Q
xi: close n q r
E: PropHolds (0 < q ⊔ ' e)
E': PropHolds (0 < r ⊔ ' e)
X:= r ⊔ ' e: Q
Y:= q ⊔ ' e: Q
' (/ (e * e) * n) ≤ ' (/ (e * e) * n)
    reflexivity.
Qed.

End rationals.

Section cauchy.
Universe UA.
Context {A : Type@{UA} } {Aclose : Closeness A}.
Context `{!PreMetric A}.

Lemma limit_unique : forall x l1 l2, IsLimit x l1 -> IsLimit x l2 -> l1 = l2.
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
forall (x : Approximation A) (l1 l2 : A),
IsLimit x l1 -> IsLimit x l2 -> l1 = l2
Proof.
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
forall (x : Approximation A) (l1 l2 : A),
IsLimit x l1 -> IsLimit x l2 -> l1 = l2
intros x l1 l2 E1 E2.
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
x: Approximation A
l1, l2: A
E1: IsLimit x l1
E2: IsLimit x l2
l1 = l2
apply separated.
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
x: Approximation A
l1, l2: A
E1: IsLimit x l1
E2: IsLimit x l2
forall e : Q+, close e l1 l2
intros e.
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
x: Approximation A
l1, l2: A
E1: IsLimit x l1
E2: IsLimit x l2
e: Q+
close e l1 l2 rewrite (pos_split2 e),(pos_split2 (e/2)).
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
x: Approximation A
l1, l2: A
E1: IsLimit x l1
E2: IsLimit x l2
e: Q+
close
  (e / 2 / 2 + e / 2 / 2 + (e / 2 / 2 + e / 2 / 2)) l1
  l2
apply triangular with (x (e / 2 / 2));[symmetry;apply E1|apply E2].
Qed.

Lemma equiv_through_approx0 : forall (y : Approximation A) ly, IsLimit y ly ->
  forall u e d, close e u (y d) -> close (e+d) u ly.
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
forall (y : Approximation A) (ly : A),
IsLimit y ly ->
forall (u : A) (e d : Q+),
close e u (y d) -> close (e + d) u ly
Proof.
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
forall (y : Approximation A) (ly : A),
IsLimit y ly ->
forall (u : A) (e d : Q+),
close e u (y d) -> close (e + d) u ly
intros y ly E1 u e d xi.
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
y: Approximation A
ly: A
E1: IsLimit y ly
u: A
e, d: Q+
xi: close e u (y d)
close (e + d) u ly
apply (merely_destruct ((fst (rounded _ _ _) xi))).
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
y: Approximation A
ly: A
E1: IsLimit y ly
u: A
e, d: Q+
xi: close e u (y d)
{d0 : Q+ &
{d' : Q+ &
((e = (d0 + d')%mc) * close d0 u (y d))%type}} ->
close (e + d) u ly
intros [d0 [d' [He E2]]].
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
y: Approximation A
ly: A
E1: IsLimit y ly
u: A
e, d: Q+
xi: close e u (y d)
d0, d': Q+
He: e = d0 + d'
E2: close d0 u (y d)
close (e + d) u ly
pose proof (triangular _ _ _ _ _ E2 (E1 d' _)) as E3.
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
y: Approximation A
ly: A
E1: IsLimit y ly
u: A
e, d: Q+
xi: close e u (y d)
d0, d': Q+
He: e = d0 + d'
E2: close d0 u (y d)
E3: close (d0 + (d' + d)) u ly
close (e + d) u ly
assert (Hrw : e + d = d0 + (d' + d));[|rewrite Hrw;trivial].
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
y: Approximation A
ly: A
E1: IsLimit y ly
u: A
e, d: Q+
xi: close e u (y d)
d0, d': Q+
He: e = d0 + d'
E2: close d0 u (y d)
E3: close (d0 + (d' + d)) u ly
e + d = d0 + (d' + d)
rewrite He.
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
y: Approximation A
ly: A
E1: IsLimit y ly
u: A
e, d: Q+
xi: close e u (y d)
d0, d': Q+
He: e = d0 + d'
E2: close d0 u (y d)
E3: close (d0 + (d' + d)) u ly
d0 + d' + d = d0 + (d' + d) symmetry.
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
y: Approximation A
ly: A
E1: IsLimit y ly
u: A
e, d: Q+
xi: close e u (y d)
d0, d': Q+
He: e = d0 + d'
E2: close d0 u (y d)
E3: close (d0 + (d' + d)) u ly
d0 + (d' + d) = d0 + d' + d apply Qpos_plus_assoc.
Qed.

Context {Alim : Lim A} `{!CauchyComplete A}.

Lemma equiv_through_approx : forall u (y : Approximation A) e d,
  close e u (y d) -> close (e+d) u (lim y).
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
Alim: Lim A
CauchyComplete0: CauchyComplete A
forall (u : A) (y : Approximation A) (e d : Q+),
close e u (y d) -> close (e + d) u (lim y)
Proof.
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
Alim: Lim A
CauchyComplete0: CauchyComplete A
forall (u : A) (y : Approximation A) (e d : Q+),
close e u (y d) -> close (e + d) u (lim y)
intros u y;apply equiv_through_approx0.
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
Alim: Lim A
CauchyComplete0: CauchyComplete A
u: A
y: Approximation A
IsLimit y (lim y) apply cauchy_complete.
Qed.

Lemma equiv_lim_lim (x y : Approximation A) (e d n e' : Q+)
  : e = d + n + e' -> close e' (x d) (y n) -> close e (lim x) (lim y).
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
Alim: Lim A
CauchyComplete0: CauchyComplete A
x, y: Approximation A
e, d, n, e': Q+
e = d + n + e' ->
close e' (x d) (y n) -> close e (lim x) (lim y)
Proof.
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
Alim: Lim A
CauchyComplete0: CauchyComplete A
x, y: Approximation A
e, d, n, e': Q+
e = d + n + e' ->
close e' (x d) (y n) -> close e (lim x) (lim y)
intros He xi.
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
Alim: Lim A
CauchyComplete0: CauchyComplete A
x, y: Approximation A
e, d, n, e': Q+
He: e = d + n + e'
xi: close e' (x d) (y n)
close e (lim x) (lim y)
rewrite He.
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
Alim: Lim A
CauchyComplete0: CauchyComplete A
x, y: Approximation A
e, d, n, e': Q+
He: e = d + n + e'
xi: close e' (x d) (y n)
close (d + n + e') (lim x) (lim y)
assert (Hrw : d + n + e' = e' + d + n) by (apply pos_eq;ring_tac.ring_with_nat);
rewrite Hrw;clear Hrw.
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
Alim: Lim A
CauchyComplete0: CauchyComplete A
x, y: Approximation A
e, d, n, e': Q+
He: e = d + n + e'
xi: close e' (x d) (y n)
close (e' + d + n) (lim x) (lim y)
apply equiv_through_approx.
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
Alim: Lim A
CauchyComplete0: CauchyComplete A
x, y: Approximation A
e, d, n, e': Q+
He: e = d + n + e'
xi: close e' (x d) (y n)
close (e' + d) (lim x) (y n)
symmetry.
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
Alim: Lim A
CauchyComplete0: CauchyComplete A
x, y: Approximation A
e, d, n, e': Q+
He: e = d + n + e'
xi: close e' (x d) (y n)
close (e' + d) (y n) (lim x) apply equiv_through_approx.
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
Alim: Lim A
CauchyComplete0: CauchyComplete A
x, y: Approximation A
e, d, n, e': Q+
He: e = d + n + e'
xi: close e' (x d) (y n)
close e' (y n) (x d) symmetry;trivial.
Qed.

Lemma lim_same_distance@{} : forall (x y : Approximation A) e,
  (forall d n, close (e+d) (x n) (y n)) ->
  forall d, close (e+d) (lim x) (lim y).
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
Alim: Lim A
CauchyComplete0: CauchyComplete A
forall (x y : Approximation A) (e : Q+),
(forall d n : Q+, close (e + d) (x n) (y n)) ->
forall d : Q+, close (e + d) (lim x) (lim y)
Proof.
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
Alim: Lim A
CauchyComplete0: CauchyComplete A
forall (x y : Approximation A) (e : Q+),
(forall d n : Q+, close (e + d) (x n) (y n)) ->
forall d : Q+, close (e + d) (lim x) (lim y)
intros x y e E d.
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
Alim: Lim A
CauchyComplete0: CauchyComplete A
x, y: Approximation A
e: Q+
E: forall d n : Q+, close (e + d) (x n) (y n)
d: Q+
close (e + d) (lim x) (lim y)
apply equiv_lim_lim with (d/3) (d/3) (e + d/3);[|apply E].
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
Alim: Lim A
CauchyComplete0: CauchyComplete A
x, y: Approximation A
e: Q+
E: forall d n : Q+, close (e + d) (x n) (y n)
d: Q+
e + d = d / 3 + d / 3 + (e + d / 3)
path_via (e + 3 / 3 * d).
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
Alim: Lim A
CauchyComplete0: CauchyComplete A
x, y: Approximation A
e: Q+
E: forall d n : Q+, close (e + d) (x n) (y n)
d: Q+
e + d = e + 3 / 3 * d
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
Alim: Lim A
CauchyComplete0: CauchyComplete A
x, y: Approximation A
e: Q+
E: forall d n : Q+, close (e + d) (x n) (y n)
d: Q+
e + 3 / 3 * d = d / 3 + d / 3 + (e + d / 3)
-
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
Alim: Lim A
CauchyComplete0: CauchyComplete A
x, y: Approximation A
e: Q+
E: forall d n : Q+, close (e + d) (x n) (y n)
d: Q+
e + d = e + 3 / 3 * d rewrite pos_recip_r,Qpos_mult_1_l;trivial.
-
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
Alim: Lim A
CauchyComplete0: CauchyComplete A
x, y: Approximation A
e: Q+
E: forall d n : Q+, close (e + d) (x n) (y n)
d: Q+
e + 3 / 3 * d = d / 3 + d / 3 + (e + d / 3) apply pos_eq;ring_tac.ring_with_nat.
Qed.

End cauchy.

Section lipschitz_lim.
Context {A:Type} {Aclose : Closeness A} `{!PreMetric A}
  `{Bclose : Closeness B} `{!PreMetric B} {Blim : Lim B}
   `{!CauchyComplete B}.

Global Instance lipschitz_lim_lipschitz (s : Approximation (A -> B)) L
  `{!forall e, Lipschitz (s e) L} : Lipschitz (lim s) L.
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
B: Type
Bclose: Closeness B
PreMetric1: PreMetric B
Blim: Lim B
CauchyComplete0: CauchyComplete B
s: Approximation (A -> B)
L: Q+
H: forall e : Q+, Lipschitz (s e) L
Lipschitz (lim s) L
Proof.
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
B: Type
Bclose: Closeness B
PreMetric1: PreMetric B
Blim: Lim B
CauchyComplete0: CauchyComplete B
s: Approximation (A -> B)
L: Q+
H: forall e : Q+, Lipschitz (s e) L
Lipschitz (lim s) L
intros e x y xi.
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
B: Type
Bclose: Closeness B
PreMetric1: PreMetric B
Blim: Lim B
CauchyComplete0: CauchyComplete B
s: Approximation (A -> B)
L: Q+
H: forall e : Q+, Lipschitz (s e) L
e: Q+
x, y: A
xi: close e x y
close (L * e) (lim s x) (lim s y)
apply rounded in xi;revert xi;apply (Trunc_ind _);intros [d [d' [E xi]]].
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
B: Type
Bclose: Closeness B
PreMetric1: PreMetric B
Blim: Lim B
CauchyComplete0: CauchyComplete B
s: Approximation (A -> B)
L: Q+
H: forall e : Q+, Lipschitz (s e) L
e: Q+
x, y: A
d, d': Q+
E: e = d + d'
xi: close d x y
close (L * e) (lim s x) (lim s y)
rewrite E,Qpos_plus_mult_distr_l.
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
B: Type
Bclose: Closeness B
PreMetric1: PreMetric B
Blim: Lim B
CauchyComplete0: CauchyComplete B
s: Approximation (A -> B)
L: Q+
H: forall e : Q+, Lipschitz (s e) L
e: Q+
x, y: A
d, d': Q+
E: e = d + d'
xi: close d x y
close (L * d + L * d') (lim s x) (lim s y)
apply lim_same_distance.
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
B: Type
Bclose: Closeness B
PreMetric1: PreMetric B
Blim: Lim B
CauchyComplete0: CauchyComplete B
s: Approximation (A -> B)
L: Q+
H: forall e : Q+, Lipschitz (s e) L
e: Q+
x, y: A
d, d': Q+
E: e = d + d'
xi: close d x y
forall d0 n : Q+,
close (L * d + d0)
  ({|
     approximate := fun e : Q+ => s e x;
     approx_equiv :=
       fun d e : Q+ =>
       close_arrow_apply (d + e) (s d) (s e)
         (approx_equiv (A -> B) s d e) x
   |} n)
  ({|
     approximate := fun e : Q+ => s e y;
     approx_equiv :=
       fun d e : Q+ =>
       close_arrow_apply (d + e) (s d) (s e)
         (approx_equiv (A -> B) s d e) y
   |} n)
clear e d' E.
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
B: Type
Bclose: Closeness B
PreMetric1: PreMetric B
Blim: Lim B
CauchyComplete0: CauchyComplete B
s: Approximation (A -> B)
L: Q+
H: forall e : Q+, Lipschitz (s e) L
x, y: A
d: Q+
xi: close d x y
forall d0 n : Q+,
close (L * d + d0)
  ({|
     approximate := fun e : Q+ => s e x;
     approx_equiv :=
       fun d e : Q+ =>
       close_arrow_apply (d + e) (s d) (s e)
         (approx_equiv (A -> B) s d e) x
   |} n)
  ({|
     approximate := fun e : Q+ => s e y;
     approx_equiv :=
       fun d e : Q+ =>
       close_arrow_apply (d + e) (s d) (s e)
         (approx_equiv (A -> B) s d e) y
   |} n)
intros d' n.
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
B: Type
Bclose: Closeness B
PreMetric1: PreMetric B
Blim: Lim B
CauchyComplete0: CauchyComplete B
s: Approximation (A -> B)
L: Q+
H: forall e : Q+, Lipschitz (s e) L
x, y: A
d: Q+
xi: close d x y
d', n: Q+
close (L * d + d')
  ({|
     approximate := fun e : Q+ => s e x;
     approx_equiv :=
       fun d e : Q+ =>
       close_arrow_apply (d + e) (s d) (s e)
         (approx_equiv (A -> B) s d e) x
   |} n)
  ({|
     approximate := fun e : Q+ => s e y;
     approx_equiv :=
       fun d e : Q+ =>
       close_arrow_apply (d + e) (s d) (s e)
         (approx_equiv (A -> B) s d e) y
   |} n) simpl.
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
B: Type
Bclose: Closeness B
PreMetric1: PreMetric B
Blim: Lim B
CauchyComplete0: CauchyComplete B
s: Approximation (A -> B)
L: Q+
H: forall e : Q+, Lipschitz (s e) L
x, y: A
d: Q+
xi: close d x y
d', n: Q+
close (L * d + d') (s n x) (s n y)
apply rounded_plus.
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
B: Type
Bclose: Closeness B
PreMetric1: PreMetric B
Blim: Lim B
CauchyComplete0: CauchyComplete B
s: Approximation (A -> B)
L: Q+
H: forall e : Q+, Lipschitz (s e) L
x, y: A
d: Q+
xi: close d x y
d', n: Q+
close (L * d) (s n x) (s n y)
apply (lipschitz (s n) L).
funext: Funext
univalence: Univalence
A: Type
Aclose: Closeness A
PreMetric0: PreMetric A
B: Type
Bclose: Closeness B
PreMetric1: PreMetric B
Blim: Lim B
CauchyComplete0: CauchyComplete B
s: Approximation (A -> B)
L: Q+
H: forall e : Q+, Lipschitz (s e) L
x, y: A
d: Q+
xi: close d x y
d', n: Q+
close d x y trivial.
Qed.

End lipschitz_lim.

End contents.

Arguments rounded_le {_ _ A _ _} e u v _ d _.
Arguments non_expanding {A _ B _} f {_ e x y} _.
Arguments lipschitz {A _ B _} f L {_ e x y} _.
Arguments uniform {A _ B _} f mu {_} _ _ _ _.
Arguments continuous {A _ B _} f {_} _ _.

Arguments map2_nonexpanding {A _ B _ C _ D _} f g {_ _} e x y xi.
Arguments map2_lipschitz {_ _ A _ B _ C _ D _} f g {_ _} Lf Lg {_ _} e x y xi.
Arguments map2_continuous {_ _ A _ B _ C _ D _} f g {_ _ _ _} u e.

Arguments Interval_close {_ _ _} _ _ _ _ _ /.

Arguments Lim A {_}.
Arguments lim {A _ _} _.

Arguments Approximation A {_}.
Arguments Build_Approximation {A _} _ _.
Arguments approximate {A _} _ _.
Arguments approx_equiv {A _} _ _ _.

Arguments CauchyComplete A {_ _}.

Arguments arrow_lim {A B _ _ _} _ / _.