\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 ClosurePrecoverSpace

\class PreuniformSpace \extends PrecoverSpace {
  | 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-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. Cc
  | cauchy-top => uniform-cauchy. $ closure-top idp
  | cauchy-refine Cc e => uniform-cauchy. $ closure-refine (uniform-cauchy. Cc) e
  | cauchy-glue Cc e => uniform-cauchy. $ closure-trans (uniform-cauchy. Cc) (\lam CU => uniform-cauchy. $ e CU) idp

  \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. (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)) => bottom-empty (rewrite e in Ux)
      | (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 ) $ uniform-inter-big _ (\lam j => Cu (suc j))

  \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 (Ux,Uy) p => (p Ux, p Uy)
      | filter-top => ((), ())
      | filter-meet (Ux,Uy) (Vx,Vy) => ((Ux, Vx), (Uy, Vy))
    }) sf $ uniform-cauchy. 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  <=* {X : PreuniformSpace} (V U : Set X) : \Prop
  => ∃ (C : isUniform) (PreuniformSpace.star V C ⊆ U)

\lemma <=*-char {X : PreuniformSpace} {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))

\class RegularPreuniformSpace \extends PreuniformSpace, CoverSpace {
  | uniform-regular {C : Set (Set E)} : isUniform C -> isCauchy \lam V => ∃ (U : C) (V <=* U)
  | isRegular Cc => uniform-cauchy. $ ClosureCoverSpace.closure-regular RegularRatherBelow (\lam Cu => uniform-cauchy. $ cauchy-subset (uniform-regular Cu) \lam {V} (inP (U,CU,V<=*U)) => inP $ later (U, CU, <=*_<=< V<=*U)) (uniform-cauchy. Cc)

  \lemma <=*-cauchy-regular {C : Set (Set E)} (Cc : isCauchy C) : isCauchy \lam V => ∃ (U : C) (V <=* U)
    => uniform-cauchy. $ ClosureCoverSpace.closure-regular StarRatherBelow (\lam Cu => uniform-cauchy. $ uniform-regular Cu) (uniform-cauchy. Cc)
} \where {
  \func fromCoverSpace (X : CoverSpace) : RegularPreuniformSpace X \cowith
    | isUniform => isCauchy
    | uniform-cover => cauchy-cover
    | uniform-top => cauchy-top
    | uniform-refine => cauchy-refine
    | uniform-inter Cc Dc => cauchy-subset (cauchy-inter Cc Dc) \lam {_} (inP (V,W,CV,DW,p)) => inP $ later (V,CV,W,DW,p)
    | isCauchy => isCauchy
    | uniform-cauchy => (closure, ClosurePrecoverSpace.closure-cauchy (\lam c => c))
    | uniform-regular Cc => cauchy-subset (isRegular Cc) \lam {V} (inP (U,CU,V<=<U)) =>
        inP $ later (U, CU, inP (_, V<=<U, \lam (inP (W, (h,t), Wx)) => h t Wx))
}

