\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Order.Lattice
\import Order.PartialOrder
\import Paths
\import Paths.Meta
\import Set.Subset
\import Topology.RatherBelow
\import Topology.TopSpace

\class PrecoverSpace \extends TopSpace {
  | isCauchy : Set (Set E) -> \Prop
  | cauchy-top : isCauchy (single top)
  | cauchy-refine {C D : Set (Set E)} : isCauchy C -> Refines C D -> isCauchy D
  | cauchy-glue {C : Set (Set E)} : isCauchy C -> \Pi {D : Set E -> Set (Set E)} -> (\Pi {U : Set E} -> C U -> isCauchy (D U))
    -> isCauchy (\lam U => ∃ (V W : Set E) (C V) (D V W) (U = V ∧ W))
  | cauchy-open {S : Set E} : isOpen S <-> ∀ {x : S} (isCauchy \lam U => U x -> U ⊆ S)

  \default open-top => cauchy-open. \lam _ => cauchy-refine cauchy-top \lam {U} _ => inP (U, \lam _ _ => (), <=-refl)
  \default open-inter Uo Vo => cauchy-open. $ later \lam {x} (Ux,Vx) => cauchy-refine (cauchy-glue (cauchy-open. Uo Ux) (\lam _ => cauchy-open. Vo Vx))
    \lam (inP (U',V',Uc,Vc,W=U'V')) => inP (U' ∧ V', \lam (U'x,V'x) {y} (U'y,V'y) => (Uc U'x U'y, Vc V'x V'y), =_<= W=U'V')
  \default open-Union So => cauchy-open. $ later \lam {x} (inP (U,SU,Ux)) => cauchy-refine (cauchy-open. (So SU) Ux) \lam {V} Vc => inP (V, \lam Vx => Vc Vx <=∘ Set.Union-cond SU, <=-refl)

  \default isOpen S : \Prop => ∀ {x : S} (isCauchy \lam U => U x -> U ⊆ S)
  \default cauchy-open \as cauchy-open-impl {S} : isOpen S <-> _ => <->refl

  \lemma cauchy-trans-dep {C : Set (Set E)} {D : \Pi {U : Set E} -> C U -> Set (Set E)} (Cc : isCauchy C) (Dc : \Pi {U : Set E} (c : C U) -> isCauchy (D c))
    : isCauchy (\lam U => ∃ (V W : Set E) (c : C V) (D c W) (U = V ∧ W))
    => transport isCauchy (ext \lam U => ext (\lam (inP (V,W,CV,DW,p)) => inP (V, W, CV, transport (D __ W) prop-pi DW., p), \lam (inP (V,W,c,DW,p)) => inP (V, W, c, (c,DW), p))) $ cauchy-glue Cc {\lam U V => \Sigma (c : C U) (D c V)} \lam CU => transport isCauchy (ext \lam V => ext (\lam d => (CU,d), \lam s => transport (D __ V) prop-pi s.)) (Dc CU)

  \func HasWeaklyDensePoints => \Pi {C : Set (Set E)} -> isCauchy (\lam U => (U = {Set E} bottom) || C U) -> isCauchy C

  \func HasDensePoints => \Pi {C : Set (Set E)} -> isCauchy C -> isCauchy \lam U => \Sigma (C U) (∃ U)

  \lemma cauchy-subset {C D : Set (Set E)} (Cc : isCauchy C) (e : \Pi {U : Set E} -> C U -> D U) : isCauchy D
    => cauchy-refine Cc \lam {U} CU => inP (U, e CU, <=-refl)

  \lemma hasDensePoints_hasWeaklyDensePoints (d : HasDensePoints) : HasWeaklyDensePoints
    => \lam Cc => cauchy-subset (d Cc) \case __ \with {
      | (byLeft e, inP (x,Ux)) => bottom-empty (rewrite e in Ux)
      | (byRight CU, _) => CU
    }

  \lemma top-cauchy {C : Set (Set E)} (Ct : C top) : isCauchy C
    => cauchy-subset cauchy-top $ later \lam p => rewriteI p Ct

  \lemma cauchy-inter {C D : Set (Set E)} (Cc : isCauchy C) (Dc : isCauchy D)
    : isCauchy (\lam U => ∃ (V W : Set E) (C V) (D W) (U = V ∧ W))
    => cauchy-glue Cc \lam _ => Dc
} \where {
  \lemma PrecoverSpace-ext {X : \Set} {S T : PrecoverSpace X} (p : \Pi {C : Set (Set X)} -> S.isCauchy C <-> T.isCauchy C) : S = T
    => exts (\lam U => <->_=. S.cauchy-open *> ext (\lam f Ux => p. (f Ux), \lam f Ux => p. (f Ux)) *> inv (<->_=. T.cauchy-open), \lam C => ext p)
}

