{- | We follow the following sources:
     [1] Peter T. Johnstone, Stone Spaces, 1982
     [2] Francis Borceux, Handbook of Categorical Algebra: Volume 3, 1994 (Chapter 1)
     [3] Peter T. Johnstone, A constructive “Closed subgroup theorem” for localic groups and groupoids, 1989
     [4] Peter T. Johnstone, Fibrewise separation axioms for locales, 1990
 -}

\import Algebra.Meta
\import Algebra.Ordered
\import Arith.Nat
\import Category
\import Category.Factorization
\import Category.Functor
\import Category.Limit
\import Category.Meta
\import Category.Subcat
\import Category.Subobj
\import Category.Topos.Sheaf.Site
\import Data.Array
\import Data.Bool
\import Data.Maybe
\import Data.Or
\import Equiv
\import Equiv.Univalence (Equiv-to-=)
\import Function (isSurj)
\import Function.Meta ($, repeat)
\import Homotopy.Fibration
\import Logic
\import Logic.Classical
\import Logic.Meta
\import Meta
\import Order.Lattice
\import Order.LinearOrder \hiding (isDense)
\import Order.PartialOrder
\import Order.StrictOrder
\import Paths
\import Paths.Meta
\import Set
\import Set.Category
\import Set.Fin
\import Topology.RatherBelow
\open Bounded(top,top-univ,bottom,bottom-univ)
\open CompleteLattice(SJoin)
\open MeetSemilattice
\open JoinSemilattice
\open PresentedFrame \hiding (<=)
\open Locale
\open Preorder (=_<=)

\class Locale \extends CompleteLattice, Bounded.DistributiveLattice, SiteWithBasis {
  | join x y => Join (if __ x y)
  | join-left {x} {y} => Join-cond true
  | join-right {x} {y} => Join-cond false
  | join-univ x<=z y<=z => Join-univ \case \elim __ \with {
    | true => x<=z
    | false => y<=z
  }
  | Join-ldistr>= {J : \Set} {f : J -> E} {e : E} : e  Join f <= Join (\lam (j : J) => e  f j)
  | ldistr>= {x} {y} {z} =>
    \have t : (\lam b => if b (x  y) (x  z)) = (\lam b => x  if b y z)
            => ext (\lam b => cases b idp)
    \in unfold (rewrite t Join-ldistr>=)
  | isBasicCover x g => x <= Join (\lam j => (g j).1)
  | basicCover-stable {x} {y} x<=y c => meet-univ <=-refl (x<=y <=∘ c) <=∘ Join-ldistr>=

  | Meet {J} g => Join (\lam (t : Total (\Pi (j : J) -> __ <= g j)) => t.1)
  | Meet-cond {J} j {f} => Join-univ (__.2 j)
  | Meet-univ {J} {f} {e} p => Join-cond (later (e,p))

  \lemma Join-ldistr {J : \Set} {f : J -> E} {e : E} : e  Join f = Join (\lam (j : J) => e  f j)
    => <=-antisymmetric Join-ldistr>= (Join-univ (\lam j => meet-monotone <=-refl (Join-cond j)))

  \lemma Join-rdistr {J : \Set} {f : J -> E} {e : E} : Join f  e = Join (\lam (j : J) => f j  e)
    => meet-comm *> Join-ldistr *> pmap Join (ext (\lam j => meet-comm))

  \lemma Join-rdistr>= {J : \Set} {f : J -> E} {e : E} : Join f  e <= Join (\lam (j : J) => f j  e)
    => =_<= Join-rdistr

  \lemma Join-distr {I J : \Set} {f : I -> E} {g : J -> E} : Join f  Join g = Join (\lam (p : \Sigma I J) => f p.1  g p.2)
    => Join-rdistr *> path (\lam i => Join (\lam i' => Join-ldistr {_} {J} {g} {f i'} @ i)) *> Join-double {_} {I} {J} {\lam i j => f i  g j}

  \lemma Join-distr>= {I J : \Set} {f : I -> E} {g : J -> E} : Join f  Join g <= Join (\lam (p : \Sigma I J) => f p.1  g p.2)
    => =_<= Join-distr

  \type \infix 4 << (x y : E) => \Pi {J : \Set} {g : J -> E} -> y <= Join g ->  (l : Array J) (x <= Join (\lam i => g (l i)))

  \type isCompact => top << top

  \type isLocallyCompact => \Pi (x : E) -> x <= SJoin (`<< x)

  \func \infixr 5 --> (x y : E) => SJoin (__  x <= y)

  \lemma exponent {x y z : E} : x  y <= z <-> x <= y --> z
    => (\lam p => Join-cond (later (x,p)), \lam p => meet-monotone p <=-refl <=∘ eval)

  \lemma exponent_monotone {x y x' y' : E} (p : x' <= x) (q : y <= y') : x --> y <= x' --> y'
    => exponent.1 $ meet-monotone <=-refl p <=∘ eval <=∘ q

  \lemma exponent-double {x y z : E} : x --> y --> z = x  y --> z
    => <=-antisymmetric (exponent.1 $ =_<= (inv meet-assoc) <=∘ meet-monotone eval <=-refl <=∘ eval) (exponent.1 $ exponent.1 $ =_<= meet-assoc <=∘ eval)

  \lemma eval {x y : E} : (x --> y)  x <= y
    => rewrite Join-rdistr (Join-univ __.2)

  \lemma exponent_meet {x y z : E} : x --> y  z = (x --> y)  (x --> z)
    => <=-antisymmetric (meet-univ (exponent_monotone <=-refl meet-left) (exponent_monotone <=-refl meet-right)) (exponent.1 (meet-univ (meet-monotone meet-left <=-refl <=∘ eval) (meet-monotone meet-right <=-refl <=∘ eval)))

  \lemma trueExponent {x y : E} (p : x <= y) : top <= x --> y
    => exponent.1 (meet-right <=∘ p)

  \func neg (x : E) => x --> bottom

  \lemma neg-inverse {x y : E} (p : x <= y) : neg y <= neg x
    => exponent.1 $ meet-monotone <=-refl p <=∘ eval

  -- | The "rather below" relation: `x <=< y` if and only if the closure of {x} is contained in {y}.
  \type \infix 4 <=< (x y : E) => top <= neg x  y

  -- | The "weakly rather below" relation: `x <=<w y` if and only if the weak closure of {x} is contained in {y}.
  \type \infix 4 <=<w (x y : E) => open y <= {NucleusFrame _} FrameHom.wclosed-image {Nucleus.map {open x}}

  \type isRegular => \Pi (x : E) -> x <= SJoin (`<=< x)

  \type isWeaklyRegular => \Pi (x : E) -> x <= SJoin (`<=<w x)

  \func open (a : E) : Nucleus (a --> __) \cowith
    | nucleus-meet => <=-antisymmetric
        (meet-univ (exponent.1 (eval <=∘ meet-left)) (exponent.1 (eval <=∘ meet-right)))
        (exponent.1 (meet-univ (meet-monotone meet-left <=-refl <=∘ eval) (meet-monotone meet-right <=-refl <=∘ eval)))
    | nucleus-unit => exponent.1 meet-left
    | nucleus-join>= => exponent.1 (transport (_  __ <= _) meet-idemp (transport (`<= _) meet-assoc (meet-monotone eval <=-refl <=∘ eval)))

  \lemma open_exp {a : E} (x y : Nucleus.locale {open a}) : (x --> {Nucleus.locale {open a}} y).1 = x.1 --> y.1
    => <=-antisymmetric (Join-univ \lam p => exponent.1 $ exponent.1 (=_<= (meet-assoc *> pmap (_ ) meet-comm *> inv meet-assoc) <=∘ meet-monotone p.2 <=-refl <=∘ Join-rdistr>= <=∘ Join-univ __.2) <=∘ y.2)
                        (Join-univ \lam p => exponent.1 $ exponent.1 (meet-left <=∘ meet-left) <=∘ Join-cond (later ((a --> p.1, nucleus-join>=), exponent.1 (meet-univ (meet-monotone meet-left <=-refl <=∘ eval) (meet-left <=∘ meet-right) <=∘ p.2) <=∘ y.2)))

  \lemma open-isOpen (a : E) : isOpen {Nucleus.map {open a}}
    => \lam x => inP (a  x.1, \lam y => rewrite Nucleus.map_direct $ open_exp x (a --> y, nucleus-join>=) *> exponent-double *> pmap (__ --> y) meet-comm)

  \func closed (a : E) : Nucleus (a  __) \cowith
    | nucleus-meet => equation
    | nucleus-unit => join-right
    | nucleus-join>= => join-univ join-left <=-refl

  \lemma closed-isClosed (a : E) : Nucleus.isClosed {closed a}
    => \lam {x} => join-univ (join-left <=∘ join-left) join-right

  \func pHat (P : \Prop) => Join (\lam (_ : P) => top)

  \lemma pHat-impl {P Q : \Prop} (f : P -> Q) : pHat P <= pHat Q
    => Join-univ (\lam p => Join-cond (f p))

  \func isPositive (a : E) => \Pi (P : \Prop) -> a <= pHat P -> P

  \lemma positive_<= {a b : E} (p : isPositive a) (a<=b : a <= b) : isPositive b
    => \lam g q => p g (a<=b <=∘ q)

  \lemma positive_cover {a : E} (p : isPositive a) {J : \Set} (g : J -> E) (c : a <= Join g) : TruncP J
    => p _ $ c <=∘ Join-univ (\lam j => top-univ <=∘ Join-cond (inP j))

  \lemma positive_Join (o : isOvert) {J : \Set} {f : J -> E} (Jf>0 : isPositive (Join f)) :  (j : J) (isPositive (f j))
    => Jf>0 _ $ Join-univ \lam j => o (f j) <=∘ pHat-impl (\lam fj>0 => inP $ later (j,fj>0))
    \where
      \lemma conv {J : \Set} {f : J -> E} (p :  (j : J) (isPositive (f j))) : isPositive (Join f) \elim p
        | inP (j,fj>0) => \lam P Jf<=P => fj>0 P $ Join-cond j <=∘ Jf<=P

  \func isOvert => \Pi (a : E) -> a <= pHat (isPositive a)

  \lemma overt_cover (o : isOvert) {a : E} : a <= Join (\lam (_ : isPositive a) => a)
    => meet-univ <=-refl (o a) <=∘ Join-ldistr>= <=∘ Join-univ (\lam p => meet-left <=∘ Join-cond {_} {isPositive a} p)

  \func restrict (a : E) : Locale \cowith
    | E => \Sigma (b : E) (b <= a)
    | <= p q => p.1 <= q.1
    | <=-refl => <=-refl
    | <=-transitive => <=∘
    | <=-antisymmetric p q => ext (<=-antisymmetric p q)
    | meet p q => (p.1  q.1, meet-left <=∘ p.2)
    | meet-left => meet-left
    | meet-right => meet-right
    | meet-univ => meet-univ
    | top => (a, <=-refl)
    | top-univ {x} => x.2
    | Join g => (Join (\lam j => (g j).1), Join-univ (\lam j => (g j).2))
    | Join-cond j {_} => Join-cond j
    | Join-univ => Join-univ
    | Join-ldistr>= => Join-ldistr>=
    \where {
      \func map : FrameHom \this (restrict a) \cowith
        | func b => (b  a, meet-right)
        | func-<= => meet-monotone __ <=-refl
        | func-top => ext top-left
        | func-top>= => meet-univ top-univ <=-refl
        | func-meet => ext equation
        | func-meet>= => =_<= equation
        | func-Join => ext Join-rdistr
        | func-Join>= => Join-rdistr>=

      \func functor : Functor (restrict a) \this \cowith
        | F x => x.1
        | Func p => p
        | Func-id => idp
        | Func-o => idp
    }
}

