\import Category.Functor
\import Data.Bool
\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.Filter
\import Set.Set
\import Topology.CoverSpace
\import Topology.CoverSpace.CoverSpaceCategory
\import Topology.CoverSpace.Complete
\import Topology.CoverSpace.StronglyComplete (StronglyCompleteCoverSpace)
\import Topology.Locale \hiding (<=<_<=)
\import Topology.Locale.LocaleCat
\import Topology.Locale.Points
\import Topology.Locale.PreorderSite
\import Topology.RatherBelow
\open LocalePrecoverSpace
\open RatherBelow
\open CompleteLattice
\open Cover
\open SiteLocale

\func CoverSpaceLocale (X : PrecoverSpace) : Locale
  => SiteLocale (site {X})
  \where {
    \func site {X : PrecoverSpace} : PreorderSite (Set X) \cowith
      | Preorder => SetLattice X
      | isBasicCover U C => OneOf (∃ (D : X.isCauchy) (C = SetIm (U ∧) D), C = (s<=< U), Given (\Pi {x : X} -> Not (U x)) (C = empty))
      | basic-cover-stable {V} {U} V<=U {C} => \case \elim C, \elim __ \with {
        | _, inP (, inP (C,Cc,idp)) => inP (_, inP (, inP (C,Cc,idp)), SetIm-elim \lam {W} CW => inP $ later (_, SetIm-con CW, MeetSemilattice.meet-monotone V<=U <=-refl), SetIm-elim \lam _ => meet-left)
        | _, inP (,idp) => inP (_, inP (,idp), \lam {W} W<=<V => inP (W, <=<-left W<=<V V<=U, <=-refl), s<=<_<= __)
        | _, inP (,(U=0,idp)) => inP (_, inP (, (\lam Vx => U=0 (V<=U Vx), idp)), Refines-refl, absurd __)
      }

    \lemma cover-cauchy {X : PrecoverSpace} {C : Set (Set X)} (Cc : isCauchy C) : Cover {site} top C
      => cover-sub (cover-basic $ inP (, inP (C,Cc,idp))) $ unfolds $ SetIm-elim \lam Ca => transport C (inv TopMeetSemilattice.top-left) Ca

    \lemma cover-reg {X : PrecoverSpace} {U : Set X} : Cover {site} U \lam V => V s<=< U
      => cover-basic $ inP (,idp)

    \lemma cover-empty {X : PrecoverSpace} {U : Set X} (Ue : \Pi {x : X} -> Not (U x)) {C : Set (Set X)} : Cover {site} U C
      => cover-sub (cover-basic $ inP (, (Ue,idp))) empty-univ

    \lemma embed_meet {U V : Set X} : embed U ∧ embed V = embed {site} (U ∧ V)
      => <=-antisymmetric (\lam {W} (W<=U,W<=V) => cover-refine (cover-inter W<=U W<=V) \lam {T} (inP (_,idp,_,idp,T<=U,T<=V)) => inP (_, idp, \lam t => (T<=U t, T<=V t))) $ embed-univ (cover-inj meet-left idp, cover-inj meet-right idp)

    \lemma embed_<=< {V U : Set X} (V<=<U : V s<=< U) : embed V Locale.<=< {CoverSpaceLocale X} embed U
      => \lam _ => cover-left top-univ $ cover-cauchy $ cauchy-subset (unfolds in V<=<U) \lam {W} => later \case \elim __ \with {
        | byLeft p => inP (_, byLeft idp, cover-refl $ inP (embed (Compl V), embed_meet =<= embed-univ (unfolds $ cover-basic $ inP (, (\lam s => s. s., ext \lam U => propExt (\lam (inP (_,e,_)) => e) absurd))), cover-refl (inv p)))
        | byRight p => inP (_, byRight idp, cover-refl (inv p))
      }

    \lemma regular : Locale.IsRegularLocale {CoverSpaceLocale X}
      => regular-site \lam U => cover-sub cover-reg (embed_<=< __)

    \lemma cover-char {X : StronglyRegularCoverSpace} {U : Set X} {C : Set(Set X)} (c : Cover {site} U C) {U' : Set X} (U'<=<U : U' s<=< U)
      : X.isCauchy \lam V => (V = Compl U') || C V \elim c
      | cover-inj {V} U<=V CV => cauchy-refine U'<=<U \lam {W} => \case \elim __ \with {
        | byLeft p => inP (W, byLeft p, <=-refl)
        | byRight p => inP (V, byRight CV, p =<= U<=V)
      }
      | cover-trans (inP (, inP (D,Dc,idp))) T<=C => cauchy-glue-refine (isStronglyRegular Dc) \lam {V'} (inP (V,DV,V'<=<V)) =>
        cauchy-subset (cover-char (T<=C $ SetIm-con $ later DV) (<=<_meet U'<=<U V'<=<V)) \lam {W} => later \case \elim __ \with {
          | byLeft p => inP (_, byLeft idp, \lam s U'x => =_<= p s. (U'x, s.))
          | byRight CW => inP (W, byRight CW, meet-right)
        }
      | cover-trans (inP (,idp)) T<=C => cauchy-glue-refine (isStronglyRegular $ isStronglyRegular $ unfolds in U'<=<U) \lam {W} => \case \elim W, \elim __ \with {
        | W', inP (W, inP (_, byLeft idp, W<=<~U'), W'<=<W) => top-cauchy $ inP $ later (_, byLeft idp, \lam W'x => s<=<_<= W<=<~U' (s<=<_<= W'<=<W W'x.))
        | W', inP (W, inP (_, byRight idp, W<=<U), W'<=<W) => cauchy-subset (cover-char (T<=C W<=<U) W'<=<W) \lam {V} => later \case \elim __ \with {
          | byLeft V=~W' => inP (_, byLeft idp, \lam s => absurd $ =_<= V=~W' s. s.)
          | byRight CV => inP (V, byRight CV, meet-right)
        }
      }
      | cover-trans (inP (,(Ue,idp))) _ => top-cauchy $ byLeft $ ext \lam a => propExt (\lam _ U'a => Ue $ s<=<_<= U'<=<U U'a) (\lam _ => ())

    \lemma cover-point-char {X : StronglyRegularCoverSpace} {U : Set X} {C : Set (Set X)} (c : Cover {site} U C) {x : X} (x<=<U : single x <=< U) : ∃ (V : C) (single x <=< V)
      => \case s<=<-inter x<=<U \with {
        | inP (V,x<=<V,V<=<U) => \case CoverSpace.cauchy-regular-cover (cover-char c V<=<U) x \with {
          | inP (W, byLeft p, x<=<W) => absurd $ <=<_<= (rewrite p in x<=<W) idp $ s<=<_<= x<=<V idp
          | inP (W, byRight CW, x<=<W) => inP (W, CW, x<=<W)
        }
      }

    \lemma hasWeaklyDensePoints {X : StronglyRegularCoverSpace} (Xd : X.HasWeaklyDensePoints) : HasDensePoints (CoverSpaceLocale X)
      => hasDensePoints-site \lam {U} p => cover-trans* cover-reg \lam {V} V<=<U => cover-empty \lam {x} Vx =>
          p {CoverSpaceLocale-unit.sitePoint x} $ later $ cauchy-subset (unfolds in s<=<_<=< V<=<U) $ later \lam {W} h (_,(idp,Wx)) => h (x,(Vx,Wx))

    \lemma cover-inh {X : PrecoverSpace} (Xd : X.HasDensePoints) {U : Set X} : Cover {site} U (\lam _ => ∃ (x : X) (U x))
      => cover-trans (inP (,idp)) \lam {V} V<=<U => cover-trans (inP (, inP (_, Xd V<=<U, idp))) $ SetIm-elim \lam {W} => later \case \elim W, \elim __ \with {
        | _, (byLeft idp, t) => cover-empty $ later \lam (Vx,nVx) => nVx Vx
        | _, (byRight idp, r) => cover-refl r
      }

    \lemma cover-reg-inh {X : PrecoverSpace} (Xd : X.HasDensePoints) {U : Set X} : Cover {site} U (\lam _ => ∃ (x : X) (single x <=< U))
      => cover-trans* cover-reg \lam {V} V<=<U => cover-sub (cover-inh Xd) \lam (inP (x,Vx)) => inP (x, <=<-right (single_<= Vx) $ s<=<_<=< V<=<U)

    \lemma hasStronglyDensePoints {X : StronglyRegularCoverSpace} (Xd : X.HasDensePoints) : HasStronglyDensePoints (CoverSpaceLocale X)
      => hasStronglyDensePoints-site \lam U => cover-sub (cover-reg-inh Xd) \lam (inP (x,x<=U)) => inP (CoverSpaceLocale-unit.sitePoint x, x<=U)
  }

