\import Category.Functor
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Order.Lattice
\import Order.PartialOrder
\import Paths.Meta
\import Set.Filter
\import Set.Subset
\import Topology.Locale
\import Topology.TopSpace
\import Topology.TopSpace.Category
\open Bounded(top, top-univ, bottom)

\func OpensFrame (S : TopSpace) : Locale (Given S.isOpen) \cowith
  | <= U V => U. ⊆ V.
  | <=-refl => <=-refl
  | <=-transitive => <=∘
  | <=-antisymmetric p q => ext (<=-antisymmetric p q)
  | Join {J} g => (\lam x => ∃ (j : J) ((g j). x), S.open-IUnion g)
  | Join-cond j c => inP (j,c)
  | Join-univ f (inP (j,c)) => f j c
  | meet U V => (U. ∧ V., open-inter U. V.)
  | meet-left => meet-left
  | meet-right => meet-right
  | meet-univ => meet-univ
  | Join-ldistr>= (a, inP (j,c)) => inP (j, (a, c))

\instance PointsSpace (L : Locale) : TopSpace (CompleteFilter L)
  | isOpen U => ∃ (a : L) (\Pi {x : CompleteFilter L} -> U x <-> x a)
  | open-top => inP (top, \lam {x} => (\lam _ => filter-top, \lam _ => ()))
  | open-inter (inP (a,f)) (inP (b,g)) => inP (a ∧ b, \lam {x} => (\lam (Ux,Vx) => filter-meet (f. Ux) (g. Vx), \lam xab => (f. $ filter-mono meet-left xab, g. $ filter-mono meet-right xab)))
  | open-Union {S} f => inP (CompleteLattice.SJoin \lam a => ∃ (U : S) (\Pi {x : CompleteFilter L} -> U x <-> x a),
                             \lam {x} => (\lam (inP (U,SU,Ux)) => \case f SU \with {
                               | inP (a,g) => filter-mono (Join-cond $ later (a, inP (U, SU, g))) (g. Ux)
                             }, \case filter-Join __ \with {
                               | inP ((a, inP (U,SU,g)), xa) => inP (U, SU, g. xa)
                             }))

\func PointsSpaceFunctor : Functor LocaleCat TopCat \cowith
  | F => PointsSpace
  | Func {L M : Locale} (f : FrameHom M L) : ContMap (PointsSpace L) (PointsSpace M) \cowith {
    | func => filter-map f
    | func-cont (inP (b,c)) => inP (f b, \lam {x} => c)
  }
  | Func-id => idp
  | Func-o => idp
  \where {
    \func filter-map {L M : Locale} (f : FrameHom M L) (x : CompleteFilter L) : CompleteFilter M \cowith
      | F b => x (f b)
      | filter-mono p => filter-mono (func-<= p)
      | filter-top => rewrite f.func-top filter-top
      | filter-meet xfa xfb => rewrite f.func-meet $ filter-meet xfa xfb
      | filter-Join => rewrite f.func-Join \lam c => filter-Join c
  }

\func points {L : Locale} : FrameHom L (OpensFrame (PointsSpace L)) \cowith
  | func a => (\lam x => x a, inP (a, \lam {x} => <->refl))
  | func-<= p {x} => filter-mono p
  | func-top>= _ => filter-top
  | func-meet>= (xa,xb) => filter-meet xa xb
  | func-Join>= c => filter-Join c

\func points^* {L : Locale} (a : L) : Set (CompleteFilter L)
  => \lam x => x a

\lemma points^*-mono {L : Locale} {a b : L} (p : a <= b) : points^* a ⊆ points^* b
  => filter-mono p __

\lemma points^*_top>= {L : Locale} : top ⊆ points^* {L} top => \lam _ => filter-top

\lemma points^*_top {L : Locale} : points^* {L} top = top => <=-antisymmetric top-univ points^*_top>=

\lemma points^*_meet>= {L : Locale} {a b : L} : points^* a ∧ points^* b ⊆ points^* (a ∧ b)
  => \lam {x} (xa,xb) => filter-meet xa xb

\lemma points^*_meet {L : Locale} {a b : L} : points^* (a ∧ b) = points^* a ∧ points^* b
  => <=-antisymmetric (meet-univ (points^*-mono meet-left) (points^*-mono meet-right)) points^*_meet>=

\func points_* {L : Locale} (U : Set (CompleteFilter L)) : L
  => L.SJoin \lam a => points^* a ⊆ U

\lemma points_*-mono {L : Locale} {U V : Set (CompleteFilter L)} (p : U ⊆ V) : points_* U <= points_* V
  => Join-univ \lam (a,q) => Join-cond $ later (a, q <=∘ p)

\lemma points_*_meet>= {L : Locale} {U V : Set (CompleteFilter L)} : points_* U ∧ points_* V <= points_* (U ∧ V)
  => Join-ldistr>= <=∘ Join-univ \lam (b,q) => Locale.Join-rdistr>= <=∘ Join-univ \lam (a,p) => Join-cond $ later (a ∧ b, meet-univ (points^*-mono meet-left <=∘ p) (points^*-mono meet-right <=∘ q))

