\import Function.Meta ($)
\import Logic
\import Logic.Meta
\import Meta
\import Order.Directed
\import Order.Lattice
\import Order.PartialOrder
\import Paths
\import Paths.Meta
\import Set
\import Set.Category
\import Set.Filter
\import Set.Subset
\open Bounded(top)

\class TopSpace \extends BaseSet {
  | isOpen : Set E -> \Prop
  | open-top : isOpen Bounded.top
  | open-inter {U V : Set E} : isOpen U -> isOpen V -> isOpen (U ∧ V)
  | open-Union {S : Set (Set E)} : ∀ {U : S} (isOpen U) -> isOpen (Set.Union S)

  \lemma cover-open {U : Set E} (c : ∀ {x : U} ∃ (V : isOpen) (V x) (V ⊆ U)) : isOpen U
    => \have uo => open-Union {_} {\lam V => \Sigma (isOpen V) (V ⊆ U)} __.
       \in transport isOpen (ext \lam x => ext (\lam (inP (V,(_,V<=U),Vx)) => V<=U Vx, \lam Ux => TruncP.map (c Ux) \lam (V,Vo,Vx,V<=U) => (V, (Vo, V<=U), Vx))) uo

  \lemma open-IUnion {J : \hType} (g : J -> Given isOpen) : isOpen \lam x => ∃ (j : J) ((g j). x)
    => \have uo => open-Union {_} {\lam U => ∃ (j : J) ((g j). = U)} \lam (inP (j,p)) => transport isOpen p (g j).
       \in transport isOpen (ext \lam x => ext (\lam (inP (U, inP (j,p), Ux)) => inP (j, rewrite p Ux), \lam (inP (j,c)) => inP ((g j)., inP (j, idp), c))) uo

  \type \infix  <=<T (V U : Set E) : \Prop
    => \Pi (y : E) -> ∃ (W : isOpen) (W y) (Given (V ∧ W) -> W ⊆ U)

  \func IsRegular => ∀ {U : isOpen} {x : U} ∃ (V : isOpen) (V x) (V <=<T U)

  \func IsLimit {I : DirectedSet} (f : I -> E) (l : E) : \Prop
    => ∀ {U : isOpen} (U l) ∃ (N : I) ∀ {n} (N <= n -> U (f n))

  \func IsClosed (U : Set E) : \Prop
    => \Pi {x : E} -> (\Pi {V : Set E} -> isOpen V -> V x -> ∃ (U ∧ V)) -> U x
}

\func NFilter {X : TopSpace} (x : X) : ProperFilter X \cowith
  | F U => ∃ (V : isOpen) (V x) (V ⊆ U)
  | filter-mono p (inP (W,Wo,Wx,q)) => inP (W, Wo, Wx, q <=∘ p)
  | filter-top => inP (top, open-top, (), <=-refl)
  | filter-meet (inP (U,Uo,Ux,p)) (inP (V,Vo,Vx,q)) => inP (U ∧ V, open-inter Uo Vo, (Ux,Vx), MeetSemilattice.meet-monotone p q)
  | isProper (inP (V,Vo,Vx,p)) => inP (x, p Vx)

\func IsDenseSet {X : TopSpace} (S : Set X) : \Prop
  => \Pi {x : X} {U : Set X} -> isOpen U -> U x -> ∃ (y : S) (U y)