\func LocalePrecoverSpace (L : Locale) : PrecoverSpace \cowith
  | E => CompleteFilter L
  | isCauchy C => top <= SJoin points_* C
  | cauchy-cover t x => \case filter-Join $ filter-mono {x} filter-top t \with {
    | inP (_, inP ((U,CU),idp), xU) => \case filter-Join xU \with {
      | inP (a,p,xa) => inP (U, CU, p xa)
    }
  }
  | cauchy-top => Join-cond top-univ <=∘ SJoin-cond idp
  | cauchy-refine p e => p <=∘ SJoin-univ \lam {U} CU => \case e CU \with {
    | inP (V,DV,U<=V) => points_*-mono U<=V <=∘ SJoin-cond DV
  }
  | cauchy-glue p e => p <=∘ SJoin-univ \lam {U} CU => meet-univ <=-refl top-univ <=∘ MeetSemilattice.meet-monotone <=-refl (e CU) <=∘
      L.SJoin-ldistr>= <=∘ SJoin-univ \lam {V} DUV => later $ transport (<= _) points_*_meet $ SJoin-cond $ inP $ later (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 xna xa => CompleteFilter.isProper $ filter-mono (filter-meet xna xa) L.<=-eval) <=∘ SJoin-cond (byLeft idp)) (points-unit <=∘ SJoin-cond (byRight idp))

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

    \lemma single_<=<-char {x : CompleteFilter L} {U : Set (CompleteFilter L)} (x<=<U : single x <=< {LocalePrecoverSpace L} U) : ∃ (a : L) (x a) (points^* a ⊆ U)
      => \have t : top L.<= L.Join \lam a => x a -> points^* a ⊆ U => x<=<U <=∘ SJoin-univ \lam {W} h => later $ L.Join-univ \lam {a} q => Join-cond \lam xa => q <=∘ later (h (x, (idp, q xa)))
         \in \case x.filter-Join $ filter-mono filter-top t \with {
          | inP (a,h,xa) => inP (a, xa, h xa)
        }

    \lemma hasWeaklyDensePoints (Ld : HasDensePoints L) : (LocalePrecoverSpace L).HasWeaklyDensePoints
      => __ <=∘ SJoin-univ \lam {U} => later \case \elim __ \with {
        | byLeft e => rewrite e $ Ld <=∘ bottom-univ
        | byRight CU => SJoin-cond CU
      }

    \lemma hasDensePoints (Ld : HasStronglyDensePoints L) : (LocalePrecoverSpace L).HasDensePoints
      => __ <=∘ SJoin-univ \lam {U} CU => L.pHat-left (densePoints_cover Ld _) <=∘ IJoin-univ (later \lam (inP (x,c)) => SJoin-cond $ later (CU, \case filter-Join c \with {
        | inP (a,p,xa) => inP (x, p xa)
      }))
  }

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

