\import Category.Functor
\import Equiv
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Order.Lattice
\import Order.Lattice.CompleteLattice
\import Order.PartialOrder
\import Paths
\import Paths.Meta
\import Set
\import Set.Filter
\import Set.Set
\import Topology.Locale
\import Topology.Locale.LocaleCat
\import Topology.Locale.PreorderSite
\import Topology.TopSpace
\import Topology.TopSpace.TopSpaceCategory
\open SiteLocale
\open Cover

\func OpensFrame (S : TopSpace) : Locale (Given S.isOpen) \cowith
  | <= U V => U. ⊆ V.
  | <=-refl => <=-refl
  | <=-transitive => <=∘
  | <=-antisymmetric p q => ext (<=-antisymmetric p q)
  | Join C => (\lam x => ∃ (U : C) (U. x), S.cover-open $ later \lam (inP (U,CU,Ux)) => inP (U., U., Ux, \lam {y} Uy => inP (U,CU,Uy)))
  | Join-cond {C} {U} CU Ux => inP (U,CU,Ux)
  | Join-univ {C} {U} h (inP (V,CV,Vx)) => h CV Vx
  | meet U V => (U. ∧ V., open-inter U. V.)
  | meet-left => meet-left
  | meet-right => meet-right
  | meet-univ => meet-univ
  | Join-ldistr>= {C} {U} (Ux, inP (V,CV,Vx)) => inP ((U. ∧ V., open-inter U. V.), SetIm-con CV, (Ux,Vx))

\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 xab meet-left, g. $ filter-mono xab meet-right)))
  | open-Union {S} f => inP (Join \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 (g. Ux) $ Join-cond $ inP (U,SU,g)
                             }, \case filter-Join __ \with {
                               | inP (a, inP (U,SU,g), xa) => inP (U, SU, g. xa)
                             }))

\func points-map {L M : Locale} (f : LocaleHom L M) (x : CompleteFilter L) : CompleteFilter M \cowith
  | F b => x (f b)
  | filter-mono q p => filter-mono q (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 x.filter-SJoin

\func PointsSpaceFunctor.{u} : Functor LocaleCat.{u} TopCat.{u} \cowith
  | F L => PointsSpace L
  | Func {L M : Locale.{u}} (f : FrameHom M L) : ContMap (PointsSpace L) (PointsSpace M) \cowith {
    | func => points-map f
    | func-cont (inP (b,c)) => inP (f b, \lam {x} => c)
  }
  | Func-id => idp
  | Func-o => idp

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

\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
  => Join \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 q => Join-cond (q <=∘ p)

\lemma points_*_meet>= {L : Locale} {U V : Set (CompleteFilter L)} : points_* U ∧ points_* V <= points_* (U ∧ V)
  => Join-ldistr>= <=∘ L.SJoin-univ \lam {b} q => L.Join-rdistr>= <=∘ L.SJoin-univ \lam {a} p => Join-cond $ 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 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
  }

\record SitePoint (P : PreorderSite) (\coerce F : P -> \Prop)
  | sitePoint-mono {x y : P} : F x -> x <= y -> F y
  | sitePoint-top : ∃ F
  | sitePoint-meet {x y : P} : F x -> F y -> ∃ (z : F) (Cover z (single x)) (Cover z (single y))
  | sitePoint-cover {x : P} {U : Set P} : isBasicCover x U -> F x -> ∃ (y : U) (F y)

\func site-point {P : PreorderSite} (p : SitePoint P) : CompleteFilter (SiteLocale P) \cowith
  | F U => ∃ (x : U.) (p x)
  | filter-mono {U} {V} (inP (x,Ux,px)) U<=V => inP (x, U<=V Ux, px)
  | filter-top => TruncP.map p.sitePoint-top \lam (x,px) => (x, (), px)
  | filter-meet {U} {V} (inP (x,Ux,px)) (inP (y,Vy,py)) => \case sitePoint-meet px py \with {
    | inP (z,pz,z<=x,z<=y) => inP (z, (U. $ cover-sub z<=x $ single_<= Ux, V. $ cover-sub z<=y $ single_<= Vy), pz)
  }
  | filter-Join (inP (x,c,px)) => \case point-cover px c \with {
    | inP (y, inP (U,CU,Uy), py) => inP (U, CU, inP (y,Uy,py))
  }
  \where {
    \lemma point-cover {p : SitePoint P} {x : P} {U : Set P} (px : p x) (c : Cover x U) : ∃ (y : U) (p y) \elim c
      | cover-inj {t} x<=t Ut => inP (t, Ut, sitePoint-mono px x<=t)
      | cover-trans x<=T T<=U => \case sitePoint-cover x<=T px \with {
        | inP (y,Ty,py) => point-cover py (T<=U Ty)
      }

    \lemma point-cover1 {p : SitePoint P} {x y : P} (px : p x) (c : Cover x (single y)) : p y
      => \case point-cover px c \with {
        | inP (_,idp,py) => py
      }

    \lemma filter-elem {p : CompleteFilter (SiteLocale P)} {U : Opens P} (pU : p U) : ∃ (x : U.) (p (embed x))
      => p.filter-SJoin $ transport p SiteLocale.element_SJoin pU

    \func locale-point (p : CompleteFilter (SiteLocale P)) : SitePoint P \cowith
      | F x => p (embed x)
      | sitePoint-mono px x<=y => filter-mono px $ embed-univ (cover-inj x<=y idp)
      | sitePoint-top => \case filter-elem filter-top \with {
        | inP (a,_,pa) => inP (a,pa)
      }
      | sitePoint-meet px py => \case filter-elem (filter-meet px py) \with {
        | inP (a,(a<=x,a<=y),pa) => inP (a, pa, a<=x, a<=y)
      }
      | sitePoint-cover x<=U px => p.filter-SJoin $ filter-mono px $ embed-univ $ cover-trans x<=U
          \lam Ut => cover-refl $ inP (_, SetIm-con Ut, cover-refl idp)

    \lemma equiv : QEquiv {SitePoint P} {CompleteFilter (SiteLocale P)} site-point locale-point \cowith
      | ret_f p => exts \lam a => propExt (\lam (inP (x,x<=a,px)) => point-cover1 px x<=a) (\lam pa => inP (a, cover-refl idp, pa))
      | f_sec p => exts \lam U => propExt (\lam (inP (x,Ux,px)) => filter-mono px $ embed-univ Ux) filter-elem
  }

\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 (\lam xa => absurd $ c xa)) <=∘ d, \lam d => Join-univ \lam p => d \lam xb => bottom-empty $ p xb)

\lemma hasDensePoints-site {P : PreorderSite} (d : \Pi {a : P} -> (\Pi {p : SitePoint P} -> Not (p a)) -> Cover a empty) : HasDensePoints (SiteLocale P)
  => cover-trans* __ \lam {t} (inP (U,eU,Ut)) => cover-sub (d \lam {p} pt => bottom-empty $ eU {site-point p} $ inP (t,Ut,pt)) \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 <= L.pHat (∃ (x : CompleteFilter L) (x a))
  => meet-univ <=-refl (d a) <=∘ Join-ldistr>= <=∘ L.SJoin-univ \lam c => Join-cond c

\lemma hasStronglyDensePoints-site {P : PreorderSite} (d : \Pi (a : P) -> Cover a \lam _ => ∃ (p : SitePoint P) (p a)) : HasStronglyDensePoints (SiteLocale P)
  => \lam U {a} Ua => cover-sub (d a) \lam (inP (p,pa)) => inP ((SiteLocale P).top, inP (site-point p, inP (a,Ua,pa)), ())