\type \infix  <=< {X : PrecoverSpace} (V U : Set X) : \Prop
  => isCauchy \lam W => Given (V ∧ W) -> W ⊆ U

\class CoverSpace \extends PrecoverSpace {
  | isRegular {C : Set (Set E)} : isCauchy C -> isCauchy \lam V => ∃ (U : C) (V <=< U)
} \where {
  \lemma CoverSpace-ext {X : \Set} {S T : CoverSpace X} (p : \Pi {C : Set (Set X)} -> S.isCauchy C <-> T.isCauchy C) : S = T
    => exts (\lam U => <->_=. S.cauchy-open *> ext (\lam f Ux => p. (f Ux), \lam f Ux => p. (f Ux)) *> inv (<->_=. T.cauchy-open), \lam C => ext p)
}

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

\lemma s<=<_<=< {X : PrecoverSpace} {V U : Set X} (p : V s<=< U) : V <=< U
  => X.cauchy-subset p $ later \case __ \with {
    | byLeft q => rewrite q \lam (x,(Vx,nVx)) => absurd (nVx Vx)
    | byRight q => \lam _ => rewrite q <=-refl
  }

\class StronglyRegularCoverSpace \extends CoverSpace {
  | isStronglyRegular {C : Set (Set E)} : isCauchy C -> isCauchy \lam V => ∃ (U : C) (V s<=< U)
  | isRegular Cc => cauchy-subset (isStronglyRegular Cc) \lam (inP (V,CV,Us<=<V)) => inP $ later (V, CV, s<=<_<=< Us<=<V)

  \lemma isStronglyRegularSubset {C : Set (Set E)} (Cc : isCauchy C) : isCauchy \lam V => ∃ (U : C) (V ⊆ U) (V s<=< U)
    => cauchy-subset (cauchy-inter Cc $ isStronglyRegular Cc) \lam {_} (inP (U, V, CU, inP (U',CU',V<=<U'), idp)) => inP $ later (U', CU', {?}, {?})
}

\instance StronglyRatherBelow {X : PrecoverSpace} : RatherBelow {SetLattice X} (s<=<)
  | <=<_top => X.top-cauchy $ byRight idp
  | <=<-left p q => cauchy-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 => cauchy-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' => cauchy-refine (X.cauchy-inter U<=<U' V<=<V') $ later \lam (inP (U'', V'', t1, 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)
  }

\record PrecoverMap \extends ContMap {
  \override Dom : PrecoverSpace
  \override Cod : PrecoverSpace
  | func-cover {D : Set (Set Cod)} : isCauchy D -> isCauchy \lam U => ∃ (V : D) (U = func ^-1 V)

  \default func-cont Uo => cauchy-open. $ later \lam {x} Ufx => cauchy-refine (func-cover (cauchy-open. Uo Ufx)) \lam (inP (W,c,d)) => inP (func ^-1 W, \lam a {_} => c a, =_<= d)
} \where {
  \func id {X : PrecoverSpace} : PrecoverMap X X \cowith
    | func x => x
    | func-cover Dc => X.cauchy-subset Dc \lam {U} DU => inP $ later (U, DU, idp)

  \func compose \alias \infixl  ∘ {X Y Z : PrecoverSpace} (g : PrecoverMap Y Z) (f : PrecoverMap X Y) : PrecoverMap X Z \cowith
    | func x => g (f x)
    | func-cover Dc => X.cauchy-subset (f.func-cover $ g.func-cover Dc) \lam (inP (V, inP (W,DW,q), p)) => inP $ later (W, DW, p *> rewrite q idp)
}