\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
\func points^* {L : Locale} (a : L) : Set (Filter L)
=> \lam F => \Sigma (Not (F bottom)) (F a)
\lemma points^*-mono {L : Locale} {a b : L} (p : a <= b) : points^* a ⊆ points^* b
=> \lam s => (s.1, filter-mono s.2 p)
\lemma points^*_meet>= {L : Locale} {a b : L} : points^* a ∧ points^* b ⊆ points^* (a ∧ b)
=> \lam {x} (xa,xb) => (xa.1, filter-meet xa.2 xb.2)
\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 (Filter L)) : L
=> L.SJoin \lam a => points^* a ⊆ U
\lemma points_*-mono {L : Locale} {U V : Set (Filter 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 (Filter 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 (Filter 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 (Filter 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 LocalePrecoverSpace (L : Locale) : PrecoverSpace \cowith
| E => Filter L
| isCauchy C => top <= Join \lam (s : Given C) => points_* s.1
| 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) => Fa.1 $ filter-mono (filter-meet Fna.2 Fa.2) L.eval) <=∘ Join-cond (later (_, byLeft idp))) (points-unit <=∘ Join-cond (later (_, byRight 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 {x} c => later $ p $ later (\lam q => c.1 $ transport x f.func-bottom q, c.2)) <=∘ 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 : Filter L) : Filter 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
}
\func LocaleCoverSpaceFunctor-fullyFaithful {L M : Locale} (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
=> propExt.dir (pmap {PrecoverMap _ _} (__ (Filter.principal (f a)) a) p) <=-refl
\in \lam p => exts \lam a => <=-antisymmetric (r p) $ r $ inv p)
\lam f => inP ({?}, {?})
\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.1
| func-<= p => Join-univ \lam (b,b<=<x) => Join-cond $ later (b, <=<-left b<=<x p)
| func-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 {?}
}