\record FrameHom \extends SetHom {
  \override Dom : Locale
  \override Cod : Locale
  | func-<= {x y : Dom} : x <= y -> func x <= func y
  | func-top : func top = top
  | func-top>= : top <= func top
  | func-meet {x y : Dom} : func (x  y) = func x  func y
  | func-meet>= {x y : Dom} : func x  func y <= func (x  y)
  | func-Join {J : \Set} {f : J -> Dom} : func (Join f) = Join (\lam j => func (f j))
  | func-Join>= {J : \Set} {f : J -> Dom} : func (Join f) <= Join (\lam j => func (f j))

  \default func-Join>= {J} {f} => transport (_ <=) func-Join <=-refl
  \default func-Join \as func-Join-impl {J} {f} => <=-antisymmetric func-Join>= (Join-univ (\lam j => func-<= (Join-cond j)))
  \default func-top>= => transportInv (_ <=) func-top <=-refl
  \default func-top => <=-antisymmetric top-univ func-top>=
  \default func-<= x<=y => rewrite (inv (pmap func (meet_<= x<=y)) *> func-meet) meet-right
  \default func-meet>= => =_<= (inv func-meet)
  \default func-meet => <=-antisymmetric (meet-univ (func-<= meet-left) (func-<= meet-right)) func-meet>=

  \lemma func-join {x y : Dom} : func (x  y) = func x  func y
    => func-Join *> pmap Join (ext (\lam b => cases b idp))

  \lemma func-join>= {x y : Dom} : func (x  y) <= func x  func y
    => =_<= func-join

  \lemma func-bottom : func bottom = bottom
    => func-Join *> pmap Join (ext (\case __))

  \lemma func-bottom>= : func bottom <= bottom
    => =_<= func-bottom

  \lemma func-pHat {P : \Prop} : func (pHat P) = pHat P
    => func-Join *> path (\lam i => Join (\lam _ => func-top i))

  \lemma func-pHat<= {P : \Prop} : pHat P <= func (pHat P)
    => =_<= (inv func-pHat)

  \lemma func-pHat>= {P : \Prop} : func (pHat P) <= pHat P
    => =_<= func-pHat

  \func direct (y : Cod) : Dom => SJoin (func __ <= y)

  \lemma direct-<= {y z : Cod} (p : y <= z) : direct y <= direct z
    => Join-univ \lam (x,q) => Join-cond (later (x, q <=∘ p))

  \lemma direct-unit {x : Dom} : x <= direct (func x)
    => Join-cond $ later (x,<=-refl)

  \lemma direct-counit {y : Cod} : func (direct y) <= y
    => func-Join>= <=∘ Join-univ __.2

  \lemma direct-adjoint {x : Dom} {y : Cod} : func x <= y <-> x <= direct y
    => (direct-unit <=∘ direct-<= __, func-<= __ <=∘ direct-counit)

  \lemma direct-meet {y z : Cod} : direct (y  z) = direct y  direct z
    => <=-antisymmetric (meet-univ (direct-<= meet-left) (direct-<= meet-right)) (Join-cond (later (direct y  direct z, meet-univ (direct-adjoint.2 meet-left) (direct-adjoint.2 meet-right))))

  \lemma direct-top : direct top = top
    => <=-antisymmetric top-univ (Join-cond (later (top, top-univ)))

  \lemma func_direct_func {x : Dom} : func (direct (func x)) = func x
    => <=-antisymmetric direct-counit (func-<= direct-unit)

  \func image : Nucleus (\lam x => direct (func x)) \cowith
    | nucleus-meet => pmap direct func-meet *> direct-meet
    | nucleus-unit => direct-unit
    | nucleus-join>= => direct-<= direct-counit

  \func factor : FrameHom image.locale Cod \cowith
    | func x => func x.1
    | func-top => func-top
    | func-meet => func-meet
    | func-Join>= => direct-counit <=∘ func-Join>=

  -- | A map is dense if and only if its image is dense.
  \func isDense => \Pi {x : Dom} -> func x <= bottom -> x <= bottom

  \lemma dense_direct (d : isDense) : direct bottom <= bottom
    => Join-univ (\lam j => d j.2)

  \lemma direct_dense (d : direct bottom <= bottom) : isDense
    => \lam {x} p => Join-cond (later (x,p)) <=∘ d

  \type isStronglyDense => \Pi {P : \Prop} {x : Dom} -> func x <= pHat P -> x <= pHat P

  \func isWeaklyClosed => \Sigma (isSurj func) (\Pi (j : Nucleus) ->
      (\Pi {P : \Prop} {x : Dom} -> func x <= pHat P -> x <= j (pHat P)) -> \Pi {x : Dom} -> direct (func x) <= j x)

  -- | The weak closure of the image
  \func wclosed-image : Nucleus \cowith
    | nucleus x => Meet \lam (j : \Sigma (j : Nucleus) (\Pi {P : \Prop} {x : Dom} -> func x <= pHat P -> x <= j (pHat P))) => j.1 x
    | nucleus-<= p => Meet-univ \lam j => Meet-cond j <=∘ nucleus-<= p
    | nucleus-meet>= => Meet-univ \lam j => meet-monotone (Meet-cond j) (Meet-cond j) <=∘ nucleus-meet>=
    | nucleus-unit {x} => Join-cond $ later (x, \lam j => nucleus-unit)
    | nucleus-join>= => Meet-univ \lam j => Meet-cond j <=∘ nucleus-<= (Meet-cond j) <=∘ nucleus-join>=

  \func wclosed-factor : FrameHom wclosed-image.locale Cod \cowith
    | func x => func x.1
    | func-top => func-top
    | func-meet => func-meet
    | func-Join>= => direct-adjoint.2 (Meet-cond $ later (image, \lam hx<=P => direct-adjoint.1 (hx<=P <=∘ func-pHat<=))) <=∘ func-Join>=

  \lemma wclosed-factor-sdense : wclosed-factor.isStronglyDense
    => \lam c => Meet-univ (\lam j => j.2 c)

  -- | A map is closed if and only if the image of a closed sublocale is closed.
  \func isClosed => \Pi {x : Cod} {y : Dom} -> direct (x  func y) <= direct x  y

  -- | The image of a closed map is closed.
  \lemma image_closed (c : isClosed) : image.isClosed
    => \lam {y} => direct-<= join-right <=∘ c <=∘ join-monotone (direct-<= bottom-univ) <=-refl

  -- | If the image of an embedding is closed, then it is a closed map.
  \lemma closed-embedding_image (s : isSurj func) (c : image.isClosed) : isClosed
    => \lam {x} {y} => \case s x \with {
      | inP (a,p) => rewriteI (p,func-join) (c <=∘ join-univ (direct-<= (func-<= bottom-univ) <=∘ join-left) (join-monotone direct-unit <=-refl))
    }

  -- | A map is open if and only if the image of an open sublocale is open.
  \func isOpen => \Pi (x : Cod) ->  (z : Dom)  y (direct (x --> func y) = z --> y)

  \lemma surjective-split (s : isSurj func) (x : Cod) : func (direct x) = x
    => \case s x \with {
      | inP (y,p) => rewriteI p func_direct_func
    }

  \lemma surj_nucleus (s : isSurj func) : Equiv factor => \new QEquiv {
    | ret y => (direct y, direct-<= direct-counit)
    | ret_f x => ext (<=-antisymmetric x.2 direct-unit)
    | f_sec y => surjective-split s y
  }

  \func functor : Functor Dom Cod \cowith
    | F => func
    | Func => func-<=
    | Func-id => idp
    | Func-o => idp
} \where {
  \lemma direct_o {L M K : Locale} (f : FrameHom L M) (g : FrameHom M K) {x : K} : direct {g FrameCat. f} x = f.direct (g.direct x)
    => <=-antisymmetric (direct-adjoint.1 $ direct-adjoint.1 $ direct-counit {g FrameCat. f}) ((direct-adjoint {g FrameCat. f}).1 $ func-<= direct-counit <=∘ direct-counit)
}

