\import Category.Functor
\import Equiv
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Order.Lattice
\import Order.PartialOrder
\import Paths
\import Paths.Meta
\import Set.Filter
\import Set.Subset
\import Topology.Locale
\import Topology.PartialCoverSpace
\import Topology.PartialCoverSpace.Category
\import Topology.RatherBelow

\record ProperLatticeFilter \extends Filter {
  \override A : BoundedLattice
  | isLatticeProper : Not (F CompleteLattice.bottom)
}

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

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

\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 (ProperLatticeFilter L)) : L
  => L.SJoin \lam a => points^* a ⊆ U

\lemma points_*-mono {L : Locale} {U V : Set (ProperLatticeFilter 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 (ProperLatticeFilter 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 (ProperLatticeFilter 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 (ProperLatticeFilter 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

\func proper-principal {L : Locale} {a : L} (a>0 : L.IsPositive a) : ProperLatticeFilter L \cowith
  | Filter => Filter.principal a
  | isLatticeProper a<=0 => TruncP.remove' $ L.positive_cover a>0 absurd $ a<=0 <=∘ bottom-univ

\lemma overt_points_* {L : Locale} (Lo : L.IsOvert) : points_* {L} bottom <= bottom
  => Join-univ \lam b => L.overt_cover Lo <=∘ Join-univ \lam b>0 => bottom-empty $ b. {proper-principal b>0} <=-refl

\func LocalePrecoverSpace (L : Locale) : PrecoverSpace \cowith
  | E => ProperLatticeFilter L
  | isCauchy C => top <= Join \lam (s : Given C) => points_* s.
  | cauchy-top => Join-cond (later (top,top-univ)) <=∘ Join-cond (later (top, idp))
  | cauchy-refine p e => p <=∘ Join-univ \lam (U,CU) => \case e CU \with {
    | inP (V,DV,U<=V) => points_*-mono U<=V <=∘ Join-cond (later (V,DV))
  }
  | cauchy-glue p e => p <=∘ Join-univ \lam (U,CU) => meet-univ <=-refl top-univ <=∘ MeetSemilattice.meet-monotone <=-refl (e CU) <=∘
                                                                                     Join-ldistr>= <=∘ Join-univ \lam (V,DUV) => transport (`<= _) points_*_meet $ Join-cond $ later (U ∧ V, inP (U, V, CU, DUV, idp))
  \where {
    \lemma points_<=< {a b : L} (p : a L.<=< b) : points^* a s<=< {LocalePrecoverSpace L} points^* b
      => unfolds $ p <=∘ join-univ (points^*-points_* (\lam {F} Fna (Fa : points^* a F) => isLatticeProper $ filter-mono (filter-meet Fna Fa) L.eval) <=∘ Join-cond (later (_, byLeft idp))) (points-unit <=∘ Join-cond (later (_, byRight idp)))

    \lemma cover-cauchy {C : Set L} (p : top <= L.SJoin C) : isCauchy {LocalePrecoverSpace L} \lam U => ∃ (a : C) (points^* a = U)
      => p <=∘ Join-univ \lam (a,Ca) => points-unit <=∘ Join-cond (later (_, inP (a, Ca, idp)))
  }

\func LocaleCoverSpace {L : Locale} (Lr : L.IsRegularLocale) : StronglyRegularCoverSpace \cowith
  | PrecoverSpace => LocalePrecoverSpace L
  | isStronglyRegular => __ <=∘ Join-univ \lam (U,CU) => Join-univ \lam (a,a<=<_*U) => Lr a <=∘ Join-univ \lam (b,b<=<a) => points-unit <=∘ Join-cond (later (points^* b, inP (U, CU, <=<-left (LocalePrecoverSpace.points_<=< b<=<a) a<=<_*U)))

\func LocaleCoverSpaceFunctor : Functor LocaleCat PrecoverSpaceCat \cowith
  | F => LocalePrecoverSpace
  | Func f => \new PrecoverMap {
    | func => filter-map f
    | func-cover c => func-top>= <=∘ f.func-<= c <=∘ func-Join>= <=∘ Join-univ \lam (V,DV) => func-Join>= <=∘ Join-univ \lam (b,p) => points^*-points_* (\lam c => later $ p $ later c) <=∘ Join-cond (later (_, inP (V, DV, idp)))
  }
  | Func-id => idp
  | Func-o => idp
  \where {
    \func filter-map {L M : Locale} (f : FrameHom M L) (x : ProperLatticeFilter L) : ProperLatticeFilter 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
      | isLatticeProper c => x.isLatticeProper $ transport x f.func-bottom c
  }

\func LocaleCoverSpaceFunctor-fullyFaithful {L M : Locale} (Lo : L.IsOvert) (Mr : M.IsRegularLocale) : Equiv (LocaleCoverSpaceFunctor.Func {L} {M})
  => Equiv.fromInjSurj _
    (\have r {f g : FrameHom M L} (p : LocaleCoverSpaceFunctor.Func f = LocaleCoverSpaceFunctor.Func g) {a : M} : f a <= g a
              => L.overt_cover Lo <=∘ Join-univ \lam fa>0 => propExt.dir (pmap {PrecoverMap _ _} (__ (proper-principal fa>0) a) p) <=-refl
     \in \lam p => exts \lam a => <=-antisymmetric (r p) $ r $ inv p)
    \lam f => inP (frameHom f, exts \lam F => exts \lam a => ext $ unfold $ unfold ({?}, {?}))
  \where {
    \protected \func frameHom (f : PrecoverMap (LocalePrecoverSpace L) (LocalePrecoverSpace M)) : FrameHom M L \cowith
      | func a => Join \lam (s : \Sigma (b : M) (b M.<=< a)) => points_* $ f ^-1 points^* s.
      | func-<= p => Join-univ \lam (b,b<=<x) => Join-cond $ later (b, <=<-left b<=<x p)
      | func-top>= => Join-cond (later (top, \lam _ => filter-top)) <=∘ Join-cond (later (top, <=<_top))
      | func-meet>= => Locale.Join-distr>= <=∘ Join-univ \lam ((b,b<=<x),(c,c<=<y)) => =_<= (inv $ pmap points_* (pmap (f ^-1) points^*_meet *> func-meet {^-1_FrameHom f} {points^* b} {points^* c}) *> points_*_meet) <=∘ Join-cond (later (b ∧ c , <=<_meet b<=<x c<=<y))
      | func-Join>= {J} {g} => Join-univ \lam (b,p) =>
        \have Mc : top <= M.SJoin (\lam c => (c = M.neg b) || (\Sigma (j : J) (c M.<=< g j)))
              => p <=∘ join-univ (M.SJoin-cond $ byLeft idp) (Join-univ \lam j => Mr (g j) <=∘ M.SJoin-univ \lam x<=<gj => M.SJoin-cond $ byRight $ later (j,x<=<gj))
        \in meet-univ <=-refl top-univ <=∘ L.meet-monotone (L.<=-refl {points_* $ f ^-1 points^* b}) (f.func-cover (LocalePrecoverSpace.cover-cauchy Mc)) <=∘ Join-ldistr>= <=∘ Join-univ \case \elim __ \with {
          | (_, inP (_, inP (_, byLeft idp, idp), idp)) => points_*_meet>= <=∘ points_*-mono (later \lam (fxb,fxnb) => absurd $ isLatticeProper $ filter-mono (filter-meet fxnb fxb) M.eval) <=∘ overt_points_* Lo <=∘ bottom-univ
          | (_, inP (_, inP (a, byRight (j,a<=<gj), idp), idp)) => meet-right <=∘ L.Join-cond (later (a,a<=<gj)) {\lam s => points_* (f ^-1 points^* s.)} <=∘ Join-cond j
        }
  }