\func LocaleCoverSpaceFunctor.{u} : Functor LocaleCat.{u} PrecoverSpaceCat.{u} \cowith
  | F L => LocalePrecoverSpace L
  | Func f => \new PrecoverMap {
    | func => points-map f
    | func-cover c => func-top>= <=∘ f.func-<= c <=∘ f.func-SJoin>= <=∘ SJoin-univ \lam {V} DV => func-Join>= <=∘
        SJoin-univ \lam {b} p => later $ points^*-points_* (\lam c => unfolds $ unfolds $ p $ later c) <=∘ SJoin-cond (inP $ later (V,DV,idp))
  }
  | Func-id => idp
  | Func-o => idp

\lemma LocaleCoverSpaceFunctor-fullyFaithful.{u} {L M : Locale.{u}} (Ld : HasDensePoints L) (Mr : M.IsRegularLocale) : IsEquiv (LocaleCoverSpaceFunctor.Func {L} {M})
  => IsEquiv.fromInjSurj
      (\have r {f g : FrameHom M L} (p : LocaleCoverSpaceFunctor.Func f = LocaleCoverSpaceFunctor.Func g) {a : M} : f a <= g a
          => f.func-<= (Mr a) <=∘ func-Join>= <=∘ SJoin-univ (later \lam {b} b<=<a => meet-univ <=-refl (top-univ <=∘ func-top>= <=∘ g.func-<= b<=<a <=∘ g.func-join>=) <=∘
              ldistr>= <=∘ join-univ (hasDensePoints-char. Ld (\lam {x} c => x.isProper $
                filter-mono (filter-meet (filter-mono c meet-right) (propExt.dir (pmap {PrecoverMap _ _} (__ x b) p) $ filter-mono c meet-left)) $
                  func-meet>= <=∘ func-<= M.<=-eval <=∘ g.func-bottom>=) <=∘ bottom-univ) meet-right)
       \in \lam p => exts \lam a => <=-antisymmetric (r p) $ r $ inv p)
      (\lam f => inP (frameHom f, exts \lam x => exts \lam a => ext (\case x.filter-SJoin __ \with {
        | inP (b,b<=<a,r) => \case filter-Join r \with {
          | inP (c,q,xc) => filter-mono (q xc) (Topology.Locale.<=<_<= b<=<a)
        }
      }, \lam fxa => \case filter-Join $ filter-mono fxa (Mr a) \with {
        | inP (b,b<=<a,fxb) => \case filter-Join $ filter-mono fxb (Mr b) \with {
          | inP (b',b'<=<b,fxb') => \case filter-Join $ x.filter-mono filter-top $ f.func-cover $ LocalePrecoverSpace.cover-cauchy {M} {\lam x => (x = M.neg b') || (x = b)} $ b'<=<b <=∘ join-univ (Join-cond $ byLeft idp) (Join-cond $ byRight idp) \with {
            | inP (_, inP ((_, inP (_, inP (_, byLeft idp, idp), idp)), idp), xe) => absurd \case filter-Join xe \with {
              | inP (c,q,xc) => CompleteFilter.isProper $ filter-mono (filter-meet (q xc) fxb') M.<=-eval
            }
            | inP (_, inP ((_, inP (_, inP (_, byRight idp, idp), idp)), idp), xe) => \case filter-Join xe \with {
              | inP (c,q,xc) => filter-mono xe (SJoin-cond b<=<a)
            }
          }
        }
      })))
  \where {
    \protected \func frameHom (f : PrecoverMap (LocalePrecoverSpace L) (LocalePrecoverSpace M)) : FrameHom M L \cowith
      | func a => SJoin (\lam b => points_* $ f ^-1 points^* b) (M.<=< a)
      | func-<= p => SJoin-univ \lam {b} b<=<x => SJoin-cond (<=<-left b<=<x p)
      | func-top>= => Join-cond (later \lam _ => filter-top) <=∘ SJoin-cond <=<_top
      | func-meet>= => L.SJoin-distr>= <=∘ SJoin-univ (later \lam {(b,c)} (b<=<x,c<=<y) => inv (pmap points_* (pmap (f ^-1) points^*_meet *> func-meet {^-1_FrameHom f} {points^* b} {points^* c}) *> points_*_meet) =<= SJoin-cond (<=<_meet b<=<x c<=<y))
      | func-Join>= {C} => SJoin-univ $ later \lam {b} p =>
        \have Mc : top <= M.Join (\lam c => (c = M.neg b) || Given (x : C) (c M.<=< x))
                 => p <=∘ join-univ (Join-cond $ byLeft idp) (Join-univ \lam {x} Cx => Mr x <=∘ Join-univ \lam {y} y<=<x => Join-cond $ byRight (x,Cx,y<=<x))
        \in meet-univ <=-refl (top-univ <=∘ f.func-cover (LocalePrecoverSpace.cover-cauchy Mc)) <=∘ L.SJoin-ldistr>= <=∘ SJoin-univ \lam {x} => later \case \elim x, \elim __ \with {
          | _, inP (_, (inP (_, byLeft idp, idp)), idp) => points_*_meet>= <=∘ points_*-mono (later \lam (fxb,fxnb) => absurd $ CompleteFilter.isProper $ filter-mono (filter-meet fxnb fxb) M.<=-eval) <=∘ Ld <=∘ bottom-univ
          | _, inP (_, (inP (a, byRight (d,Cd,a<=<d), idp)), idp) => meet-right <=∘ SJoin-cond a<=<d <=∘ SJoin-cond Cd
        }
  }