-- | Nuclei encode sublocales
\record Nucleus {L : Locale} (\coerce nucleus : L -> L) {
  | nucleus-meet {x y : L} : nucleus (x  y) = nucleus x  nucleus y
  | nucleus-meet>= {x y : L} : nucleus x  nucleus y <= nucleus (x  y)
  | nucleus-<= {x y : L} : x <= y -> nucleus x <= nucleus y
  | nucleus-unit {x : L} : x <= nucleus x
  | nucleus-join>= {x : L} : nucleus (nucleus x) <= nucleus x
  | nucleus-join {x : L} : nucleus (nucleus x) = nucleus x

  \default nucleus-<= p => rewrite (inv (pmap nucleus (meet_<= p)) *> nucleus-meet) meet-right
  \default nucleus-meet => <=-antisymmetric (meet-univ (nucleus-<= meet-left) (nucleus-<= meet-right)) nucleus-meet>=
  \default nucleus-meet>= => =_<= (inv nucleus-meet)
  \default nucleus-join => <=-antisymmetric nucleus-join>= nucleus-unit
  \default nucleus-join>= => =_<= nucleus-join

  \lemma nucleus-univ {x y : L} (p : x <= nucleus y) : nucleus x <= nucleus y
    => nucleus-<= p <=∘ nucleus-join>=

  \lemma nucleus_exponent {x y : L} (p : nucleus y <= y) : nucleus (x --> y) <= x --> y
    => exponent.1 $ meet-monotone <=-refl nucleus-unit <=∘ nucleus-meet>= <=∘ nucleus-<= eval <=∘ p

  \lemma exponent-func {x y : L} : x --> y <= nucleus x --> nucleus y
    => Join-univ \lam p => exponent.1 $ meet-monotone nucleus-unit <=-refl <=∘ nucleus-meet>= <=∘ nucleus-<= p.2

  \type Subtype => \Sigma (x : L) (nucleus x <= x)

  \instance locale : Locale Subtype
    | <= (x,_) (y,_) => x <= y
    | <=-refl => <=-refl
    | <=-transitive => <=-transitive
    | <=-antisymmetric p q => ext (<=-antisymmetric p q)
    | meet (x,p) (y,q) => (x  y, rewrite nucleus-meet (meet-monotone p q))
    | meet-left => meet-left
    | meet-right => meet-right
    | meet-univ => meet-univ
    | top => (top, top-univ)
    | top-univ => top-univ
    | Join f => (nucleus (Join (f __).1), nucleus-join>=)
    | Join-cond j {f} => Join-cond j <=∘ nucleus-unit
    | Join-univ {J} {f} {e} h => nucleus-<= (Join-univ h) <=∘ e.2
    | Join-ldistr>= {J} {f} {e} => meet-monotone nucleus-unit <=-refl <=∘ transport (`<= _) nucleus-meet (nucleus-<= Join-ldistr>=)

  \func map : FrameHom L locale \cowith
    | func x => (nucleus x, nucleus-join>=)
    | func-top => ext (<=-antisymmetric top-univ nucleus-unit)
    | func-meet => ext nucleus-meet
    | func-Join>= => nucleus-<= $ Join-univ \lam j => nucleus-unit <=∘ Join-cond j
    \where {
      \lemma surjective : isSurj map
        => \lam y => inP (y.1, ext $ <=-antisymmetric y.2 nucleus-unit)
    }

  \func functor : Functor locale L \cowith
    | F x => x.1
    | Func p => p
    | Func-id => idp
    | Func-o => idp

  \lemma map_direct (x : locale) : map.direct x = x.1
    => <=-antisymmetric (Join-univ (\lam j => nucleus-unit <=∘ j.2)) (Join-cond (later (x.1, x.2)))

  \func isClosed => \Pi {x : L} -> nucleus x <= nucleus bottom  x

  \func isDense => nucleus bottom <= bottom
}

-- | The order of nuclei is inversed. That is, `n <= m` iff `m.locale` is a sublocale of `n.locale`.
\instance NucleusFrame (L : Locale) : Locale (Nucleus {L})
  | <= j j' => \Pi {x : L} -> j x <= j' x
  | <=-refl => <=-refl
  | <=-transitive p q {x} => <=-transitive p q
  | <=-antisymmetric p q => exts (\lam x => <=-antisymmetric p q)
  | meet (j j' : Nucleus {L}) : Nucleus => \new Nucleus {
    | nucleus x => j x  j' x
    | nucleus-meet => rewrite (nucleus-meet {j}) $ rewrite (nucleus-meet {j'}) equation
    | nucleus-unit => meet-univ nucleus-unit nucleus-unit
    | nucleus-join>= => meet-monotone (Nucleus.nucleus-univ meet-left) (Nucleus.nucleus-univ meet-right)
  }
  | meet-left => meet-left
  | meet-right => meet-right
  | meet-univ p q {x} => meet-univ p q
  | top => \new Nucleus {
    | nucleus _ => top
    | nucleus-meet>= => top-univ
    | nucleus-<= _ => <=-refl
    | nucleus-unit => top-univ
    | nucleus-join>= => <=-refl
  }
  | top-univ => top-univ
  | Join {J} g => \new Nucleus {
    | nucleus x => Meet \lam (p : \Sigma (n : Nucleus) (\Pi (j : J) {x : L} -> g j x <= n x)) => p.1 x
    | nucleus-meet>= => Meet-univ \lam p => meet-univ (meet-left <=∘ Meet-cond p) (meet-right <=∘ Meet-cond p) <=∘ nucleus-meet>=
    | nucleus-<= x<=y => Meet-univ \lam p => Meet-cond p <=∘ nucleus-<= x<=y
    | nucleus-unit => Meet-univ \lam p => nucleus-unit
    | nucleus-join>= => Meet-univ \lam p => Meet-cond p <=∘ Nucleus.nucleus-univ (Meet-cond p)
  }
  | Join-cond j {g} {x} => Join-cond $ later (g j x, \lam p => p.2 j)
  | Join-univ c {x} => Join-univ \lam p => p.2 (_,c)
  | Join-ldistr>= {J} {g} {k} {x} => Join-ldistr>= <=∘ Join-univ (\lam p => Meet-univ \lam q => =_<= meet-comm <=∘ exp-univ2 (p.2 (exp k q.1, \lam j => exp-univ1 \lam {y} => =_<= meet-comm <=∘ q.2 j)))
  \where {
    \open Topology.Locale(NucleusFrame)

    \func exp {L : Locale} (j j' : Nucleus {L}) : Nucleus \cowith
      | nucleus x => Meet \lam (p : \Sigma (y : L) (x <= y)) => j p.1 --> j' p.1
      | nucleus-meet>= {a} {b} =>
        \have lem {x y z : L} : (x  y)  z = (x  z)  (y  z) => equation
        \in Meet-univ \lam p => meet-monotone (Meet-cond $ later (a  p.1, join-left)) (Meet-cond $ later (b  p.1, join-left)) <=∘
          exponent.1 (=_<= lem <=∘ meet-monotone (meet-monotone <=-refl (nucleus-<= join-right) <=∘ eval) (meet-monotone <=-refl (nucleus-<= join-right) <=∘ eval) <=∘
            nucleus-meet>= <=∘ nucleus-<= (ldistr>= <=∘ join-univ (L.rdistr>= <=∘ join-univ p.2 meet-left) meet-right))
      | nucleus-<= x<=y => Meet-univ \lam p => Meet-cond (later (p.1, x<=y <=∘ p.2)) <=∘ exponent.1 eval
      | nucleus-unit => Meet-univ \lam p => exponent.1 $ meet-left <=∘ p.2 <=∘ nucleus-unit
      | nucleus-join>= => Meet-univ \lam p => Meet-cond (later (j p.1 --> j' p.1, Meet-cond p)) <=∘ exponent_monotone <=-refl (Nucleus.nucleus_exponent nucleus-join>=) <=∘
          =_<= exponent-double <=∘ exponent_monotone (meet-univ (nucleus-<= $ exponent.1 $ meet-left <=∘ nucleus-unit) <=-refl) <=-refl

    \lemma exp-univ1 {L : Locale} {j k n : Nucleus {L}} (p : \Pi {x : L} -> meet j k x <= n x) {x : L} : j x <= exp k n x
      => Meet-univ \lam q => exponent.1 $ meet-monotone (nucleus-<= q.2) <=-refl <=∘ p

    \lemma exp-univ2 {L : Locale} {k n : Nucleus {L}} {x y : L} (p : y <= exp k n x) : y  k x <= n x
      => exponent.2 $ p <=∘ Meet-cond (later (x,<=-refl))

    \func <=-map {L : Locale} (j j' : Nucleus {L}) (j<=j' : j <= j') : FrameHom j.locale j'.locale \cowith
      | func x => (j' x.1, nucleus-join>=)
      | func-<= => nucleus-<=
      | func-top>= => nucleus-unit
      | func-meet>= => nucleus-meet>=
      | func-Join>= => unfold $ nucleus-<= j<=j' <=∘ nucleus-join>= <=∘ nucleus-<= (Join-univ (\lam j => nucleus-unit <=∘ Join-cond j))
      \where
        \lemma surjective {L : Locale} {j j' : Nucleus {L}} (j<=j' : j <= j') : isSurj (<=-map j j' j<=j')
          => \lam y => inP ((y.1, j<=j' <=∘ y.2), ext $ <=-antisymmetric y.2 nucleus-unit)

    \lemma double-nucleus-left {L : Locale} {j k : Nucleus {L}} (j<=k : j <= k) (x : L) : k (j x) = k x
      => <=-antisymmetric (k.nucleus-univ j<=k) (nucleus-<= nucleus-unit)

    \lemma double-nucleus-right {L : Locale} {j k : Nucleus {L}} (j<=k : j <= k) (x : L) : j (k x) = k x
      => <=-antisymmetric (j<=k <=∘ nucleus-join>=) nucleus-unit

    \lemma wclosure_<= {j : Nucleus {}} : j.map.wclosed-image <= {NucleusFrame _} j
      => \lam {x} => Meet-cond $ later (j, nucleus-unit <=∘ __)

    \lemma wclosure-sdense {j : Nucleus {}} : isStronglyDense {<=-map j.map.wclosed-image j wclosure_<=}
      => \lam c => Meet-univ (\lam p => p.2 c)

    \lemma wclosure-inclusion {j : Nucleus {}} (x : j.L) : <=-map j.map.wclosed-image j wclosure_<= (j.map.wclosed-image.map x) = j.map x
      => ext $ double-nucleus-left {j.L} wclosure_<= x

    \lemma nucleus>=open {L : Locale} {a : L} {j : Nucleus {L}} (c : top <= j a) : open a <= j
      => \lam {x} => j.exponent-func <=∘ meet-univ <=-refl (top-univ <=∘ c) <=∘ eval
      \where
        \lemma conv {L : Locale} {a : L} {j : Nucleus {L}} (c : open a <= j) : top <= j a
          => exponent.1 meet-right <=∘ c

    \lemma open_<= {L : Locale} {a b : L} (p : a <= b) : open b <= open a
      => \lam {x} => exponent_monotone p <=-refl
      \where
        \lemma conv {L : Locale} {a b : L} (p : open b <= open a) : a <= b
          => meet-univ top-univ <=-refl <=∘ exponent.2 (nucleus>=open.conv p)

    -- | The intersection of two sublocales is a pullback.
    \sfunc intersection-pullback {L : Locale} (j k : Nucleus {L}) : Pullback {LocaleCat} j.map k.map (Nucleus.locale {j  k})
        (<=-map j (j  k) (join-left {NucleusFrame L})) (<=-map k (j  k) (join-right {NucleusFrame L}))
      => \have coh : j.map  {LocaleCat} <=-map j (j  k) (join-left {_} {j}) = k.map  {LocaleCat} <=-map k (j  k) (join-right {_} {j})
           => exts \lam x => ext $ double-nucleus-left {_} {j} {j  k} (join-left {_} {j} {k}) x *> inv (double-nucleus-left {_} {k} {j  k} (join-right {_} {j} {k}) x)
         \in regularSubobj_meet-pullback.exact {LocaleCat} j.map (surj_regular $ Nucleus.map.surjective {j}) k.map (surj_regular $ Nucleus.map.surjective {k}) {<=-map j (j  k) (join-left {NucleusFrame L})} coh
              (surj_regular {_} {_} {j.map  {LocaleCat} <=-map j (j  k) (join-left {_} {j})} (isSurj.comp Nucleus.map.surjective (<=-map.surjective (join-left {_} {j}))))
              (inP (_, idp), inP (_, inv coh), \case \elim __ \with {
                | regSubobj {sub} (f : FrameHom) fm => \lam (inP (h1,jh1=f)) (inP (h2,kh2=f)) =>
                    \have jk<=f : j  k <= f.image => join-univ
                            (\lam {x} => direct-adjoint.1 $ transport (\lam (f : FrameHom L sub) => f (j x) <= f x) jh1=f $ func-<= nucleus-join>=)
                            (\lam {x} => direct-adjoint.1 $ transport (\lam (f : FrameHom L sub) => f (k x) <= f x) kh2=f $ func-<= nucleus-join>=)
                    \in inP (<=-map (j  k) f.image jk<=f  f.factor, exts \lam x =>
                          func_direct_func *> pmap f (double-nucleus-left {_} {j} {j  k} (join-left {_} {j}) x) *> <=-antisymmetric (direct-adjoint.2 jk<=f) (func-<= $ nucleus-unit {j  k}))
              })
  }

\lemma closed>=open {L : Locale} {c a : L} (p : top <= c  a) : closed c >= open a
  => \lam {x} => meet-univ <=-refl (top-univ <=∘ p) <=∘ ldistr>= <=∘ join-monotone meet-right eval
  \where
    \lemma conv {L : Locale} {c a : L} (p : closed c >= open a) : top <= c  a
      => trueExponent <=-refl <=∘ p

\lemma open<=closed {L : Locale} {c a : L} (p : c  a <= bottom) : open a >= closed c
  => \lam {x} => unfold (join-univ (exponent.1 (p <=∘ bottom-univ)) (exponent.1 meet-left))
  \where
    \lemma conv {L : Locale} {c a : L} (p : open a >= closed c) : c  a <= bottom
      => meet-monotone join-left <=-refl <=∘ exponent.2 p

-- | A closed and "bounded" sublocale is compact.
\lemma closed-compact {L : Locale} {N : Nucleus {L}} (c : N.isClosed) {a : L} (w : a << top) (b : N >= open a) : N.locale.isCompact
  => \lam {J} {g} top<=g =>
      \let | g' (j : Maybe J) : L => \case \elim j \with { | nothing => N bottom | just j => (g j).1 }
           | top<=g' : top <= Join g' => top<=g <=∘ c <=∘ join-univ (Join-cond nothing) (Join-univ (\lam j => Join-cond (just j)))
           | (inP (l,a<=g'l)) => w top<=g'
      \in inP (filterMap (\lam x => x) l, unfold $ trueExponent a<=g'l <=∘ b <=∘ Nucleus.nucleus-univ (Join-univ \lam j' => later $ cases (l j' arg addPath) \with {
        | nothing, _ => Nucleus.nucleus-<= bottom-univ
        | just j, p => \have (k,q) => filterMap-index (\lam x => x) l p
                       \in rewriteI q (Join-cond k) <=∘ nucleus-unit
      }))

\func FrameCat : Cat Locale \cowith
  | Hom => FrameHom
  | id L => \new FrameHom {
    | func x => x
    | func-top => idp
    | func-meet => idp
    | func-Join => idp
  }
  | o {L M K : Locale} (g : FrameHom M K) (f : FrameHom L M) : FrameHom L K => \new FrameHom {
    | func x => g (f x)
    | func-top => pmap g func-top *> func-top
    | func-meet {x} {y} => pmap g func-meet *> func-meet
    | func-Join {J} {h} => pmap g func-Join *> func-Join
  }
  | id-left => idp
  | id-right => idp
  | o-assoc => idp
  | univalence => sip \lam {X} {S1} {S2} (h1 : FrameHom) (h2 : FrameHom) => exts Locale {
    | <= x y => ext (h1.func-<=, h2.func-<=)
    | meet x y => h1.func-meet
    | top => h1.func-top
    | Join f => h1.func-Join
  }
  \where {
    \func equiv_iso {f : FrameHom} (e : Equiv f) : Iso {FrameCat} f \cowith
      | hinv => \new FrameHom {
        | func => e.ret
        | func-top => pmap e.ret (inv func-top) *> e.ret_f top
        | func-meet {x} {y} => pmap e.ret (inv (func-meet *> pmap2 () (e.f_ret x) (e.f_ret y))) *> e.ret_f _
        | func-Join {J} {g} => pmap e.ret (inv (func-Join *> path (\lam i => Join (\lam j => e.f_ret (g j) i)))) *> e.ret_f _
      }
      | hinv_f => exts e.ret_f
      | f_hinv => exts e.f_ret
  }

{- | Presentation of frames.
 -   {conj} represents meets and {BasicCover} represents relation `__ <= Join __`.
 -}
\class FramePres \extends BaseSet {
  | conj : E -> E -> E
  | BasicCover {J : \Set} : E -> (J -> E) -> \Prop

  \type \infix 4 << (x y : E) => \Pi {J : \Set} {g : J -> E} -> Cover y g ->  (l : Array J) (Cover x (\lam i => g (l i)))

  \func SCover (x : E) (U : E -> \Prop) => Cover x (\lam (t : \Sigma (x : E) (U x)) => t.1)

  \type isLocallyCompact => \Pi (x : E) -> SCover x (`<< x)

  \func isPositive (a : E) => \Pi {J : \Set} (g : J -> E) -> Cover a g -> TruncP J

  \func isOvert => \Pi (a : E) -> Cover a (\lam (_ : isPositive a) => a)
} \where {
  \type Indexing {I X : \Set} (h : I -> \Sigma (J : \Set) X (J -> X)) {J : \Set} (e : X) (g : J -> X)
    =>  (i : I) (p : Equiv {(h i).1} {J}) ((h i).2 = e) (\Pi (j : (h i).1) -> (h i).3 j = g (p j))

  \lemma indexing-make {I X : \Set} {h : I -> \Sigma (J : \Set) X (J -> X)} (i : I) : Indexing h (h i).2 (h i).3
    => inP (i, idEquiv, idp, \lam j => idp)

  \lemma indexing-transport {I X : \Set} {g : I -> \Sigma (J : \Set) X (J -> X)}
                            (P : \Pi {J : \Set} (e : X) (f : J -> X) -> \Prop)
                            (p : \Pi (i : I) -> P (g i).2 (g i).3)
                            {J : \Set} {e : X} {f : J -> X} (b : Indexing g e f) : P e f \elim b
    | inP (i,q,s,t) =>
      \have r : ((g i).1, (g i).3) = {\Sigma (K : \Set) (K -> X)} (J,f) => exts (Equiv-to-= q, t)
      \in coe (\lam i => P {(r @ i).1} (s @ i) (r @ i).2) (p i) right
}