\lemma points_*_meet {L : Locale} {U V : Set (CompleteFilter L)} : points_* (U ∧ V) = points_* U ∧ points_* V
  => <=-antisymmetric (meet-univ (points_*-mono meet-left) (points_*-mono meet-right)) points_*_meet>=

\lemma points^*-points_* {L : Locale} {a : L} {U : Set (CompleteFilter L)} (p : points^* a ⊆ U) : a <= points_* U
  => Join-cond $ later (a,p)

\lemma points-unit {L : Locale} {a : L} : a <= points_* (points^* a)
  => points^*-points_* <=-refl

\lemma points-counit {L : Locale} {U : Set (CompleteFilter L)} : points^* (points_* U) ⊆ U
  => \lam p => \case filter-Join p \with {
    | inP ((a,q),xa) => q xa
  }

\func framePres-point {P : FramePres} (F : P -> \Prop) (\property F-inh : ∃ F) (\property F-conj : \Pi {a b : P} -> F (conj a b) <-> (\Sigma (F a) (F b)))
                      (\property F-cover : \Pi {J : \Set} {a : P} {f : J -> P} -> BasicCover a f -> F a -> ∃ (j : J) (F (f j)))
  : CompleteFilter (PresentedFrame P) \cowith
  | F U => ∃ (x : U.) (F x)
  | filter-mono {U} {V} p (inP (x,Ux,Fx)) => inP (x, p Ux, Fx)
  | filter-top => TruncP.map F-inh \lam (x,Fx) => (x, (), Fx)
  | filter-meet {U} {V} (inP (x,Ux,Fx)) (inP (y,Vy,Fy)) => inP (conj x y, cover-inj (x, y, Ux, Vy) idp, F-conj. (Fx,Fy))
  | filter-Join (inP (x,c,Fx)) => \case cover-filter c Fx \with {
    | inP ((j,x,fjx),Fx) => inP (j, inP (x, fjx, Fx))
  }
  \where {
    \lemma cover-filter {x : P} {J : \Set} {g : J -> P} (c : Cover x g) (Fx : F x) : ∃ (j : J) (F (g j)) \elim c
      | cover-basic b => F-cover b Fx
      | cover-inj j p => inP (j, rewrite p Fx)
      | cover-trans c e => \case cover-filter c Fx \with {
        | inP (i,Ffi) => cover-filter (e i) Ffi
      }
      | cover-proj1 p j q => inP (j, rewrite q (F-conj. $ rewrite p in Fx).)
      | cover-idemp j p => inP (j, rewrite p $ F-conj. (Fx,Fx))
      | cover-comm p j q => inP (j, rewrite q $ F-conj. \have Fab => F-conj. (rewrite p in Fx) \in (Fab., Fab.))
      | cover-ldistr p c q =>
        \have Fab => F-conj. (rewrite p in Fx)
        \in \case cover-filter c Fab. \with {
               | inP (j,Ffj) => inP (j, rewrite (q j) $ F-conj. (Fab., Ffj))
             }
  }

\func HasDensePoints (L : Locale) : \Prop
  => points_* bottom <= L.bottom

\lemma hasDensePoints-char {L : Locale} : HasDensePoints L <-> (\Pi {a : L} -> (\Pi {x : CompleteFilter L} -> Not (x a)) -> a <= bottom)
  => (\lam d {a} c => Join-cond (later (a, \lam xa => absurd $ c xa)) <=∘ d, \lam d => Join-univ \lam (b,p) => d \lam xb => \case p xb \with {
    | inP ((),_)
  })

\lemma hasDensePoints-fromPres {P : FramePres} (d : \Pi {a : P} -> points^* (PresentedFrame.embed a) ⊆ bottom -> Cover a absurd) : HasDensePoints (PresentedFrame P)
  => cover-trans __ \lam ((U,p),V,UV) => cover-trans (d $ points^*-mono (PresentedFrame.embed<= $ cover-inj (V,UV) idp) <=∘ p) \case __

\func HasStronglyDensePoints (L : Locale) : \Prop
  => \Pi (a : L) -> a <= L.pHat (∃ (x : CompleteFilter L) (x a))

\lemma densePoints_cover {L : Locale} (d : HasStronglyDensePoints L) (a : L) : a <= Join \lam (_ : ∃ (x : CompleteFilter L) (x a)) => a
  => meet-univ <=-refl (d a) <=∘ Join-ldistr>= <=∘ Join-univ \lam c => meet-left <=∘ Join-cond c

\lemma hasStronglyDensePoints-fromPres {P : FramePres} (d : \Pi (a : P) -> Cover a {∃ (points^* (PresentedFrame.embed a))} \lam _ => a) : HasStronglyDensePoints (PresentedFrame P)
  => \lam U {a} Ua => cover-trans (d a) \lam (inP (x,ax)) => cover-inj (inP (x, filter-mono (PresentedFrame.embed<= $ cover-inj (a,Ua) idp) ax), a, ()) idp