```\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Order.Lattice
\import Order.PartialOrder
\import Paths
\import Paths.Meta
\import Set.Filter
\import Set.Subset
\import Topology.CoverSpace
\import Topology.CoverSpace.Complete
\import Topology.RatherBelow
\open Set
\open Bounded(top,top-univ,bottom,bottom-univ)
\open ClosurePrecoverSpace

\class UniformSpace \extends CompletelyRegularCoverSpace {
| isUniform : Set (Set E) -> \Prop
| uniform-cover {C : Set (Set E)} : isUniform C -> \Pi (x : E) -> ∃ (U : C) (U x)
| uniform-top : isUniform (single top)
| uniform-refine {C D : Set (Set E)} : isUniform C -> Refines C D -> isUniform D
| uniform-inter {C D : Set (Set E)} : isUniform C -> isUniform D -> isUniform (CoverInter C D)
| uniform-star {C : Set (Set E)} : isUniform C -> ∃ (D : isUniform) ∀ {V : D} ∃ (U : C) ∀ {W : D} (Given (V ∧ W) -> W ⊆ U)
| uniform-cauchy {C : Set (Set E)} : isCauchy C <-> Closure isUniform C

| cauchy-cover Cc x => closure-filter (pointFilter x) (\lam Cu => uniform-cover Cu x) \$ uniform-cauchy.1 Cc
| cauchy-top => uniform-cauchy.2 \$ closure-top idp
| cauchy-refine Cc e => uniform-cauchy.2 \$ closure-refine (uniform-cauchy.1 Cc) e
| cauchy-glue Cc e => uniform-cauchy.2 \$ closure-trans (uniform-cauchy.1 Cc) (\lam CU => uniform-cauchy.1 \$ e CU) idp
| isCompletelyRegular Cc => cauchy-subset (uniform-cauchy.2 \$ isCompletelyRegular {ClosureRegularCoverSpace isUniform uniform-cover uniform-star} (uniform-cauchy.1 Cc))
\lam {V} (inP (U,CU,V<=<U)) => inP \$ later (U, CU, unfolds \$ unfolds at V<=<U \$ TruncP.map V<=<U \lam (R',c,d,e) => (R', \lam r => uniform-cauchy.2 \$ c r, d, e))

\default isCauchy : Set (Set E) -> \Prop => Closure isUniform
\default uniform-cauchy \as uniform-cauchy-impl {C} : isCauchy C <-> Closure isUniform C => <->refl

\lemma makeCauchy {C : Set (Set E)} (Cu : isUniform C) : CoverSpace.isCauchy C
=> uniform-cauchy.2 (closure Cu)

\func IsProperUniform : \Prop
=> ∀ {C : isUniform} (isUniform \lam U => \Sigma (C U) (∃ U))

\func IsWeaklyProperUniform : \Prop
=> \Pi {C : Set (Set E)} -> isUniform (\lam U => (U = {Set E} bottom) || C U) -> isUniform C

\lemma proper_weaklyProper (p : IsProperUniform) : IsWeaklyProperUniform
=> \lam Cu => uniform-subset (p Cu) \case __ \with {
| (byLeft e, inP (x,Ux)) => \case rewrite e in Ux \with {
| inP ((),_)
}
| (byRight CU, _) => CU
}

\lemma inhabited_weaklyProper (p : TruncP E) : IsWeaklyProperUniform \elim p
| inP x => \lam Cu => uniform-refine Cu \case \elim __ \with {
| byLeft p => \case uniform-cover Cu x \with {
| inP (_, byLeft idp, inP ((),_))
| inP (V, byRight CV, Vx) => inP (V, CV, rewrite p bottom-univ)
}
| byRight CU => inP (_, CU, <=-refl)
}

\lemma uniform-inter-big (Cs : Array (Set (Set E))) (Cu : ∀ (C : Cs) (isUniform C)) : isUniform (CoverInterBig Cs) \elim Cs
| nil => uniform-top
| C :: Cs => uniform-inter (Cu 0) \$ uniform-inter-big _ (\lam j => Cu (suc j))

\lemma <=*-inter {V U : Set E} (p : V <=* U) : ∃ (V' : Set E) (V <=* V') (V' <=* U) \elim p
| inP (C,Cc,p) => \case uniform-star Cc \with {
| inP (D,Dc,g) => inP (star V D, inP (D, Dc, <=-refl), inP (D, Dc, (\case __ \with {
| inP (W, (DW, (y, (inP (V', (DV', (z, (Vz, V'z))), V'y), Wy))), Wx) => \case g DV' \with {
| inP (U',CU',h) => inP \$ later (U', (CU', (z, (Vz, h DV' (z,(V'z,V'z)) V'z))), h DW (y, (V'y, Wy)) Wx)
}
}) <=∘ p))
}

\lemma <=*-regular {C : Set (Set E)} (Cu : isUniform C) : isUniform \lam V => ∃ (U : C) (V <=* U)
=> \case uniform-star Cu \with {
| inP (D,Du,h) => uniform-subset Du \lam {V} DV => \case h DV \with {
| inP (U,CU,g) => inP \$ later (U, CU, inP (D, Du, \lam {y} (inP (W,(DW,s),Wy)) => g DW s Wy))
}
}

\lemma <=*-cauchy-regular {C : Set (Set E)} (Cc : CoverSpace.isCauchy C) : CoverSpace.isCauchy \lam V => ∃ (U : C) (V <=* U)
=> uniform-cauchy.2 \$ ClosureCoverSpace.closure-regular StarRatherBelow (\lam Cu => closure \$ <=*-regular Cu) (uniform-cauchy.1 Cc)

\lemma <=<-regular {C : Set (Set E)} (Cu : isUniform C) : isUniform \lam V => ∃ (U : C) (V <=< U)
=> uniform-subset (<=*-regular Cu) \lam {V} (inP (U,CU,p)) => inP \$ later (U, CU, <=*_<=< p)

\lemma uniform-separated {x y : E} : ∀ {C : CoverSpace.isCauchy} ∃ (U : C) (\Sigma (U x) (U y)) <-> ∀ {C : isUniform} ∃ (U : C) (\Sigma (U x) (U y))
=> (\lam sf Cu => sf \$ makeCauchy Cu, \lam sf Cc => closure-filter (\new SetFilter E {
| F U => \Sigma (U x) (U y)
| filter-mono p (Ux,Uy) => (p Ux, p Uy)
| filter-top => ((), ())
| filter-meet (Ux,Uy) (Vx,Vy) => ((Ux, Vx), (Uy, Vy))
}) sf \$ uniform-cauchy.1 Cc)
} \where {
\func star {X : \Set} (V : Set X) (C : Set (Set X)) : Set X
=> Union \lam W => \Sigma (C W) (Given (V ∧ W))

\lemma star-monotone {X : \Set} {V U : Set X} (p : V ⊆ U) {C D : Set (Set X)} (r : Refines C D) : star V C ⊆ star U D
=> \lam (inP (W',(CW',(y,(Vy,W'y))),W'x)) => \case r CW' \with {
| inP (W,DW,W'<=W) => inP (W, (DW, (y, (p Vy, W'<=W W'y))), W'<=W W'x)
}
}

\func \infix 4 <=* {X : UniformSpace} (V U : Set X) : \Prop
=> ∃ (C : isUniform) (UniformSpace.star V C ⊆ U)

\lemma <=*-char {X : UniformSpace} {V U : Set X} : V <=* U <-> isUniform \lam W => Given (V ∧ W) -> W ⊆ U
=> (\lam (inP (C,Cu,p)) => uniform-subset Cu \$ later \lam {W} CW s Wx => p \$ inP (W,(CW,s),Wx),
\lam Cu => inP (_, Cu, \lam (inP (W,(g,s),Wx)) => g s Wx))

\lemma <=*_<=< {X : UniformSpace} {V U : Set X} (p : V <=* U) : V <=< U
=> X.makeCauchy (<=*-char.1 p)

\instance StarRatherBelow {X : UniformSpace} : RatherBelow (<=* {X})
| <=<-left (inP (C,Cu,p)) q => inP (C, Cu, p <=∘ q)
| <=<-right p (inP (C,Cu,q)) => inP (C, Cu, UniformSpace.star-monotone p Refines-refl <=∘ q)
| <=<_top => inP (single top, uniform-top, top-univ)
| <=<_meet (inP (C,Cu,p)) (inP (D,Du,q)) => inP (_, uniform-inter Cu Du, meet-univ (UniformSpace.star-monotone meet-left Refines-inter-left <=∘ p) (UniformSpace.star-monotone meet-right Refines-inter-right <=∘ q))

\lemma uniform-subset {X : UniformSpace} {C D : Set (Set X)} (Cc : isUniform C) (e : \Pi {U : Set X} -> C U -> D U) : isUniform D
=> uniform-refine Cc \lam {U} CU => inP (U, e CU, <=-refl)

\lemma top-uniform {X : UniformSpace} {C : Set (Set X)} (Ct : C top) : isUniform C
=> uniform-subset uniform-top \$ later \lam p => rewriteI p Ct

\lemma uniform-embedding-char {X : UniformSpace} {Y : PrecoverSpace} {f : PrecoverMap X Y}
: f.IsEmbedding <-> ∀ {C : isUniform} (isCauchy \lam V => ∃ (U : C) (f ^-1 V ⊆ U))
=> (\lam e Cu => e \$ X.makeCauchy Cu, closure-embedding (uniform-cauchy.1 __) f)

\record LocallyUniformMap \extends CoverMap {
\override Dom : UniformSpace
\override Cod : UniformSpace

| func-locally-uniform {E : Set (Set Cod)} : isUniform E -> ∃ (C : isUniform) ∀ {U : C} (isUniform \lam V => ∃ (W : E) (U ∧ V ⊆ func ^-1 W))
| func-cover {E'} E'c => closure-univ-cover (\lam {E} Eu => uniform-cauchy.2 \case func-locally-uniform Eu \with {
| inP (C,Cu,e) => closure-refine (closure-trans (closure Cu) (\lam CU => closure (e CU)) idp) \lam {Z} (inP (U, V, CU, inP (W, EW, q), p)) => inP \$ later (_, inP (W, EW, idp), rewrite p q)
}) (uniform-cauchy.1 E'c)
}

\record UniformMap \extends LocallyUniformMap {
| func-uniform {E : Set (Set Cod)} : isUniform E -> isUniform \lam U => ∃ (V : E) (U = func ^-1 V)
| func-locally-uniform Eu => inP (_, func-uniform Eu, \lam (inP (V,EV,p)) => uniform-subset (func-uniform Eu) \lam _ => inP \$ later (V, EV, rewrite p meet-left))

\func IsEmbedding : \Prop
=> \Pi {C : Set (Set Dom)} -> isUniform C -> isUniform \lam V => ∃ (U : C) (func ^-1 V ⊆ U)

\lemma embedding->coverEmbedding (e : IsEmbedding) : CoverMap.IsEmbedding
=> closure-embedding {_} {isUniform} (uniform-cauchy.1 __) \this \lam Cu => uniform-cauchy.2 (closure (e Cu))

\func IsDenseEmbedding : \Prop
=> \Sigma IsDense IsEmbedding
} \where {
\func compose \alias \infixl 8 ∘ {X Y Z : UniformSpace} (g : UniformMap Y Z) (f : UniformMap X Y) : UniformMap X Z \cowith
| func x => g (f x)
| func-uniform Du => uniform-subset (f.func-uniform \$ g.func-uniform Du) \lam (inP (V, inP (W,DW,q), p)) => inP \$ later (W, DW, p *> rewrite q idp)
}

\func UniformTransfer {X : \Set} {Y : UniformSpace} (f : X -> Y) : UniformSpace X \cowith
| CoverSpace => CoverTransfer f
| isUniform C => isUniform \lam V => ∃ (U : C) (f ^-1 V ⊆ U)
| uniform-cover Ec x => \case uniform-cover Ec (f x) \with {
| inP (U, inP (V,CV,p), Ufx) => inP (V, CV, p Ufx)
}
| uniform-top => top-uniform \$ inP \$ later (top, idp, top-univ)
| uniform-refine Ec r => uniform-subset Ec \lam (inP (V,CV,p)) => \case r CV \with {
| inP (W,DW,V<=W) => inP \$ later (W, DW, p <=∘ V<=W)
}
| uniform-inter Cu Du => uniform-subset (uniform-inter Cu Du) \lam {_} (inP (U', inP (U,CU,Up), V', inP (V,DV,Vp), idp)) => inP \$ later (U ∧ V, inP (U, CU, V, DV, idp), MeetSemilattice.meet-monotone Up Vp)
| uniform-star Cu => \case uniform-star Cu \with {
| inP (D',D'u,h) => inP (\lam V => ∃ (V' : D') (V = f ^-1 V'), uniform-subset D'u \lam {V'} D'V' => \case h D'V' \with {
| inP (V, inP (U,CU,p), g) => inP \$ later (_, inP (V', D'V', idp), <=-refl)
}, \lam {_} (inP (V',D'V',idp)) => \case h D'V' \with {
| inP (V, inP (U,CU,p), g) => inP (U, CU, \lam {_} (inP (W',D'W',idp)) (x,s) {y} W'fy => p \$ g D'W' (f x, s) W'fy)
})
}
| uniform-cauchy => (\lam Cc => closure-refine (closure-univ-closure f (\lam Cu => closure \$ uniform-subset Cu \lam {U} CU => inP \$ later (_, inP (U, CU, idp), <=-refl)) (uniform-cauchy.1 Cc)) \lam {_} (inP (V, inP (U,CU,p), idp)) => inP (U, CU, p),
closure-cauchy {X} {CoverTransfer f} \lam Cu => Y.makeCauchy Cu)

\type \infix 4 s<=* {X : UniformSpace} (V U : Set X) : \Prop
=> isUniform \lam W => (W = Compl V) || (W = U)

\instance StronglyStarRatherBelow {X : UniformSpace} : RatherBelow (s<=* {X})
| <=<_top => unfolds \$ top-uniform \$ byRight idp
| <=<-left p q => uniform-refine (unfolds in p) \lam {U'} => later \case __ \with {
| byLeft r => rewrite r \$ inP (_, byLeft idp, <=-refl)
| byRight r => rewrite r \$ inP (_, byRight idp, q)
}
| <=<-right p q => uniform-refine (unfolds in q) \lam {U'} => later \case __ \with {
| byLeft r => inP (_, byLeft idp, rewrite r \lam nVx Wx => nVx (p Wx))
| byRight r => inP (U', byRight r, <=-refl)
}
| <=<_meet U<=<U' V<=<V' => uniform-refine (uniform-inter (unfolds in U<=<U') V<=<V') \$ later \lam (inP (U'', t1, V'', t2, p)) => rewrite p \case \elim t1, \elim t2 \with {
| byLeft r, _ => inP (_, byLeft idp, rewrite r \lam (nUx,_) (Ux,_) => nUx Ux)
| _, byLeft r => inP (_, byLeft idp, rewrite r \lam (_,nVx) (_,Vx) => nVx Vx)
| byRight q, byRight r => inP (_, byRight \$ pmap2 (∧) q r, <=-refl)
}

\class StronglyRegularUniformSpace \extends UniformSpace, StronglyRegularCoverSpace {
| isStronglyRegularUniform {C : Set (Set E)} : isUniform C -> isUniform \lam V => ∃ (U : C) (V s<=* U)
| isStronglyRegular Cc => uniform-cauchy.2 \$ ClosureCoverSpace.closure-regular StronglyRatherBelow (\lam Cu => closure \$ uniform-subset (isStronglyRegularUniform Cu) \lam {V} (inP (U,CU,p)) => inP \$ later (U, CU, uniform-cauchy.2 \$ closure p)) (uniform-cauchy.1 Cc)

\lemma s<=*-cauchy-regular {C : Set (Set E)} (Cc : CoverSpace.isCauchy C) : CoverSpace.isCauchy \lam V => ∃ (U : C) (V s<=* U)
=> uniform-cauchy.2 \$ ClosureCoverSpace.closure-regular StronglyStarRatherBelow (\lam Cu => closure \$ isStronglyRegularUniform Cu) (uniform-cauchy.1 Cc)
}

\func StronglyRegularUniformTransfer {X : \Set} {Y : StronglyRegularUniformSpace} (f : X -> Y) : StronglyRegularUniformSpace X \cowith
| UniformSpace => UniformTransfer f
| isStronglyRegularUniform Cu => uniform-subset (isStronglyRegularUniform Cu) \lam {V} (inP (U, inP (W,CW,p), V<=<U)) => inP \$ later
(_, inP (W, CW, <=<-left (uniform-subset (unfolds in V<=<U) \lam {W} e => inP \$ later (_, ||.map (pmap (f ^-1)) (pmap (f ^-1)) e, <=-refl)) p), <=-refl)```