\func CoverSpaceLocale-unit {X : StronglyRegularCoverSpace} (Xo : X.HasWeaklyDensePoints) : PrecoverMap X (LocaleCoverSpace {CoverSpaceLocale X} CoverSpaceLocale.regular) \cowith
  | func x => site-point (sitePoint x)
  | func-cover Dc => Xo $ cauchy-refine (isRegular $ CoverSpaceLocale.cover-char (Dc ()) <=<_top) \lam {V} => \case __ \with {
    | inP (_, byLeft idp, V<=<U) => inP (bottom, byLeft idp, <=<_<= V<=<U <=∘ \lam t => absurd $ t ())
    | inP (_, byRight (inP (_, inP ((W,DW),idp), U<=W)), V<=<U) => inP (_, byRight $ inP (W,DW,idp), \lam {y} Vy => \case CoverSpaceLocale.cover-point-char U<=W $ <=<-right (single_<= Vy) V<=<U \with {
      | inP (U', inP (W',W'<=W,W'U'), y<=<U') => W'<=W $ inP $ later (U', W'U', y<=<U')
    })
  }
  \where {
    \func sitePoint (x : X) : SitePoint CoverSpaceLocale.site \cowith
      | F U => single x <=< U
      | sitePoint-mono => <=<-left
      | sitePoint-top => inP (top, <=<_top)
      | sitePoint-meet {U} {V} x<=<U x<=<V => inP (U ∧ V, <=<_meet-same x<=<U x<=<V, cover-inj meet-left idp, cover-inj meet-right idp)
      | sitePoint-cover {U} {C} U<=C x<=<U => CoverSpaceLocale.cover-point-char (cover-basic U<=C) x<=<U

    \lemma isDense (Xd : X.HasWeaklyDensePoints) : PrecoverMap.IsWeaklyDense {CoverSpaceLocale-unit Xd}
      => \lam {U} Uo c (F,UF) => \case F.filter-SJoin  $ F.filter-mono filter-top $ <=<_single. $ (PrecoverSpace.open-char {LocaleCoverSpace {CoverSpaceLocale X} CoverSpaceLocale.regular}). Uo UF \with {
        | inP (W,h,FW) => \case filter-Join FW \with {
          | inP (V,p,FV) => \case F.filter-SJoin (transport F element_SJoin FV) \with {
            | inP (V',VV',FV') => F.isProper $ filter-mono FV' $ embed-univ $ cover-trans (inP (,idp)) \lam {W} W<=<V' =>
              CoverSpaceLocale.cover-empty \lam {x} Wx => c (_, inP (x,idp), h (p FV) $ p $ inP $ later (V', VV', <=<-right (single_<= Wx) $ s<=<_<=< W<=<V'))
          }
        }
      }

    \lemma isEmbedding (Xd : X.HasWeaklyDensePoints) : PrecoverMap.IsEmbedding {CoverSpaceLocale-unit Xd}
      => \lam {C} Cc _ => cover-trans (inP (, inP (C, Cc, idp))) $ SetIm-elim \lam {U} CU => cover-refl $ inP $ later
          (_, SetIm-cone (points^* $ embed U) $ inP (U, CU, \lam {x} (inP (V,V<=U,x<=<V)) => \case CoverSpaceLocale.cover-point-char V<=U x<=<V \with {
            | inP (_,idp,x<=<U) => <=<_<= x<=<U idp
          }), cover-refl $ inP (embed U, <=-refl, cover-inj meet-right idp))

    \lemma isDenseEmbedding (Xd : X.HasWeaklyDensePoints) : PrecoverMap.IsWeaklyDenseEmbedding {CoverSpaceLocale-unit Xd}
      => (isDense Xd, isEmbedding Xd)
  }

\func LocaleCompleteCoverSpace {L : Locale} (Lr : L.IsRegularLocale) : StronglyCompleteCoverSpace \cowith
  | StronglyRegularCoverSpace => LocaleCoverSpace Lr
  | isSeparatedCoverSpace {x} {y} sh => exts \lam a =>
      \have | sh1 => separated-char {\this}   sh
            | sh2 => separated-char   $ inv $ separated-char {\this}   sh
      \in ext (\lam xa => \case filter-Join $ filter-mono xa (Lr a) \with {
        | inP (b,b<=<a,xb) => sh1 $ <=<-right (\lam q => rewriteI q xb) $ s<=<_<=< $ points_<=< b<=<a
      }, \lam ya => \case filter-Join $ filter-mono ya (Lr a) \with {
        | inP (b,b<=<a,xb) => sh2 $ <=<-right (\lam q => rewriteI q xb) $ s<=<_<=< $ points_<=< b<=<a
      })
  | isStronglyComplete F => inP (makeFilter F, \lam {V} F<=<V => \case single_<=<-char F<=<V \with {
    | inP (a, inP (b,b<=<a,p), q) => filter-mono (filter-mono p $ points^*-mono $ Topology.Locale.<=<_<= b<=<a) q
  })
  \where {
    \open SeparatedCoverSpace

    \func makeFilter (F : WeaklyCauchyFilter (LocaleCoverSpace Lr)) : CompleteFilter L \cowith
      | F a => ∃ (b : L) (b L.<=< a) (F (points^* b))
      | filter-mono (inP (c,c<=<a,Fc)) a<=b => inP (c, <=<-left c<=<a a<=b, Fc)
      | filter-top => inP (top, <=<_top, rewrite points^*_top filter-top)
      | filter-meet (inP (a',a'<=<a,Fa')) (inP (b',b'<=<b,Fb')) => inP (a' ∧ b', <=<_meet a'<=<a b'<=<b, rewrite points^*_meet $ filter-meet Fa' Fb')
      | filter-Join {C} (inP (b,b<=<C,Fb)) => \case F.isCauchyFilter {\lam U => (U = points^* (L.neg b)) || Given (x : C) (a : L) (a L.<=< x) (U = points^* a)} (b<=<C <=∘ join-univ (points-unit <=∘ SJoin-cond (byLeft idp)) (Join-univ \lam {x} Cx => Lr x <=∘ Join-univ \lam {y} y<=<x => points-unit <=∘ SJoin-cond (byRight $ later (x,Cx,y,y<=<x,idp)))) \with {
        | inP (_, byLeft idp, p) => absurd $ F.isWeaklyProper $ filter-mono (filter-meet p Fb) \lam {x} s => absurd $ x.isProper $ x.filter-mono (x.filter-meet s. s.) Locale.<=-eval
        | inP (_, byRight (d,Cd,a,a<=<d,idp), p) => inP (d, Cd, inP (a,a<=<d,p))
      }
  }