\truncated \data Cover {P : FramePres} (x : P) {J : \Set} (g : J -> P) : \Prop
  | cover-basic (BasicCover x g)
  | cover-inj (j : J) (g j = x)
  | cover-trans {I : \Set} {f : I -> P} (Cover x f) (\Pi (i : I) -> Cover (f i) g)
  | cover-proj1 {a b : P} (x = conj a b) (j : J) (g j = a)
  | cover-idemp (j : J) (g j = conj x x)
  | cover-comm {a b : P} (x = conj a b) (j : J) (g j = conj b a)
  | cover-ldistr {a b : P} (x = conj a b) {f : J -> P} (Cover b f) (\Pi (j : J) -> g j = conj a (f j))
  \where {
    \lemma cover-trans1 {P : FramePres} {x : P} {J : \Set} {g : J -> P} {y : P} (c : Cover1 x y) (d : Cover y g) : Cover x g
      => cover-trans c (\lam _ => d)

    \lemma cover-proj2 {P : FramePres} {x : P} {J : \Set} {g : J -> P} {a b : P} (p : x = conj a b) (j : J) (q : g j = b) : Cover x g
      => cover-trans (cover-comm {_} {_} {\Sigma} {\lam _ => conj b a} p () idp) (\lam _ => cover-proj1 idp j q)

    \lemma cover-index {P : FramePres} {x : P} {l : Array P} (i : Index x l) : Cover x l
      => cover-inj i.1 i.2

    \lemma cover-ldistr' {P : FramePres} {x : P} {J : \Set} {g : J -> P} {a b : P} (x=ab : x = conj a b) {I : \Set} {h : I -> P} (ah : Cover b h) (f : \Pi (i : I) ->  (j : J) (g j = conj a (h i))) : Cover x g
      => cover-trans (cover-ldistr {_} {_} {I} {\lam i => conj a (h i)} x=ab ah (\lam j => idp)) \lam i => \case f i \with {
        | inP (j,p) => cover-inj j p
      }

    \lemma cover-rdistr' {P : FramePres} {x : P} {J : \Set} {g : J -> P} {a b : P} (x=ab : x = conj a b) {I : \Set} {h : I -> P} (ah : Cover a h) (f : \Pi (i : I) ->  (j : J) (g j = conj (h i) b)) : Cover x g
      => \have t => cover-trans {P} {_} {I} {\lam j => conj b (h j)} (cover-comm {P} {x} {\Sigma} {\lam _ => conj b a} x=ab () idp) \lam _ => cover-ldistr' idp ah (\lam j => inP (j,idp))
         \in cover-trans t \lam j => \case f j \with {
           | inP (i,p) => cover-comm idp i p
         }

    \lemma cover-rdistr {P : FramePres} {x : P} {J : \Set} {g : J -> P} {a b : P} (x=ab : x = conj a b) {h : J -> P} (ah : Cover a h) (f : \Pi (j : J) -> g j = conj (h j) b) : Cover x g
      => cover-rdistr' x=ab ah (\lam j => inP (j, f j))

    \lemma cover-conj {P : FramePres} {J : \Set} {g : J -> P} {a b : P} {I1 : \Set} {h1 : I1 -> P} (aV : Cover a h1) {I2 : \Set} {h2 : I2 -> P} (bW : Cover b h2) (f : \Pi {i1 : I1} {i2 : I2} ->  (j : J) (g j = conj (h1 i1) (h2 i2))) : Cover (conj a b) g
      => cover-trans {P} {_} {J} {g} {_} {\lam i => conj a (h2 i)} (cover-ldistr' idp bW (\lam i => inP (i, idp))) (\lam i2 => cover-rdistr' idp aV (\lam i1 => f))

    \lemma cover-conj1 {P : FramePres} {a a' b b' : P} (c : Cover1 a a') (d : Cover1 b b') : Cover1 (conj a b) (conj a' b')
      => cover-conj c d (\lam {_} {_} => inP ((), idp))

    \lemma cover-prod {P : FramePres} {x y z : P} (c : Cover1 x y) (d : Cover1 x z) : Cover1 x (conj y z)
      => cover-trans (cover-idemp {_} {_} {_} {\lam _ => conj x x} () idp) \lam _ => cover-conj c d (\lam {i1} {i2} => inP ((),idp))

    \lemma map {F : FramePresPrehom} {x : F.Dom} {J : \Set} {g : J -> F.Dom} (c : Cover x g) : Cover (F x) (\lam j => F (g j)) \elim c
      | cover-basic b => cover-basic (func-cover b)
      | cover-inj j p => cover-inj j (pmap F p)
      | cover-trans c g => cover-trans (map c) (\lam i => map (g i))
      | cover-proj1 p j q => cover-proj1 (pmap F p *> func-conj) j (pmap F q)
      | cover-idemp j p => cover-idemp j (pmap F p *> func-conj)
      | cover-comm p j q => cover-comm (pmap F p *> func-conj) j (pmap F q *> func-conj)
      | cover-ldistr p c f => cover-ldistr (pmap F p *> func-conj) (map c) (\lam j => pmap F (f j) *> func-conj)

    \lemma cover_top {L : Bounded.MeetSemilattice} {P : FramePres L ()} {x : L} : Cover1 x L.top
      => transport (Cover1 __ _) Bounded.MeetSemilattice.top-left $ cover-proj1 idp () idp

    \lemma cover_<= {L : MeetSemilattice} {P : FramePres L ()} {x y : L} (p : x <= y) : Cover1 x y
      => rewriteI (L.meet_<= p) $ cover-proj2 idp () idp

    \lemma cover-inj_<= {L : MeetSemilattice} {P : FramePres L ()} {x : L} {J : \Set} {g : J -> P} (j : J) (p : x <= g j) : Cover x g
      => cover-trans1 (cover_<= p) (cover-inj j idp)
  }