\class UniformSpace \extends RegularPreuniformSpace, CompletelyRegularCoverSpace {
  | uniform-star {C : Set (Set E)} : isUniform C -> ∃ (D : isUniform) ∀ {V : D} ∃ (U : C) ∀ {W : D} (Given (V ∧ W) -> W ⊆ U)
  | uniform-regular Cu => \case uniform-star Cu \with {
    | inP (D,Du,h) => uniform-cauchy. $ closure $ 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))
    }
  }
  | isCompletelyRegular Cc => cauchy-subset (uniform-cauchy. $ isCompletelyRegular {ClosureRegularCoverSpace isUniform uniform-cover uniform-star} (uniform-cauchy. 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. $ c r, d, e))

  \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 (PreuniformSpace.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 <=<-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 <=*_<=< {X : PreuniformSpace} {V U : Set X} (p : V <=* U) : V <=< U
  => X.makeCauchy (<=*-char. p)

\instance StarRatherBelow {X : PreuniformSpace} : RatherBelow (<=* {X})
  | <=<-left (inP (C,Cu,p)) q => inP (C, Cu, p <=∘ q)
  | <=<-right p (inP (C,Cu,q)) => inP (C, Cu, PreuniformSpace.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 (PreuniformSpace.star-monotone meet-left Refines-inter-left <=∘ p) (PreuniformSpace.star-monotone meet-right Refines-inter-right <=∘ q))

\lemma uniform-subset {X : PreuniformSpace} {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 : PreuniformSpace} {C : Set (Set X)} (Ct : C top) : isUniform C
  => uniform-subset uniform-top $ later \lam p => rewriteI p Ct

\lemma uniform-embedding-char {X : PreuniformSpace} {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. __) f)

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

  | 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. \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. 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 IsUniformEmbedding : \Prop
    => \Pi {C : Set (Set Dom)} -> isUniform C -> isUniform \lam V => ∃ (U : C) (func ^-1 V ⊆ U)

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

  \func IsDenseUniformEmbedding : \Prop
    => \Sigma IsDense IsUniformEmbedding

  \func IsWeaklyDenseUniformEmbedding : \Prop
    => \Sigma IsWeaklyDense IsUniformEmbedding
} \where {
  \func id {X : RegularPreuniformSpace} : UniformMap X X \cowith
    | func x => x
    | func-uniform Eu => uniform-subset Eu \lam {U} EU => inP $ later (U, EU, idp)

  \func compose \alias \infixl  ∘ {X Y Z : RegularPreuniformSpace} (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 const {X Y : RegularPreuniformSpace} (y : Y) : UniformMap X Y \cowith
    | func _ => y
    | func-uniform Eu => top-uniform \case uniform-cover Eu y \with {
      | inP (U,EU,Uy) => inP $ later (U, EU, <=-antisymmetric (\lam _ => Uy) top-univ)
    }

  \lemma lift {X Y Z : RegularPreuniformSpace} {f : X -> Y} (g : UniformMap Y Z) (ge : g.IsUniformEmbedding) (fg : UniformMap X Z (\lam x => g (f x))) : UniformMap X Y f \cowith
    | func-uniform Eu => uniform-refine (fg.func-uniform (ge Eu)) \lam {_} (inP (V, inP (U,EU,p), idp)) => inP (_, inP (U, EU, idp), ^-1_<= f p)
}

\func RegularPreuniformTransfer {X : \Set} {Y : RegularPreuniformSpace} (f : X -> Y) : RegularPreuniformSpace 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-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. Cc)) \lam {_} (inP (V, inP (U,CU,p), idp)) => inP (U, CU, p),
                       closure-cauchy {X} {CoverTransfer f} \lam Cu => Y.makeCauchy Cu)
  | uniform-regular Cu => cauchy-subset (uniform-regular Cu) $ later \lam {V} (inP (U, inP (W,CW,p), inP (D,Du,q))) => inP (_, inP (W, CW,
      inP (\lam W => ∃ (W' : D) (W = f ^-1 W'),
           uniform-subset Du \lam {V} DV => inP $ later (_, inP (V, DV, idp), <=-refl),
           \lam {y} (inP (W',(inP (V',DV',r), (x,(Vfx,W'x))),W'y)) => p $ q $ inP (V', (DV', (f x, (Vfx, rewrite r in W'x))), rewrite r in W'y)
          )), <=-refl)

\func UniformTransfer {X : \Set} {Y : UniformSpace} (f : X -> Y) : UniformSpace X \cowith
  | RegularPreuniformSpace => RegularPreuniformTransfer f
  | 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)
    })
  }

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

\lemma s<=*_s<=< {X : PreuniformSpace} {V U : Set X} (p : V s<=* U) : V s<=< U
  => X.makeCauchy p

\lemma s<=*_<=* {X : PreuniformSpace} {V U : Set X} (p : V s<=* U) : V <=* U
  => <=*-char. $ uniform-subset (unfolds in p) \lam {W} e s => \case \elim e \with {
    | byLeft q => absurd $ later $ (rewrite q in s..) s..
    | byRight q => =_<= q
  }

