\import Data.Bool
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Order.Lattice
\import Order.PartialOrder
\import Paths
\import Paths.Meta
\import Set.Subset
\import Topology.Locale
\import Topology.PartialCoverSpace
\import Topology.RatherBelow

\func CoverSpaceLocale (X : PrecoverSpace) : Locale
  => PresentedFrame (framePres {X})
  \where {
    \open PresentedFrame

    \func framePres {X : PrecoverSpace} : FramePres (Set X) \cowith
      | conj => ∧
      | BasicCover {J} U f => Given (U = {Set X} top) (C : X.isCauchy) (∀ {V : C} ∃ (j : J) (f j = V)) || (\Pi {V : Set X} -> V s<=< U -> ∃ (j : J) (f j = V)) || (U = {Set X} bottom)

    \lemma cover-cauchy {X : PrecoverSpace} {C : Set (Set X)} (Cc : isCauchy C) : FramePres.SCover {framePres} top C
      => cover-basic $ byLeft (idp, C, Cc, \lam {V} CV => inP ((V,CV), idp))

    \lemma cover-reg {X : PrecoverSpace} {U : Set X} : FramePres.SCover U \lam V => V s<=< U
      => cover-trans (cover-basic {framePres} {U} {\Sigma (V : Set X) (V s<=< U)} $ byRight $ byLeft \lam p => inP ((_, p), idp)) \lam s => cover-inj s idp

    \lemma cover-empty {X : PrecoverSpace} {U : Set X} (Ue : \Pi {x : X} -> Not (U x)) {J : \Set} {g : J -> Set X} : Cover {framePres} U g
      => cover-basic $ byRight $ byRight $ <=-antisymmetric (\lam Ux => absurd $ Ue Ux) bottom-univ

    \lemma embed_<=< {V U : Set X} (V<=<U : V s<=< U) : embed V Locale.<=< {CoverSpaceLocale X} embed U
      => \lam _ => Cover.cover-trans1 Cover.cover_top $ cover-basic $ byLeft
        (idp, _, V<=<U, \case __ \with {
          | byLeft p => inP ((true, _, cover-inj ((embed $ Compl V, rewrite embed_meet $ embed<= $ cover-basic $ byRight $ byRight $ <=-antisymmetric (later \lam (nVx,Vx) => absurd $ nVx Vx) bottom-univ), _, rewrite p $ cover-inj () idp) idp), idp)
          | byRight p => inP ((false, _, rewrite p $ cover-inj () idp), idp)
        })

    \lemma regular : Locale.IsRegularLocale {CoverSpaceLocale X}
      => regular-fromPres \lam U => cover-basic $ byRight $ byLeft $ later \lam {V} V<=<U => inP ((V, embed_<=< V<=<U), idp)

    \lemma cover-char {X : StronglyRegularCoverSpace} {U : Set X} {J : \Set} {g : J -> Set X} (c : Cover {framePres} U g) {U' : Set X} (U'<=<U : U' s<=< U)
      : X.isCauchy \lam V => (V = Compl U') || (\Sigma (j : J) (g j = V)) \elim c
      | cover-basic (byLeft (p,C,Cc,h)) => PrecoverSpace.cauchy-subset Cc \case h __ \with {
        | inP r => byRight r
      }
      | cover-basic (byRight (byLeft h)) => {?}
      {- cauchy-refine (isStronglyRegular U'<=<U) \lam {V'} (inP (V, e, V'<=<V)) => \case \elim e \with {
        | byLeft p => inP (_, byLeft idp, {?})
        | byRight p => inP (V', \case h (rewrite p in V'<=<V) \with {
          | inP s => byRight s
        }, <=-refl)
      } -}
      | cover-basic (byRight (byRight h)) => X.cauchy-refine U'<=<U \lam {W} t => inP (_, byLeft idp, {?}) -- PrecoverSpace.top-cauchy $ byLeft $ <=-antisymmetric (later \lam _ U'x => {?} {- bottom-empty $ s<=<_<= (rewrite h in U'<=<U) U'x -}) top-univ
      | cover-inj j p => PrecoverSpace.cauchy-subset (unfolds in U'<=<U) \case __ \with {
        | byLeft q => byLeft q
        | byRight q => byRight $ later (j, p *> inv q)
      }
      | cover-trans {I} {f} c d =>
        \have t => cauchy-glue (isStronglyRegular $ cover-char c U'<=<U)
          {\lam U1 V1 => U1 s<=< Compl U' || (\Sigma (i : I) (U1 s<=< f i) ((V1 = Compl U1) || (\Sigma (j : J) (g j = V1))))} \case __ \with {
            | inP (W, byLeft e, W'<=<W) => PrecoverSpace.top-cauchy $ byLeft $ rewrite e in W'<=<W
            | inP (W, byRight (i,fi=W), W'<=<W) => PrecoverSpace.cauchy-subset (cover-char (d i) (rewrite (inv fi=W) in W'<=<W)) \lam e => byRight $ later (i, rewrite fi=W W'<=<W, e)
          }
        \in cauchy-refine t \case __ \with {
          | inP (V, W, inP (U, byLeft e, V<=<U), _, Z=VW) => inP (_, byLeft idp, rewrite Z=VW $ meet-left <=∘ {?} {- s<=<_<= V<=<U <=∘ =_<= e -})
          | inP (V, W, inP (U, _, V<=<U), byLeft e2, Z=VW) => inP (_, byLeft idp, rewrite Z=VW $ meet-left <=∘ {?} {- s<=<_<= e2 -})
          | inP (V, W, inP (U, _, V<=<U), byRight (i, V<=<fi, byLeft e), Z=VW) => inP (_, byLeft idp, rewrite (Z=VW,e) \lam (Vx,nVx) => absurd $ nVx Vx)
          | inP (V, W, inP (U, _, V<=<U), byRight (i, V<=<fi, byRight (j,gj=W)), Z=VW) => inP (_, byRight (j,idp), rewrite (Z=VW,gj=W) meet-right)
        }
      | cover-proj1 {U1} {U2} p j q => cauchy-refine U'<=<U \lam {V} => \case __ \with {
        | byLeft r => inP (V, byLeft r, <=-refl)
        | byRight r => inP (U1, byRight (j,q), rewrite (r *> p) meet-left)
      }
      | cover-idemp j p => PrecoverSpace.cauchy-subset (unfolds in U'<=<U) \case __ \with {
        | byLeft r => byLeft r
        | byRight r => byRight $ later (j, p *> MeetSemilattice.meet-idemp *> inv r)
      }
      | cover-comm p j q => PrecoverSpace.cauchy-subset (unfolds in U'<=<U) \case __ \with {
        | byLeft r => byLeft r
        | byRight r => byRight $ later (j, q *> MeetSemilattice.meet-comm *> inv (r *> p))
      }
      | cover-ldistr {W} p c q =>
        \have | t1 => cover-char c (<=<-left U'<=<U $ later $ rewrite p meet-right)
              | t2 : U' s<=< W => <=<-left U'<=<U $ later $ rewrite p meet-left
        \in cauchy-refine (PrecoverSpace.cauchy-inter t1 t2) \case __ \with {
          | inP (V1, V2, byLeft e1, _, r) => inP (_, byLeft idp, rewrite (r,e1) meet-left)
          | inP (V1, V2, _, byLeft e2, r) => inP (_, byLeft idp, rewrite (r,e2) meet-right)
          | inP (_, _, byRight (j,idp), byRight idp, r) => inP (_, byRight (j, idp), rewrite (r, q j) $ =_<= MeetSemilattice.meet-comm)
        }

    \lemma cover-inh {X : PrecoverSpace} (Xd : X.HasDensePoints) {U : Set X} : Cover {framePres} U {\Sigma (x : X) (U x)} \lam _ => U
      => cover-trans cover-reg \lam (V,V<=<U) =>
        cover-trans (cover-ldistr (<=-antisymmetric (meet-univ <=-refl top-univ) meet-left) (cover-cauchy (Xd V<=<U)) \lam _ => idp) \case \elim __ \with {
          | (_, (byLeft idp, inP (x,nVx))) => cover-empty $ later \lam (Vx,nVx) => nVx Vx
          | (_, (byRight idp, inP (x,Ux))) => Cover.cover-inj_<= (x,Ux) __.
        }
  }