\func Cover1 {P : FramePres} (x y : P) => Cover x {\Sigma} (\lam _ => y)

\truncated \data Cover' {P : FramePres} (x : P) {J : \Set} (g : J -> P) : \Prop
  | cover-basic' {a b : P} (x = conj a b) {f : J -> P} (BasicCover b f) (\Pi (j : J) -> g j = conj a (f j))
  | cover-inj' (j : J) (g j = x)
  | cover-trans' {I : \Set} {f : I -> P} (Cover' x f) (\Pi (i : I) -> Cover' (f i) g)
  | cover-proj1-inj' {a b : P} (x = conj a b) (j : J) (g j = a)
  | cover-proj2-inj' {a b : P} (x = conj a b) (j : J) (g j = b)
  | cover-prod-inj' {a b : P} (Cover' x {\Sigma} (\lam _ => a)) (Cover' x {\Sigma} (\lam _ => b)) (j : J) (g j = conj a b)
  \where {
    \func Cover1' {P : FramePres} (x y : P) => Cover' x {\Sigma} (\lam _ => y)

    \lemma cover-prod' {P : FramePres} {x y z : P} (c : Cover1' x y) (d : Cover1' x z) : Cover1' x (conj y z)
      => cover-prod-inj' c d () idp

    \lemma cover-proj1' {P : FramePres} {x y : P} : Cover1' (conj x y) x
      => cover-proj1-inj' idp () idp

    \lemma cover-proj2' {P : FramePres} {x y : P} : Cover1' (conj x y) y
      => cover-proj2-inj' idp () idp

    \lemma cover-ldistr' {P : FramePres} {J : \Set} {g : J -> P} {a b : P} {f : J -> P} (c : Cover b f) (q : \Pi (j : J) -> g j = conj a (f j)) : Cover' (conj a b) g \elim c
      | cover-basic c => cover-basic' idp c q
      | cover-inj j idp => cover-inj' j (q j)
      | cover-trans c d => cover-trans' (cover-ldistr' c (\lam j => idp)) (\lam i => cover-ldistr' (d i) q)
      | cover-proj1 p j s => cover-prod-inj' cover-proj1' (cover-trans' cover-proj2' \lam _ => cover-proj1-inj' p () s) j (q j)
      | cover-idemp j p => cover-prod-inj' cover-proj1' (cover-prod' cover-proj2' cover-proj2') j (q j *> pmap (conj a) p)
      | cover-comm idp j p => cover-prod-inj' cover-proj1' (cover-trans' cover-proj2' \lam _ => cover-prod' cover-proj2' cover-proj1') j (q j *> pmap (conj a) p)
      | cover-ldistr idp c p => cover-trans' (cover-prod' (cover-prod' cover-proj1' (cover-trans' cover-proj2' \lam _ => cover-proj1')) (cover-trans' cover-proj2' \lam _ => cover-proj2'))
          \lam _ => cover-trans' (cover-ldistr' c (\lam j => idp)) \lam j => cover-prod-inj' (cover-trans' cover-proj1' (\lam _ => cover-proj1')) (cover-prod' (cover-trans' cover-proj1' (\lam _ => cover-proj2')) cover-proj2') j (q j *> pmap (conj a) (p j))

    \lemma cover-cover' {P : FramePres} {x : P} {J : \Set} {g : J -> P} (c : Cover x g) : Cover' x g
      => cover-trans' (cover-prod' (cover-inj' () idp) (cover-inj' () idp))
          \lam _ => cover-trans' (cover-ldistr' c (\lam j => idp)) \lam j => cover-proj2-inj' idp j idp

    \lemma cover'-cover {P : FramePres} {x : P} {J : \Set} {g : J -> P} (c : Cover' x g) : Cover x g \elim c
      | cover-basic' p b q => cover-ldistr p (cover-basic b) q
      | cover-inj' j p => cover-inj j p
      | cover-trans' c d => cover-trans (cover'-cover c) \lam i => cover'-cover (d i)
      | cover-proj1-inj' p j q => cover-proj1 p j q
      | cover-proj2-inj' p j q => Cover.cover-proj2 p j q
      | cover-prod-inj' c1 c2 j p => cover-trans (Cover.cover-prod (cover'-cover c1) (cover'-cover c2)) (\lam _ => cover-inj j p)
  }

