\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.1 ⊆ V.1
| <=-refl => <=-refl
| <=-transitive => <=∘
| <=-antisymmetric p q => ext (<=-antisymmetric p q)
| Join {J} g => (\lam x => ∃ (j : J) ((g j).1 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.1 ∧ V.1, open-inter U.2 V.2)
| 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.1 Ux) (g.1 Vx), \lam xab => (f.2 $filter-mono meet-left xab, g.2$ 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.1 Ux) }, \case filter-Join __ \with { | inP ((a, inP (U,SU,g)), xa) => inP (U, SU, g.2 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.1) (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.2 (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.1$ rewrite p in Fx).1)
| cover-idemp j p => inP (j, rewrite p $F-conj.2 (Fx,Fx)) | cover-comm p j q => inP (j, rewrite q$ F-conj.2 \have Fab => F-conj.1 (rewrite p in Fx) \in (Fab.2, Fab.1))
| cover-ldistr p c q =>
\have Fab => F-conj.1 (rewrite p in Fx)
\in \case cover-filter c Fab.2 \with {
| inP (j,Ffj) => inP (j, rewrite (q j) $F-conj.2 (Fab.1, 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