\instance StronglyStarRatherBelow {X : PreuniformSpace} : 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 StronglyRegularPreuniformSpace \extends RegularPreuniformSpace, StronglyRegularCoverSpace {
  | uniform-strongly-regular {C : Set (Set E)} : isUniform C -> isCauchy \lam V => ∃ (U : C) (V s<=* U)
  | uniform-regular Cu => cauchy-subset (uniform-strongly-regular Cu) \lam {V} (inP (U,CU,p)) => inP $ later (U, CU, s<=*_<=* p)
  | isStronglyRegular Cc => uniform-cauchy. $ ClosureCoverSpace.closure-regular StronglyRatherBelow (\lam Cu => uniform-cauchy. $ cauchy-subset (uniform-strongly-regular Cu) \lam {V} (inP (U,CU,p)) => inP $ later (U, CU, uniform-cauchy. $ closure p)) (uniform-cauchy. Cc)

  \lemma s<=*-cauchy-regular {C : Set (Set E)} (Cc : CoverSpace.isCauchy C) : CoverSpace.isCauchy \lam V => ∃ (U : C) (V s<=* U)
    => uniform-cauchy. $ ClosureCoverSpace.closure-regular StronglyStarRatherBelow (\lam Cu => uniform-cauchy. $ uniform-strongly-regular Cu) (uniform-cauchy. Cc)
} \where {
    \func fromCoverSpace (X : StronglyRegularCoverSpace) : StronglyRegularPreuniformSpace X \cowith
      | isUniform => isCauchy
      | uniform-cover => cauchy-cover
      | uniform-top => cauchy-top
      | uniform-refine => cauchy-refine
      | uniform-inter Cc Dc => cauchy-subset (cauchy-inter Cc Dc) \lam {_} (inP (V,W,CV,DW,p)) => inP $ later (V,CV,W,DW,p)
      | isCauchy => isCauchy
      | uniform-cauchy => (closure, ClosurePrecoverSpace.closure-cauchy (\lam c => c))
      | uniform-strongly-regular Cc => cauchy-subset (isStronglyRegular Cc) \lam {V} (inP (U,CU,V<=<U)) => inP $ later (U,CU,V<=<U)
}

\class StronglyRegularUniformSpace \extends UniformSpace, StronglyRegularPreuniformSpace {
  | uniform-strongly-star {C : Set (Set E)} : isUniform C -> ∃ (D : isUniform) ∀ {V : D} ∃ (U : C) ∀ {W : D} (Not (Given (V ∧ W)) || W ⊆ U)
  | uniform-star Cu => \case uniform-strongly-star Cu \with {
    | inP (D,Du,h) => inP (D, Du, \lam DV => \case h DV \with {
      | inP (U,CU,g) => inP (U, CU, \lam DW s {y} Wy => \case g DW \with {
        | byLeft e => absurd (e s)
        | byRight e => e Wy
      })
    })
  }
  | uniform-strongly-regular Cu => \case uniform-strongly-star Cu \with {
    | inP (D,Du,h) => uniform-cauchy. $ closure $ uniform-subset Du \lam {V} DV => \case h DV \with {
      | inP (U,CU,g) => inP $ later (U, CU, uniform-refine Du \lam {W} DW => later \case g DW \with {
        | byLeft p => inP (_, byLeft idp, \lam {x} Wx Vx => p (x,(Vx,Wx)))
        | byRight p => inP (U, byRight idp, p)
      })
    }
  }

  \lemma s<=*-regular {C : Set (Set E)} (Cu : isUniform C) : isUniform \lam V => ∃ (U : C) (V s<=* U)
    => \case uniform-strongly-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, uniform-refine Du \lam {W} DW => \case g DW \with {
          | byLeft e => inP (_, byLeft idp, \lam {x} Wx Vx => e (x,(Vx,Wx)))
          | byRight e => inP (_, byRight idp, e)
        })
      }
    }

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

\func StronglyRegularUniformTransfer {X : \Set} {Y : StronglyRegularUniformSpace} (f : X -> Y) : StronglyRegularUniformSpace X \cowith
  | PreuniformSpace => UniformTransfer f
  | uniform-strongly-star Cu => \case uniform-strongly-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)) => \case g D'W' \with {
        | byLeft e => byLeft \lam s => e (f s., s.)
        | byRight e => byRight $ ^-1_<= f e <=∘ p
      })
    })
  }