\func framePresPreorder (P : FramePres) : Preorder P \cowith
  | <= => Cover1
  | <=-refl => cover-inj () idp
  | <=-transitive p q => cover-trans p (\lam _ => q)

\func framePresSite (P : FramePres) : SiteWithBasis \cowith
  | Precat => framePresPreorder P
  | pullback {x y z : P} (f : Cover1 x z) (g : Cover1 y z) => \new Pullback {framePresPreorder P} f g {
    | apex => conj x y
    | pbProj1 => cover-proj1 idp () idp
    | pbProj2 => cover-proj2 idp () idp
    | pbCoh => prop-pi
    | pbMap p1 p2 _ => cover-prod p1 p2
    | pbBeta1 => prop-pi
    | pbBeta2 => prop-pi
    | pbEta _ _ => prop-pi
  }
  | isBasicCover x {J} g =>  (y : P) (Cover1 x y) (g' : J -> P) (BasicCover y g') (\Pi (j : J) -> \Sigma (Cover1 (g j).1 (g' j)) (Cover1 (conj x (g' j)) (g j).1))
  | basicCover-stable {x} {y} x<=y {J} {g} (inP (z,y<=z,g',c,d)) => inP (z, cover-trans x<=y (\lam _ => y<=z), g', c, \lam j => (cover-trans (cover-proj2 idp () idp) (\lam _ => (d j).1),
      cover-prod (cover-proj1 idp () idp) (cover-trans (cover-prod (cover-trans (cover-proj1 idp () idp) (\lam _ => x<=y)) (cover-proj2 idp () idp)) (\lam _ => (d j).2))))
  \where \open Cover

\record FramePresPrehom \extends SetHom {
  \override Dom : FramePres
  \override Cod : FramePres
  | func-conj {x y : Dom} : func (conj x y) = conj (func x) (func y)
  | func-cover {J : \Set} {x : Dom} {f : J -> Dom} : BasicCover x f -> BasicCover (func x) (\lam j => func (f j))

  \func functor : Functor (framePresSite Dom) (framePresSite Cod) \cowith
    | F => func
    | Func => Cover.map
    | Func-id => idp
    | Func-o => idp
}

\record FramePresHom \extends FramePresPrehom
  | func-image {y : Cod} : Cover y func

\instance FramePresCat : Cat FramePres
  | Hom => FramePresHom
  | id X => \new FramePresHom {
    | func x => x
    | func-conj => idp
    | func-cover c => c
    | func-image {x} => cover-inj x idp
  }
  | o g f => \new FramePresHom {
    | func x => g (f x)
    | func-conj => pmap g func-conj *> func-conj
    | func-cover c => func-cover (func-cover c)
    | func-image => cover-trans func-image (\lam y => Cover.map func-image)
  }
  | id-left => idp
  | id-right => idp
  | o-assoc => idp
  | univalence => sip \lam {X} {S1} {S2} (h1 : FramePresHom) (h2 : FramePresHom) => exts FramePres {
    | conj x y => h1.func-conj
    | BasicCover x f => ext (h1.func-cover, h2.func-cover)
  }

{- | We can define the underlying set of {PresentedFrame} as the quotient of the set `P -> \Prop`
 -   under the relation `\Sigma (U <= V) (V <= U)`, where `U <= V` iff `\Pi (x : P) -> U x -> Cover x V`.
 -   Alternatively, we can define this set as a maximal element of an equivalence class.
 -   A subset is maximal if every element covered by it actually belongs to it.
 -   We use the second option.
 -}
\instance PresentedFrame (P : FramePres) : Locale
  | E => Opens P
  | <= => <=
  | <=-refl u => u
  | <=-transitive U<=V V<=W xU => V<=W (U<=V xU)
  | <=-antisymmetric U<=V V<=U => exts (\lam x => ext (U<=V, V<=U))
  | meet U V => closure \lam (t : \Sigma (a b : P) (U.1 a) (V.1 b)) => conj t.1 t.2
  | meet-left {U} {V} => closure<= \lam t => cover-proj1 idp (t.1,t.3) idp
  | meet-right {U} {V} => closure<= \lam t => Cover.cover-proj2 idp (t.2,t.4) idp
  | meet-univ {U} {V} {W} W<=U W<=V {x} xW => cover-trans (cover-idemp {P} {x} {\Sigma} {\lam _ => conj x x} () idp) \lam _ => cover-inj (x, x, W<=U xW, W<=V xW) idp
  | top => (\lam _ => \Sigma, \lam _ _ => ())
  | top-univ _ => ()
  | Join {J} f => closure {_} {\Sigma (j : J) (x : P) ((f j).1 x)} __.2
  | Join-cond j {_} {x} c => cover-inj (j,x,c) idp
  | Join-univ {J} {f} {U} d => closure<= \lam t => cover-inj (t.2, d t.1 t.3) idp
  | Join-ldistr>= => cover-trans __ \lam t => Cover.cover-ldistr' idp t.4 \lam s => inP ((s.1, conj t.1 s.2, cover-inj (t.1, s.2, t.3, s.3) idp), idp)
  \where {
    \open FramePres(SCover)
    \open Topology.Locale(PresentedFrame)

    \type Opens (P : FramePres) => \Sigma (U : P -> \Prop) (\Pi (x : P) -> SCover x U -> U x)

    \func closure {P : FramePres} {J : \Set} (g : J -> P) : Opens P
      => (Cover __ g, \lam x c => cover-trans c __.2)

    \type \infix 4 <= {P : FramePres} (U V : Opens P) => \Pi {x : P} -> U.1 x -> V.1 x

    \lemma closure<= {P : FramePres} {J : \Set} {g : J -> P} {U : Opens P} (p : \Pi (j : J) -> SCover (g j) U.1) : closure g <= U
      => \lam {x} c => U.2 x (cover-trans c p)

    \func embed {P : FramePres} (x : P) : PresentedFrame P
      => closure {_} {\Sigma} (\lam _ => x)

    \lemma embed<= {P : FramePres} {x : P} {U : Opens P} (p : SCover x U.1) : embed x <= U
      => closure<= (\lam _ => p)

    \lemma element_join {P : FramePres} {U : Opens P} : U = Join (\lam (q : \Sigma (x : P) (U.1 x)) => embed q.1)
      => <=-antisymmetric (\lam {x} Ux => cover-inj ((x,Ux), x, cover-inj () idp) idp) (\lam {x} c => U.2 x $ cover-trans c \lam q => cover-trans q.3 \lam _ => cover-inj q.1 idp)

    \func surj-map {L : Locale} {P : FramePres} (f : FrameHom L (PresentedFrame P)) (p : \Pi (y : P) ->  (x : L) (f x = embed y)) (U : PresentedFrame P) : \Sigma (x : L) (f x = U)
      => (SJoin (\lam x => f x <= U), func-Join *> exts (\lam y => ext (
          \lam c => U.2 y (cover-trans c \lam i => cover-inj (i.2, i.1.2 i.3) idp),
          \lam yU => \case p y \with {
            | inP (x,q) => cover-inj ((x, \lam {z} t => U.2 z $ rewrite q at t $ cover-trans t \lam _ => cover-inj (y,yU) idp), y, rewrite q (cover-inj () idp)) idp
          })))

    \lemma Cover_embed {P : FramePres} {a b : P} (a<=b : Cover1 a b) : embed a <= embed b
      => Cover.cover-trans1 __ a<=b

    \lemma embed_Cover {P : FramePres} {a b : P} (p : embed a <= embed b) : Cover1 a b
      => p (cover-inj () idp)

    \lemma embed_meet {P : FramePres} {a b : P} : embed a  embed b = embed (conj a b)
      => exts \lam e => ext (cover-trans __ \lam i => Cover.cover-conj1 i.3 i.4, Cover.cover-trans1 __ $ cover-inj (a, b, cover-inj () idp, cover-inj () idp) idp)

    \lemma func-equality {P : FramePres} {L : Locale} (f g : FrameHom (PresentedFrame P) L) (p : \Pi (x : P) -> f (embed x) = g (embed x)) (U : PresentedFrame P) : f U = g U
      => pmap f element_join *> f.func-Join *> path (\lam i => Join (\lam q => p q.1 i)) *> inv (pmap g element_join *> g.func-Join)

    \lemma func-equality_ext {P : FramePres} {L : Locale} {f g : FrameHom (PresentedFrame P) L} (p : \Pi (x : P) -> f (embed x) = g (embed x)) : f = g
      => exts $ func-equality f g p
  }

{- | Unital presentation of frames.
 -   {unit} represents the top element.
 -}
\class FrameUPres \extends FramePres
  | unit : E
  | isUnit {x : E} : BasicCover x (\lam (_ : \Sigma) => unit)

\record FrameUPresHom \extends FramePresHom {
  \override Dom : FrameUPres
  \override Cod : FrameUPres
  | func-unit : func unit = unit
  | func-image => cover-trans (cover-basic isUnit) (\lam _ => cover-inj unit func-unit)
}

\instance FrameUPresCat : Cat FrameUPres
  | Hom => FrameUPresHom
  | id X => \new FrameUPresHom {
    | FramePresHom => FramePresCat.id X
    | func-unit => idp
  }
  | o g f => \new FrameUPresHom {
    | FramePresHom => FramePresCat.o g f
    | func-unit => pmap g func-unit *> func-unit
  }
  | id-left => idp
  | id-right => idp
  | o-assoc => idp
  | univalence => sip \lam {X} {S1} {S2} (h1 : FrameUPresHom) (h2 : FrameUPresHom) => exts FrameUPres {
    | conj x y => h1.func-conj
    | BasicCover x f => ext (h1.func-cover, h2.func-cover)
    | unit => h1.func-unit
  }

\instance FrameUPresCocompleteCat : CocompleteCat FrameUPres
  | Cat => FrameUPresCat
  | colimit {J} G => \new Limit {
    | Cone => colimit-cone G
    | limMap => colimit-univ G
    | limBeta c j => idp
    | limUnique p => exts (colimit-univ-eq G (\lam {j} x => path (\lam i => p j i x)))
  }
  \where {
    \open FramePres

    \truncated \data FTerm {J : SmallPrecat} (G : Functor J FrameUPresCat) : \Set
      | finj {j : J} (G j)
      | fconj (FTerm G) (FTerm G)
      | funit
      | finj-eq {j j' : J} (h : Hom j j') (x : G j) : finj (G.Func h x) = finj x
      | fconj-eq {j : J} (x y : G j) : finj (conj x y) = fconj (finj x) (finj y)
      | funit-eq {j : J} : finj (unit {G j}) = funit

    \instance colimit-obj {J : SmallPrecat} (G : Functor J FrameUPresCat) : FrameUPres
      | E => FTerm G
      | conj => fconj
      | BasicCover {K} x f => (\Sigma (j : J) (y : G j) (g : K -> G j) (BasicCover y g) (x = finj y) (\Pi (k : K) -> f k = finj (g k))) || ((K,f) = {\Sigma (K : \Set) (K -> FTerm G)} (\Sigma, \lam _ => funit))
      | unit => funit
      | isUnit => byRight idp

    \func fpair {L M : Locale} (a : L) (b : M) : FTerm (Comp FrameUnitalReflectiveSubcat (Functor.op {Product.functor {Fin 2} {LocaleCat} ((L :: M :: nil) DArray.!!)}))
      => fconj (mkcon finj {0 : Fin 2} a) (mkcon finj {1 : Fin 2} b)

    \open Cover

    \lemma term-product {L M : Locale} (x : FTerm (Comp FrameUnitalReflectiveSubcat (Functor.op {Product.functor {Fin 2} {LocaleCat} ((L :: M :: nil) DArray.!!)})))
      :  (a : L) (b : M) (Cover1 x (fpair a b)) (Cover1 (fpair a b) x) \elim x
      | finj {0} a => inP (a, top, cover-prod (cover-inj () idp) (transportInv (Cover1 _) funit-eq (cover-basic (byRight idp))), cover-proj1 idp () idp)
      | finj {1} b => inP (top, b, cover-prod (transportInv (Cover1 _) funit-eq (cover-basic (byRight idp))) (cover-inj () idp), cover-proj2 idp () idp)
      | fconj t1 t2 => \case term-product t1, term-product t2 \with {
        | inP (a1,b1,p1,q1), inP (a2,b2,p2,q2) => inP (a1  a2, b1  b2,
            cover-prod (transportInv (Cover1 _) (path (fconj-eq a1 a2)) (cover-prod (cover-trans1 (cover-proj1 idp () idp) (cover-trans1 p1 (cover-proj1 idp () idp))) (cover-trans1 (cover-proj2 idp () idp) (cover-trans1 p2 (cover-proj1 idp () idp)))))
                       (transportInv (Cover1 _) (path (fconj-eq b1 b2)) (cover-prod (cover-trans1 (cover-proj1 idp () idp) (cover-trans1 p1 (cover-proj2 idp () idp))) (cover-trans1 (cover-proj2 idp () idp) (cover-trans1 p2 (cover-proj2 idp () idp))))),
            cover-prod (cover-trans1 (cover-prod (cover-trans1 (cover-proj1 idp () idp) (transportInv (Cover1 __ _) (path (fconj-eq a1 a2)) (cover-proj1 idp () idp))) (cover-trans1 (cover-proj2 idp () idp) (transportInv (Cover1 __ _) (path (fconj-eq b1 b2)) (cover-proj1 idp () idp)))) q1)
                       (cover-trans1 (cover-prod (cover-trans1 (cover-proj1 idp () idp) (transportInv (Cover1 __ _) (path (fconj-eq a1 a2)) (cover-proj2 idp () idp))) (cover-trans1 (cover-proj2 idp () idp) (transportInv (Cover1 __ _) (path (fconj-eq b1 b2)) (cover-proj2 idp () idp)))) q2))
      }
      | funit => inP (top, top, cover-prod (transportInv (Cover1 funit) funit-eq (cover-inj () idp)) (transportInv (Cover1 funit) funit-eq (cover-inj () idp)), cover-basic (byRight idp))

    \func colimitMap {J : SmallPrecat} (G : Functor J FrameUPresCat) (j : J) : FrameUPresHom (G j) (colimit-obj G) \cowith
      | func => finj
      | func-conj => path (fconj-eq _ _)
      | func-cover b => byLeft (_, _, _, b, idp, \lam k => idp)
      | func-unit => path funit-eq

    \func colimit-func {J : SmallPrecat} (G : Functor J FrameUPresCat) {Z : FrameUPres} (c : Cone G.op Z) (t : FTerm G) : Z \elim t
      | finj x => c.coneMap _ x
      | fconj t1 t2 => conj (colimit-func G c t1) (colimit-func G c t2)
      | funit => unit
      | finj-eq h x i => (c.coneCoh h @ i) x
      | fconj-eq {j} x y => func-conj {c.coneMap j} {x} {y}
      | funit-eq {j} => func-unit {c.coneMap j}

    \func colimit-univ {J : SmallPrecat} (G : Functor J FrameUPresCat) {Z : FrameUPres} (c : Cone G.op Z) : FrameUPresHom (colimit-obj G) Z \cowith
      | func => colimit-func G c
      | func-conj => idp
      | func-cover => \case __ \with {
        | byLeft (j,y,g,b,p,q) => rewrite p $ coe (\lam i => BasicCover _ (\lam k => colimit-func G c (inv (q k) @ i))) (func-cover {c.coneMap j} b) right
        | byRight p => transportInv (\lam q => BasicCover _ (\lam k => colimit-func G c (q.2 k))) p isUnit
      }
      | func-unit => idp

    \func colimit-cone {J : SmallPrecat} (G : Functor J FrameUPresCat) : Cone G.op \cowith
      | apex => colimit-obj G
      | coneMap => colimitMap G
      | coneCoh h => exts (\lam x => path (finj-eq h x))

    \lemma colimit-univ-eq {J : SmallPrecat} (G : Functor J FrameUPresCat) {Z : FrameUPres} {f g : FrameUPresHom (colimit-obj G) Z}
                           (p : \Pi {j : J} (x : G j) -> f (finj x) = g (finj x)) (t : FTerm G)
      : f t = g t \elim t
      | finj x => p x
      | fconj t1 t2 => func-conj *> pmap2 conj (colimit-univ-eq G p t1) (colimit-univ-eq G p t2) *> inv func-conj
      | funit => func-unit *> inv func-unit
  }

\func FrameUnitalSubcat : FullyFaithfulFunctor FrameCat FrameUPresCat \cowith
  | F (L : Locale) : FrameUPres \cowith {
    | E => L
    | conj => meet
    | BasicCover x f => x <= Join f
    | unit => top
    | isUnit => top-univ <=∘ Join-cond ()
  }
  | Func {X Y : Locale} (h : FrameHom X Y) : FrameUPresHom (F X) (F Y) \cowith {
    | func => h
    | func-conj => func-meet
    | func-cover c => transport (_ <=) func-Join (FrameHom.func-<= c)
    | func-unit => func-top
  }
  | Func-id => idp
  | Func-o => idp
  | isFullyFaithful => \new QEquiv {
    | ret h => \new FrameHom {
      | func => h
      | func-top => func-unit
      | func-meet => func-conj
      | func-Join>= => func-cover {h} <=-refl
    }
    | ret_f h => idp
    | f_sec h => idp
  }
  \where {
    \lemma Func-inverse {L M : Locale} (f : FrameUPresHom (F L) (F M)) (x : L) : FrameUnitalSubcat.inverse f x = f x
      => path (\lam i => FrameUnitalSubcat.inverse-right i x)
  }

\func FrameReflectiveSubcat : ReflectiveSubPrecat FrameCat FramePresCat \cowith
  | F => F
  | Func => Func
  | Func-id => idp
  | Func-o => idp
  | isFullyFaithful {X} {Y} => \new QEquiv {
    | ret h => \new FrameHom {
      | func => h
      | func-top>= => locale_cover (func-image {h}) <=∘ Join-univ (\lam x => rewrite (inv (pmap (func {h}) (meet_<= top-univ)) *> func-conj) meet-right)
      | func-meet => func-conj
      | func-Join>= => func-cover {h} <=-refl
    }
    | ret_f h => idp
    | f_sec h => idp
  }
  | reflector => PresentedFrame
  | reflectorMap (X : FramePres) : FramePresHom X (F (PresentedFrame X)) \cowith {
    | func => PresentedFrame.embed
    | func-conj {x} {y} => <=-antisymmetric
        (cover-trans __ \lam _ => cover-inj (x, y, cover-inj () idp, cover-inj () idp) idp)
        (cover-trans __ \lam t => Cover.cover-conj t.3 t.4 (\lam {_} {_} => inP ((),idp)))
    | func-cover {_} {_} {f} b c => cover-trans c \lam _ => cover-trans (cover-basic b) \lam j => cover-inj (j, f j, cover-inj () idp) idp
    | func-image => cover-basic (\lam {x} _ => cover-inj (x, x, cover-inj () idp) idp)
  }
  | isReflective {X : FramePres} {Y : Locale} => \new QEquiv {
    | ret => adjointMap
    | ret_f f => exts \lam U =>
        \let | g (q : \Sigma (x : X) (U.1 x)) => reflectorMap X q.1
             | t : U = Join g => exts \lam x => ext (\lam u => cover-inj ((x, u), x,