\record ContMap \extends SetHom {
  \override Dom : TopSpace
  \override Cod : TopSpace

  | func-cont {U : Cod -> \Prop} : isOpen U -> isOpen \lam x => U (func x)

  \func IsDense : \Prop
    => IsDenseSet (\lam y => ∃ (x : Dom) (func x = y))

  \func IsEmbedding : \Prop
    => ∀ {U : isOpen} ∃ (V : isOpen) (U = func ^-1 V)

  \lemma embedding-char : IsEmbedding <-> ∀ {U : isOpen} {x : U} ∃ (V : isOpen) (V (func x)) (func ^-1 V ⊆ U)
    => (\lam e Uo Ux => \case e Uo \with {
      | inP (V,Vo,p) => inP (V, Vo, rewrite p in Ux, rewrite p <=-refl)
    }, \lam e {U} Uo => inP (_, open-Union {_} {\lam V => \Sigma (isOpen V) (func ^-1 V ⊆ U)} __., ext \lam x => ext (\lam Ux => \case e Uo Ux \with {
      | inP (V,Vo,Vfx,p) => inP (V, (Vo, p), Vfx)
    }, \lam (inP (V,(Vo,p),Vfx)) => p Vfx)))

  \func IsDenseEmbedding : \Prop
    => \Sigma IsDense IsEmbedding
} \where {
  \func id {X : TopSpace} : ContMap X X \cowith
    | func x => x
    | func-cont Uo => Uo

  \func compose \alias \infixl  ∘ {X Y Z : TopSpace} (g : ContMap Y Z) (f : ContMap X Y) : ContMap X Z \cowith
    | func x => g (f x)
    | func-cont Uo => f.func-cont (g.func-cont Uo)

  \func const {Y X : TopSpace} (x : X) : ContMap Y X \cowith
    | func _ => x
    | func-cont _ => Y.cover-open \lam Ux => inP (top, open-top, (), \lam _ => Ux)
}

\lemma const-limit {I : DirectedSet} {X : TopSpace} {x : X} : X.IsLimit (\lam (_ : I) => x) x
  => \lam _ Ux => \case I.isInhabitted \with {
    | inP N => inP (N, \lam _ => Ux)
  }

\lemma cont-limit {I : DirectedSet} {X Y : TopSpace} {f : I -> X} {l : X} (p : X.IsLimit f l) (g : ContMap X Y) : Y.IsLimit (\lam n => g (f n)) (g l)
  => \lam Uo Ugl => p (g.func-cont Uo) Ugl

\class HausdorffTopSpace \extends TopSpace
  | isHausdorff {x y : E} : ∀ {U V : isOpen} (U x) (V y) ∃ (U ∧ V) -> x = y

\lemma denseSet-lift-unique {X : TopSpace} {Y : HausdorffTopSpace} {S : Set X} (Sd : IsDenseSet S) (f g : ContMap X Y) (p : \Pi {x : X} -> S x -> f x = g x) (x : X) : f x = g x
  => isHausdorff \lam {U} Uo Vo Ufx Vgx => \case Sd {x} (open-inter (f.func-cont Uo) (g.func-cont Vo)) (Ufx,Vgx) \with {
    | inP (y,Sy,(Ufy,Vgy)) => inP (g y, (transport U (p Sy) Ufy, Vgy))
  }

\lemma dense-lift-unique {X Y : TopSpace} {Z : HausdorffTopSpace} (f : ContMap X Y) (fd : f.IsDense) (g h : ContMap Y Z) (p : \Pi (x : X) -> g (f x) = h (f x)) (y : Y) : g y = h y
  => denseSet-lift-unique fd g h (\lam (inP (x,q)) => rewriteI q (p x)) y

\func TopTransfer {X : \Set} {Y : TopSpace} (f : X -> Y) : TopSpace X \cowith
  | isOpen U => ∃ (V : isOpen) (U = f ^-1 V)
  | open-top => inP (top, open-top, idp)
  | open-inter (inP (V,Vo,p)) (inP (V',V'o,p')) => inP (V ∧ V', open-inter Vo V'o, pmap2 (∧) p p')
  | open-Union {S} h => inP (Set.Union \lam V => \Sigma (isOpen V) (f ^-1 V ⊆ Set.Union S), open-Union __., <=-antisymmetric (\lam (inP (U,SU,Ux)) => \case h SU \with {
    | inP (V,Vo,p) => inP (V, (Vo, rewriteI p $ Set.Union-cond SU), rewrite p in Ux)
  }) (\lam (inP (V,(Vo,p),Vfx)) => p Vfx))