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). Proof. hnf. intros e x y xi;exact (non_expanding g (non_expanding f xi)). Qed.
Require Import Import NatPair.Instances. Import Quoting.Instances.