{- | We follow the following sources:
     [] Peter T. Johnstone, Stone Spaces, 1982
     [] Francis Borceux, Handbook of Categorical Algebra: Volume 3, 1994 (Chapter 1)
     [] Peter T. Johnstone, A constructive “Closed subgroup theorem” for localic groups and groupoids, 1989
     [] 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).)
  | 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.)
  | Meet-cond {J} j {f} => Join-univ (__. 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. ∧ g p.)
    => 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. ∧ g p.)
    => =_<= Join-distr

  \type \infix  << (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  --> (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. $ meet-monotone <=-refl p <=∘ eval <=∘ q

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

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

  \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. (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. (meet-right <=∘ p)

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

  \lemma neg-inverse {x y : E} (p : x <= y) : neg y <= neg x
    => exponent. $ 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  <=< (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  <=<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. (eval <=∘ meet-left)) (exponent. (eval <=∘ meet-right)))
        (exponent. (meet-univ (meet-monotone meet-left <=-refl <=∘ eval) (meet-monotone meet-right <=-refl <=∘ eval)))
    | nucleus-unit => exponent. meet-left
    | nucleus-join>= => exponent. (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). = x. --> y.
    => <=-antisymmetric (Join-univ \lam p => exponent. $ exponent. (=_<= (meet-assoc *> pmap (_ ∧) meet-comm *> inv meet-assoc) <=∘ meet-monotone p. <=-refl <=∘ Join-rdistr>= <=∘ Join-univ __.) <=∘ y.)
                        (Join-univ \lam p => exponent. $ exponent. (meet-left <=∘ meet-left) <=∘ Join-cond (later ((a --> p., nucleus-join>=), exponent. (meet-univ (meet-monotone meet-left <=-refl <=∘ eval) (meet-left <=∘ meet-right) <=∘ p.) <=∘ y.)))

  \lemma open-isOpen (a : E) : isOpen {Nucleus.map {open a}}
    => \lam x => inP (a ∧ x., \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. <= q.
    | <=-refl => <=-refl
    | <=-transitive => <=∘
    | <=-antisymmetric p q => ext (<=-antisymmetric p q)
    | meet p q => (p. ∧ q., meet-left <=∘ p.)
    | meet-left => meet-left
    | meet-right => meet-right
    | meet-univ => meet-univ
    | top => (a, <=-refl)
    | top-univ {x} => x.
    | Join g => (Join (\lam j => (g j).), Join-univ (\lam j => (g j).))
    | 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.
        | 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 __.

  \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. meet-left) (direct-adjoint. 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.
    | 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.)

  \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. 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.
    | func-top => func-top
    | func-meet => func-meet
    | func-Join>= => direct-adjoint. (Meet-cond $ later (image, \lam hx<=P => direct-adjoint. (hx<=P <=∘ func-pHat<=))) <=∘ func-Join>=

  \lemma wclosed-factor-sdense : wclosed-factor.isStronglyDense
    => \lam c => Meet-univ (\lam j => j. 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. 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. $ direct-adjoint. $ direct-counit {g FrameCat.∘ f}) ((direct-adjoint {g FrameCat.∘ f}). $ 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. $ 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. $ meet-monotone nucleus-unit <=-refl <=∘ nucleus-meet>= <=∘ nucleus-<= p.

  \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 __).), nucleus-join>=)
    | Join-cond j {f} => Join-cond j <=∘ nucleus-unit
    | Join-univ {J} {f} {e} h => nucleus-<= (Join-univ h) <=∘ e.
    | 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., ext $ <=-antisymmetric y. nucleus-unit)
    }

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

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

  \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. 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. j)
  | Join-univ c {x} => Join-univ \lam p => p. (_,c)
  | Join-ldistr>= {J} {g} {k} {x} => Join-ldistr>= <=∘ Join-univ (\lam p => Meet-univ \lam q => =_<= meet-comm <=∘ exp-univ2 (p. (exp k q., \lam j => exp-univ1 \lam {y} => =_<= meet-comm <=∘ q. 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. --> j' p.
      | 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., join-left)) (Meet-cond $ later (b ∨ p., join-left)) <=∘
          exponent. (=_<= 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. meet-left) meet-right))
      | nucleus-<= x<=y => Meet-univ \lam p => Meet-cond (later (p., x<=y <=∘ p.)) <=∘ exponent. eval
      | nucleus-unit => Meet-univ \lam p => exponent. $ meet-left <=∘ p. <=∘ nucleus-unit
      | nucleus-join>= => Meet-univ \lam p => Meet-cond (later (j p. --> j' p., Meet-cond p)) <=∘ exponent_monotone <=-refl (Nucleus.nucleus_exponent nucleus-join>=) <=∘
          =_<= exponent-double <=∘ exponent_monotone (meet-univ (nucleus-<= $ exponent. $ 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. $ meet-monotone (nucleus-<= q.) <=-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. $ 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., 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., j<=j' <=∘ y.), ext $ <=-antisymmetric y. 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. 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. 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. (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. $ transport (\lam (f : FrameHom L sub) => f (j x) <= f x) jh1=f $ func-<= nucleus-join>=)
                            (\lam {x} => direct-adjoint. $ 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. 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. (p <=∘ bottom-univ)) (exponent. meet-left))
  \where
    \lemma conv {L : Locale} {c a : L} (p : open a >= closed c) : c ∧ a <= bottom
      => meet-monotone join-left <=-refl <=∘ exponent. 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). }
           | 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  << (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.)

  \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).} {J}) ((h i). = e) (\Pi (j : (h i).) -> (h i). j = g (p j))

  \lemma indexing-make {I X : \Set} {h : I -> \Sigma (J : \Set) X (J -> X)} (i : I) : Indexing h (h i). (h i).
    => 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). (g i).)
                            {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)., (g i).) = {\Sigma (K : \Set) (K -> X)} (J,f) => exts (Equiv-to-= q, t)
      \in coe (\lam i => P {(r @ i).} (s @ i) (r @ i).) (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. i.

    \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). (g' j)) (Cover1 (conj x (g' j)) (g j).))
  | 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).),
      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).))))
  \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. a) (V. b)) => conj t. t.
  | meet-left {U} {V} => closure<= \lam t => cover-proj1 idp (t.,t.) idp
  | meet-right {U} {V} => closure<= \lam t => Cover.cover-proj2 idp (t.,t.) 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). x)} __.
  | Join-cond j {_} {x} c => cover-inj (j,x,c) idp
  | Join-univ {J} {f} {U} d => closure<= \lam t => cover-inj (t., d t. t.) idp
  | Join-ldistr>= => cover-trans __ \lam t => Cover.cover-ldistr' idp t. \lam s => inP ((s., conj t. s., cover-inj (t., s., t., s.) 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 __.)

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

    \lemma closure<= {P : FramePres} {J : \Set} {g : J -> P} {U : Opens P} (p : \Pi (j : J) -> SCover (g j) U.) : closure g <= U
      => \lam {x} c => U. 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.) : embed x <= U
      => closure<= (\lam _ => p)

    \lemma element_join {P : FramePres} {U : Opens P} : U = Join (\lam (q : \Sigma (x : P) (U. x)) => embed q.)
      => <=-antisymmetric (\lam {x} Ux => cover-inj ((x,Ux), x, cover-inj () idp) idp) (\lam {x} c => U. x $ cover-trans c \lam q => cover-trans q. \lam _ => cover-inj q. 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. y (cover-trans c \lam i => cover-inj (i., i.. i.) idp),
          \lam yU => \case p y \with {
            | inP (x,q) => cover-inj ((x, \lam {z} t => U. 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. i., 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. 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 } {LocaleCat} ((L :: M :: nil) DArray.!!)}))
      => fconj (mkcon finj { : Fin } a) (mkcon finj { : Fin } b)

    \open Cover

    \lemma term-product {L M : Locale} (x : FTerm (Comp FrameUnitalReflectiveSubcat (Functor.op {Product.functor {Fin } {LocaleCat} ((L :: M :: nil) DArray.!!)})))
      : ∃ (a : L) (b : M) (Cover1 x (fpair a b)) (Cover1 (fpair a b) x) \elim x
      | finj {} a => inP (a, top, cover-prod (cover-inj () idp) (transportInv (Cover1 _) funit-eq (cover-basic (byRight idp))), cover-proj1 idp () idp)
      | finj {} 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. 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. t. (\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. x)) => reflectorMap X q.
             | t : U = Join g => exts \lam x => ext (\lam u => cover-inj ((x, u), x, cover-inj () idp) idp, closure<= \lam t => cover-trans t. \lam _ => cover-inj t. idp)
        \in rewrite t $ func-Join {_} {_} {g} *> inv (pmap Join (ext (\lam j => pmap f PresentedFrame.element_join *> func-Join))) *> inv (func-Join {f} {_} {g})
    | f_sec f => exts (adjointMap_embed f)
  }
  \where {
    \open PresentedFrame \hiding (<=)
    \open FrameUnitalSubcat

    \lemma locale_cover {L : Locale} {x : L} {J : \Set} {g : J -> L} (c : Cover {F L} x g) : x <= L.Join g \elim c
      | cover-basic b => b
      | cover-inj j p => rewriteI p (Join-cond j)
      | cover-trans c f => locale_cover c <=∘ Join-univ (\lam i => locale_cover (f i))
      | cover-proj1 p j q => rewrite p (meet-left <=∘ rewriteI q (Join-cond j))
      | cover-idemp j p => transport (`<= _) (p *> meet-idemp) (Join-cond j)
      | cover-comm p j q => transport (`<= _) (q *> meet-comm *> inv p) (Join-cond j)
      | cover-ldistr p c f => rewrite p (meet-monotone <=-refl (locale_cover c) <=∘ Join-ldistr>= <=∘ Join-univ (\lam j => transport (`<= _) (f j) (Join-cond j)))

    \func adjointMap {X : FramePres} {Y : Locale} (f : FramePresHom X (F Y)) : FrameHom (PresentedFrame X) Y \cowith
      | func U => Y.Join {\Sigma (x : X) (U. x)} (\lam j => f j.)
      | func-top>= => locale_cover f.func-image <=∘ Join-univ (\lam x => Join-cond (x, ()))
      | func-meet {U} {V} => <=-antisymmetric
          (Join-univ $ later \lam p => locale_cover (Cover.map p.) <=∘ Join-univ (\lam t => rewrite f.func-conj $ Join-cond $ later ((t.,t.),(t.,t.))))
          (Join-univ \lam p => transport (`<= _) f.func-conj (Y.Join-cond $ later (conj p.. p.., cover-inj (later (p.., p.., p.., p..)) idp))) *> inv Locale.Join-distr
      | func-Join>= => Join-univ \lam p => locale_cover (Cover.map p.) <=∘ Join-univ (\lam t => Join-cond (later (t.,t.)) <=∘ Join-cond t.)

    \lemma adjointMap_embed {X : FramePres} {Y : Locale} (f : FramePresHom X (F Y)) (x : X) : adjointMap f (embed x) = f x
      => <=-antisymmetric
          (Join-univ (\lam j => locale_cover (Cover.map j.) <=∘ Join-univ (\lam _ => <=-refl)))
          (Join-cond (later (x, cover-inj () idp)))
  }

\func FrameUnitalReflectiveSubcat : ReflectiveSubPrecat FrameCat FrameUPresCat \cowith
  | FullyFaithfulFunctor => FrameUnitalSubcat
  | reflector X => FrameReflectiveSubcat.reflector X
  | reflectorMap X => \new FrameUPresHom {
    | FramePresHom => FrameReflectiveSubcat.reflectorMap X
    | func-unit => exts (\lam e => ext (\lam _ => (), \lam _ => cover-basic isUnit))
  }
  | isReflective {X} {Y} => \new QEquiv {
    | ret h => FrameReflectiveSubcat.isReflective.ret h
    | ret_f h => FrameReflectiveSubcat.isReflective.ret_f h
    | f_sec h => ext (path (\lam i => func {FrameReflectiveSubcat.isReflective.f_ret h @ i}))
  }

\func FrameBicat : BicompleteCat \cowith
  | Cat => FrameCat
  | limit G => \new Limit {
    | apex => limit-obj G
    | coneMap j => \new FrameHom {
      | func P => P. j
      | func-top => idp
      | func-meet => idp
      | func-Join => idp
    }
    | coneCoh h => exts (\lam P => P. h)
    | isLimit Z => \new QEquiv {
      | ret (c : Cone) => \new FrameHom {
        | func z => (\lam j => c.coneMap j z, \lam h => path (\lam i => func {c.coneCoh h @ i} z))
        | func-top => exts (\lam j => func-top)
        | func-meet => exts (\lam j => func-meet)
        | func-Join => exts (\lam j => func-Join)
      }
      | ret_f f => exts (\lam z => exts (\lam j => idp))
      | f_sec c => idp
    }
  }
  | pullback {X} {Y} {Z} f g => \new Pullback {
    | apex => pullback-obj f g
    | pbProj1 => proj1
    | pbProj2 => proj2
    | pbCoh => exts __.
    | pbMap p1 p2 c => \new FrameHom {
      | func x => (p1 x, p2 x, path (\lam i => c i x))
      | func-top => ext (func-top, func-top)
      | func-meet => ext (func-meet, func-meet)
      | func-Join => ext (func-Join, func-Join)
    }
    | pbBeta1 => idp
    | pbBeta2 => idp
    | pbEta p q => exts (\lam x => ext (path (\lam i => p i x), path (\lam i => q i x)))
  }
  | colimit G => reflectiveSubPrecatColimit FrameUnitalReflectiveSubcat G (FrameUPresCocompleteCat.colimit (Comp FrameUnitalReflectiveSubcat G))
  \where {
    \func limit-obj {J : SmallPrecat} (G : Functor J FrameCat) : Locale \cowith
      | E => \Sigma (P : \Pi (j : J) -> G j) (\Pi {j j' : J} (h : Hom j j') -> G.Func h (P j) = P j')
      | <= (P,_) (Q,_) => \Pi (j : J) -> P j <= Q j
      | <=-refl j => <=-refl
      | <=-transitive p q j => <=-transitive (p j) (q j)
      | <=-antisymmetric p q => exts (\lam j => <=-antisymmetric (p j) (q j))
      | meet (P,Pc) (Q,Qc) => (\lam j => P j ∧ Q j, \lam h => func-meet *> pmap2 (∧) (Pc h) (Qc h))
      | meet-left j => meet-left
      | meet-right j => meet-right
      | meet-univ p q j => meet-univ (p j) (q j)
      | top => (\lam j => top, \lam h => func-top)
      | top-univ j => top-univ
      | Join F => (\lam j => Join (\lam k => (F k). j), \lam {j} {j'} h => func-Join *> path (\lam i => Join (\lam k => (F k). h @ i)))
      | Join-cond k j => Join-cond k
      | Join-univ p j => Join-univ (\lam k => p k j)
      | Join-ldistr>= j => Join-ldistr>=

    \func pullback-obj {L M K : Locale} (f : FrameHom L K) (g : FrameHom M K) : Locale \cowith
      | E => \Sigma (x : L) (y : M) (f x = g y)
      | <= P Q => \Sigma (P. <= Q.) (P. <= Q.)
      | <=-refl => (<=-refl, <=-refl)
      | <=-transitive p q => (p. <=∘ q., p. <=∘ q.)
      | <=-antisymmetric p q => ext (<=-antisymmetric p. q., <=-antisymmetric p. q.)
      | meet P Q => (P. ∧ Q., P. ∧ Q., func-meet *> pmap2 (∧) P. Q. *> inv func-meet)
      | meet-left => (meet-left, meet-left)
      | meet-right => (meet-right, meet-right)
      | meet-univ p q => (meet-univ p. q., meet-univ p. q.)
      | top => (top, top, func-top *> inv func-top)
      | top-univ => (top-univ, top-univ)
      | Join F => (Join (\lam j => (F j).), Join (\lam j => (F j).), func-Join *> pmap Join (ext (\lam j => (F j).)) *> inv func-Join)
      | Join-cond j {f} => (Join-cond j, Join-cond j)
      | Join-univ p => (Join-univ (\lam j => (p j).), Join-univ (\lam j => (p j).))
      | Join-ldistr>= => (Join-ldistr>=, Join-ldistr>=)

    \func proj1 {L M K : Locale} {f : FrameHom L K} {g : FrameHom M K} : FrameHom (pullback-obj f g) L \cowith
      | func P => P.
      | func-top => idp
      | func-meet => idp
      | func-Join>= => <=-refl

    \func proj2 {L M K : Locale} {f : FrameHom L K} {g : FrameHom M K} : FrameHom (pullback-obj f g) M \cowith
      | func P => P.
      | func-top => idp
      | func-meet => idp
      | func-Join>= => <=-refl

    \lemma coneMap_finj {J : SmallPrecat} {G : Functor J FrameCat} (j : J) (x : G j)
      : coneMap {FrameBicat.colimit G} j x = embed (FrameUPresCocompleteCat.finj {J} {Comp FrameUnitalReflectiveSubcat G} x)
      => FrameUnitalSubcat.Func-inverse _ x
  }

\func discrete (X : \Set) : Locale (X -> \Prop) \cowith
  | <= U V => \Pi {x : X} -> U x -> V x
  | <=-refl u => u
  | <=-transitive p q u => q (p u)
  | <=-antisymmetric p q => ext (\lam e => ext (p,q))
  | meet U V x => \Sigma (U x) (V x)
  | meet-left => __.
  | meet-right => __.
  | meet-univ p q e => (p e, q e)
  | top _ => \Sigma
  | top-univ _ => ()
  | Join {J} F x => ∃ (j : J) (F j x)
  | Join-cond j u => inP (j,u)
  | Join-univ c => \case __ \with {
    | inP (j,u) => c j u
  }
  | Join-ldistr>= => \case __ \with {
    | (u, inP (j,v)) => inP (j,(u,v))
  }
  \where {
    \func functor : Functor SetCat LocaleCat \cowith
      | F => discrete
      | Func {X} {Y} f => \new FrameHom {
        | func U x => U (f x)
        | func-top>= _ => ()
        | func-meet => idp
        | func-Join => idp
      }
      | Func-id => idp
      | Func-o => idp

    \lemma exponent {X : \Set} (P Q : X -> \Prop) : P --> {discrete X} Q = (\lam x => P x -> Q x)
      => ext \lam x => ext (\lam (inP ((S,SP=>Q),s)) p => SP=>Q (s,p), \lam P=>Q => inP ((\lam x => P x -> Q x, \lam p => p. p.), P=>Q))
  }

\instance LocaleCat : BicompleteCat \cowith
  | Cat => Cat.op {FrameBicat}
  | limit (G : Functor) => FrameBicat.colimit G.op
  | colimit (G : Functor) => FrameBicat.limit G.op
  | terminal {
    | apex => discrete (\Sigma)
    | proj => \case __
    | tupleMap _ => \new FrameHom {
      | func P => pHat (P ())
      | func-<= x<=y => Join-univ (\lam xu => Join-cond (x<=y xu))
      | func-top>= => Join-cond ()
      | func-meet>= => rewrite Join-distr $ Join-univ (\lam p => meet-left <=∘ Join-cond p)
      | func-Join>= => Join-univ (\lam (inP (j,x)) => Join-cond x <=∘ Join-cond j)
    }
    | tupleBeta {_} {_} {j} => \case j
    | tupleEq _ => exts \lam P =>
        \have t : P = pHat {discrete (\Sigma)} (P ()) => ext \lam _ => ext (\lam x => inP (x,()), \lam (inP (x,_)) => x)
        \in rewrite t $ func-Join *> path (\lam i => Join (\lam _ => (func-top *> inv func-top) i)) *> inv func-Join
  }
  \where {
    \lemma terminal-direct {L : Locale} (x : L) : direct {LocaleCat.terminalMap {L}} x = (\lam _ => top <= x)
      => ext \lam _ => ext (\lam (inP ((P,P<=x),p)) => Join-cond p <=∘ P<=x, \lam top<=x => inP ((\lam _ => \Sigma, top-univ <=∘ top<=x), ()))
  }

\open FrameHom

-- | Open maps are closed under pullbacks.
\lemma pullback_open (P : Pullback {LocaleCat}) (o : isOpen {P.g}) : isOpen {P.pbProj1}
  => {?} -- [2, Theorem 1.6.4]

-- | Strongly dense maps are closed under pullbacks along open maps.
\lemma pullback_sdense (P : Pullback {LocaleCat}) (o : isOpen {P.f}) (d : isStronglyDense {P.g}) : isStronglyDense {P.pbProj1}
  => {?} -- [3, Lemma 1.9]

-- | A locale {L} is overt if and only the unique map from L to the terminal locale is open.
\lemma overt=open {L : Locale} : L.isOvert <-> isOpen {LocaleCat.terminalMap {L}}
  => coe2 (\lam i => L.isOvert <-> (\Pi (x : L) -> ∃ (P : \Sigma -> \Prop) ∀ (Q : \Sigma -> \Prop) (LocaleCat.terminal-direct (x --> pHat (Q ())) i = discrete.exponent P Q @ i))) right
      (\lam o x => inP (\lam _ => isPositive x, \lam Q => ext \lam _ => ext (\lam x<=Q x>0 => x>0 (Q ()) $ meet-univ top-univ <=-refl <=∘ exponent. x<=Q, \lam f => exponent. $ meet-right <=∘ o x <=∘ pHat-impl f)),
       \lam f x => \case f x \with {
         | inP (P,g) => meet-univ top-univ <=-refl <=∘ exponent. (propExt.conv (pmap (__ ()) $ g (\lam _ => isPositive x)) (\lam p Q x<=Q => propExt.dir (pmap (__ ()) $ g (\lam _ => Q)) (exponent. $ meet-right <=∘ x<=Q) p))
       }) left

-- | Open maps are closed under composition.
\lemma open-comp {L M K : Locale} (f : Hom L M) (fo : isOpen {f}) (g : Hom M K) (go : isOpen {g}) : isOpen {g LocaleCat.∘ f}
  => {?} -- [2, Corollary 1.6.3]

\lemma regular_surj {L M : Locale} {f : Hom L M} (reg : isRegularMono {LocaleCat} f) : isSurj f \elim reg
  | inP (E : Equalizer) => \lam y =>
    \let | E' : Equalizer => LocaleCat.equalizer E.f E.g
         | s => PresentedFrame.surj-map E'.eql regular_surj-lemma
         | i : Iso => Equalizer.unique E E'
         | x => (s (i.hinv y)).
    \in inP (x, inv (path (\lam j => Equalizer.unique-map E E' j x)) *> pmap i.f (s (i.hinv y)). *> path (\lam j => i.hinv_f j y))
  \where {
    \open FrameUPresCocompleteCat

    \func regular_surj-lemma {L M : Locale} {f g : LocaleCat.Hom L M} (y : FTerm (Comp FrameUnitalReflectiveSubcat (Functor.op {Equalizer.functor {LocaleCat} f g})))
      : ∃ (x : L) (Equalizer.eql {LocaleCat.equalizer f g} x = embed y) \elim y
      | finj {j} x => \case \elim j, \elim x \with {
        | false, x => inP (x, FrameBicat.coneMap_finj false x)
        | true, x => inP (f x, FrameBicat.coneMap_finj false (f x) *> pmap embed (path (finj-eq {Equalizer.Shape.op} Equalizer.arrow1 x)))
      }
      | fconj t1 t2 => \case regular_surj-lemma t1, regular_surj-lemma t2 \with {
        | inP (x1,p1), inP (x2,p2) => inP (x1 ∧ x2, func-meet *> pmap2 (∧) p1 p2 *> exts (\lam e => ext (cover-trans __ (\lam i => Cover.cover-conj1 i. i.), cover-trans __ (\lam _ => cover-inj (t1, t2, cover-inj () idp, cover-inj () idp) idp))))
      }
      | funit => inP (top, func-top *> exts (\lam e => ext (\lam _ => cover-basic (byRight idp), \lam _ => ())))
  }

\lemma surj_regular {L M : Locale} {f : FrameHom M L} (sur : isSurj f) : isRegularMono {LocaleCat} f
  => \let pb : Pullback => FrameBicat.pullback f f
     \in inP (\new Equalizer {LocaleCat} {M} {pb} pb.pbProj1 pb.pbProj2 L f pb.pbCoh {
       | isEqualizer Z => \new ESEquiv {
         | isSurjMap (h,p) =>
           \have lem (x : M) => path (\lam i => p i (f.direct (f x), x, FrameHom.surjective-split sur (f x)))
           \in inP (\new FrameHom {
             | func x => h (f.direct x)
             | func-top => pmap h f.direct-top *> func-top
             | func-meet => pmap h f.direct-meet *> func-meet
             | func-Join {J} {g} => inv (pmap (\lam z => h (f.direct z)) func-Join *> path (\lam i => h (f.direct (Join (\lam j => FrameHom.surjective-split sur (g j) i))))) *> lem _ *> func-Join
           }, ext (exts lem))
         | Embedding => Embedding.fromInjection \lam {h} {h'} p => exts \case sur __ \with {
           | inP (x,q) => inv (pmap h q) *> pmap (\lam z => z. x) p *> pmap h' q
         }
       }
     })

\func surj_equiv {f : FrameHom} (sur : isSurj f) : Iso {FrameCat} {f.image.locale} {f.Cod}
  => FrameCat.equiv_iso {\new FrameHom f.image.locale f.Cod {
    | func x => f x.
    | func-top => func-top
    | func-meet => func-meet
    | func-Join>= => f.direct-counit <=∘ func-Join>=
  }} (\new QEquiv {
    | ret x => (f.direct x, f.direct-<= $ =_<= $ f.surjective-split sur x)
    | ret_f x => ext (<=-antisymmetric x. f.direct-unit)
    | f_sec x => f.surjective-split sur x
  })
  \where {
    \lemma map-comm {f : FrameHom} (sur : isSurj f) (x : f.Dom) : Iso.f {surj_equiv sur} (f.image.map x) = f x
      => f.surjective-split sur (f x)
  }

\type isHausdorffLocale (L : Locale) => generalized L (LocaleCat.Bprod L L) LocaleCat.proj1 LocaleCat.proj2
  \where {
    \open PrecatWithBprod
    \open CartesianPrecat
    \open FrameUPresCocompleteCat
    \open Cover
    \open FrameReflectiveSubcat(locale_cover)
    \open FrameBicat(coneMap_finj)

    \func generalized (L M : Locale) (p1 p2 : Hom M L) => \Pi (a b : L) (y : M)
      -> a ∧ b <= SJoin (\lam x => p1 x ∧ p2 x <= y)
      -> p1 a ∧ p2 b <= extend p1 p2 y

    \func extend {L M : Locale} (p1 p2 : Hom M L) (y : M)
      => SJoin (\lam x => x <= y || (\Sigma (a b : L) (a ∧ b <= bottom) (x = p1 a ∧ p2 b)))

    \lemma diagonal_func {L : Locale} (U : LocaleCat.Bprod L L) : diagonal L U = SJoin (\lam x => U. (fpair x x))
      => <=-antisymmetric (Join-univ (\lam j => \case term-product j. \with {
        | inP (a,b,p,q) => locale_cover (map {colimit-univ (Comp FrameUnitalReflectiveSubcat (Functor.op {Product.functor (L :: L :: nil)})) $ Cone.map FrameUnitalReflectiveSubcat.op $ Product.fromLimit.cone {_} {_} {_} {Product.functor (L :: L :: nil)} \case __ \with { |  => id L |  => id L }} p) <=∘
            Join-univ (\lam _ => Join-cond $ later (a ∧ b, U. _ $ cover-trans1 (cover-conj1 (transportInv (Cover1 __ _) (path (fconj-eq a b)) (cover-proj1 idp () idp)) (transportInv (Cover1 __ _) (path (fconj-eq a b)) (cover-proj2 idp () idp))) $ cover-trans1 q $ cover-inj j idp))
      })) (Join-univ (\lam j => meet-univ <=-refl <=-refl <=∘ Join-cond (later (_, j.))))

    \lemma diagonal_direct {L : Locale} (a : L) : FrameHom.direct {diagonal L} a = PresentedFrame.closure (\lam (j : \Sigma (b c : L) (b ∧ c <= a)) => fpair j. j.)
      => <=-antisymmetric (Join-univ (\lam (U,Up) {t} Ut => \case term-product t \with {
        | inP (x,y,p,q) => cover-trans1 p (cover-inj (x, y, Join-cond (later (_, U. _ $ unfold fpair $ repeat {} (rewrite (path (fconj-eq x y))) $ cover-trans1 (cover-conj1 (cover-proj1 idp () idp) (cover-proj2 idp () idp)) $ cover-trans1 q $ cover-inj (t,Ut) idp)) <=∘ =_<= (inv (diagonal_func U)) <=∘ Up) idp)
      })) $ closure<= \lam j => cover-inj (_, unfold FrameHom.direct $ cover-inj (
            \let U => closure (\lam _ => fpair j. j.)
            \in (U, =_<= (diagonal_func U) <=∘ Join-univ (\lam k =>
                \have m => colimit-univ _ $ Product.fromLimit.cone $ later \case __ \with { |  => id _ |  => id _ }
                \in (meet-univ <=-refl <=-refl <=∘ locale_cover (map {m} k.) <=∘ Join-univ (\lam _ => <=-refl)) <=∘ j.)), _, cover-inj () idp) idp) idp

    \lemma diagonal-isClosed {L : Locale} (h : isHausdorffLocale L) : Nucleus.isClosed {FrameHom.image {diagonal L}}
      => \lam {U} => rewrite (diagonal_direct, diagonal_direct, diagonal_func, FrameHom.func-bottom {diagonal L}) $ closure<= $ later \lam j =>
          \have t => h j. j. U (j. <=∘ Join-univ (\lam k => Join-cond $ later (_, \lam {x} c => U. x (cover-trans c \lam (a,b,a<=k,b<=k) => run {
                       rewrite coneMap_finj at a<=k,
                       rewrite coneMap_finj at b<=k,
                       cover-trans1 (cover-conj1 a<=k b<=k),
                       cover-inj (_, k.) idp
                     })))) (cover-inj (_, _, rewrite coneMap_finj $ cover-inj () idp, rewrite coneMap_finj $ cover-inj () idp) idp)
          \in cover-trans t \lam l => cover-inj (l., \case l.. \with {
            | byLeft v => cover-inj (false, l., v l.) idp
            | byRight v => cover-inj (true, l., cover-trans (transport (__. l.) v. l.) \lam (a,b,a<=v1,b<=v2) => cover-trans1 (cover-conj1 (rewrite coneMap_finj at a<=v1 $ a<=v1) (rewrite coneMap_finj at b<=v2 $ b<=v2)) (cover-inj (v.,v.,v.) idp)) idp
          }) idp
  }

-- | Regular locales are Hausdorff
\lemma regular_Hausdorff {L : Locale} (reg : L.isRegular) : isHausdorffLocale L
  => generalized reg (LocaleCat.Bprod L L) LocaleCat.proj1 LocaleCat.proj2
  \where {
    \open isHausdorffLocale (extend)
    \open FrameHom

    \lemma generalized {L : Locale} (reg : L.isRegular) (M : Locale) (p1 p2 : LocaleCat.Hom M L) : isHausdorffLocale.generalized L M p1 p2
      => \lam a b U p =>
         \have | lem1 {d x y : L} (p : d <=< x) (q : p1 (y ∧ x) ∧ p2 d <= extend p1 p2 U) : p1 y ∧ p2 d <= extend p1 p2 U
                 => meet-monotone (func-<= (meet-univ <=-refl (top-univ <=∘ later p) <=∘ ldistr>=) <=∘ func-Join>=) <=-refl <=∘ Join-rdistr>= <=∘ Join-univ (\case \elim __ \with {
                   | false => q
                   | true => Join-cond (later (p1 (y ∧ neg d) ∧ p2 d, byRight (y ∧ neg d, d, meet-monotone meet-right <=-refl <=∘ eval, idp)))
                 })
               | lem2 {d x y : L} (p : d <=< x) (q : p1 d ∧ p2 (y ∧ x) <= extend p1 p2 U) : p1 d ∧ p2 y <= extend p1 p2 U
                 => meet-monotone <=-refl (func-<= (meet-univ <=-refl (top-univ <=∘ later p) <=∘ ldistr>=) <=∘ func-Join>=) <=∘ Join-ldistr>= <=∘ Join-univ (\case \elim __ \with {
                   | false => q
                   | true => Join-cond (later (p1 d ∧ p2 (y ∧ neg d), byRight (d, y ∧ neg d, meet-monotone <=-refl meet-right <=∘ =_<= meet-comm <=∘ eval, idp)))
                 })
               | tu<=NU {t u : L} (q : p1 u ∧ p2 u <= extend p1 p2 U) : p1 t ∧ p2 u <= extend p1 p2 U
                 => meet-monotone <=-refl (func-<= (reg u) <=∘ func-Join>=) <=∘ Join-ldistr>= <=∘ Join-univ (\lam j => lem1 j. (meet-monotone (func-<= meet-right) (func-<= (<=<_<= j.)) <=∘ q))
               | ss<=NU => meet-monotone <=-refl func-Join>= <=∘ Join-ldistr>= <=∘ Join-univ (\lam j => tu<=NU (Join-cond (later (p1 j. ∧ p2 j., byLeft j.))))
         \in meet-monotone (func-<= (reg a) <=∘ func-Join>=) <=-refl <=∘ Join-rdistr>= <=∘ Join-univ (\lam j => lem2 j. (meet-monotone <=-refl (func-<= (=_<= meet-comm <=∘ p)) <=∘ tu<=NU ss<=NU))
  }

\func dense_closed_ofs : OFS {LocaleCat} \cowith
  | L f => isDense {f}
  | R (f : FrameHom) => \Sigma f.image.isClosed (isSurj f)
  | factors {L} {M} (h : FrameHom) =>
    \have n : Nucleus => closed (h.direct bottom)
    \in (n.locale,
         \new FrameHom {
           | func x => h.func x.
           | func-top => func-top
           | func-meet => func-meet
           | func-Join>= => func-join>= <=∘ join-univ (direct-counit <=∘ bottom-univ) func-Join>=
         },
         n.map,
         exts \lam x => func-join *> <=-antisymmetric (join-univ (direct-counit <=∘ bottom-univ) <=-refl) join-right,
         \lam {x} p => unfold $ direct-unit <=∘ direct-<= p <=∘ join-left,
         (\lam {x} => =_<= (n.map_direct (n.map x)) <=∘ join-univ (join-left <=∘ =_<= (inv (n.map_direct (n.map bottom))) <=∘ join-left) join-right, Nucleus.map.surjective {n}))
  | unique-lift f (g : FrameHom) Lf Rg => OFS.liftFromMono {LocaleCat} f g (regularMono_Mono (surj_regular Rg.)) \lam t s p =>
    \have lem x : s (g.direct (g x)) = s x => <=-antisymmetric (func-<= (Rg. {x}) <=∘ func-join>= <=∘ join-univ (Lf (=_<= (inv (path (\lam i => p i (g.direct (inv g.func-bottom i)))) *> pmap t (surjective-split Rg. bottom) *> func-bottom)) <=∘ bottom-univ) <=-refl) (func-<= direct-unit)
    \in (\new FrameHom {
       | func x => s (g.direct x)
       | func-top => pmap s g.direct-top *> func-top
       | func-meet => pmap s g.direct-meet *> func-meet
       | func-Join {J} {F} => inv (pmap (\lam x => s (g.direct x)) func-Join *> path (\lam i => s (g.direct (Join (\lam j => g.surjective-split Rg. (F j) i))))) *> lem _ *> func-Join
     }, exts lem)
  \where \open FrameHom

\func sdense_wclosed_ofs : OFS {LocaleCat} \cowith
  | L f => isStronglyDense {f}
  | R f => isWeaklyClosed {f}
  | factors {L} {M} (h : FrameHom) =>
    \have left+right=h x : h.wclosed-factor (h.wclosed-image.map x) = h x => unfold $ <=-antisymmetric (direct-adjoint. (Meet-cond $ later (h.image, \lam {P} {y} hy<=P => direct-adjoint. (hy<=P <=∘ func-pHat<=)))) (func-<= h.wclosed-image.nucleus-unit)
    \in (h.wclosed-image.locale, h.wclosed-factor, h.wclosed-image.map, exts left+right=h, h.wclosed-factor-sdense,
        (Nucleus.map.surjective, \lam j p {x} => Join-univ \lam k => nucleus-unit {h.wclosed-image} <=∘ k. <=∘
          Meet-cond (later (j, \lam {P} {y} t => p $ h.wclosed-factor-sdense {P} {h.wclosed-image.map y} $ rewrite left+right=h t))))
  | unique-lift f (g : FrameHom) Lf Rg => OFS.liftFromMono {LocaleCat} f g (regularMono_Mono (surj_regular Rg.)) \lam t (s : FrameHom) gt=sf =>
      \have g<=s : g.image <= s.image => Rg. s.image \lam {P} {x} gx<=P => direct-adjoint. $ Lf (rewriteI (path (gt=sf __ x)) $ func-<= gx<=P <=∘ func-pHat>=) <=∘ func-pHat<=
      \in (hinv {surj_equiv Rg.} ∘ NucleusFrame.<=-map g.image s.image g<=s ∘ s.factor, exts \lam x => func_direct_func *> <=-antisymmetric (direct-adjoint. g<=s) (func-<= direct-unit))
  \where \open FrameHom

\type isWeaklyHausdorff (L : Locale) => isWeaklyClosed {LocaleCat.diagonal L}

-- | A weakly regular locale is weakly Hausdorff
\lemma wregular_wHausdorff {L : Locale} (reg : L.isWeaklyRegular) : isWeaklyHausdorff L
  => {?} -- [4, Corollary 3.4]

\lemma overt-fromPres {P : FramePres} (o : P.isOvert) : isOvert {PresentedFrame P}
  => \lam U {x} Ux => cover-trans (o x) \lam i => cover-inj (\lam Q p => TruncP.remove' $ TruncP.map (i _ (p Ux)) __., x, ()) idp

\lemma sdense_positive {f : FrameHom} (d : f.isStronglyDense) {x : f.Dom} (p : isPositive x) : isPositive (f x)
  => \lam P fx<=P => p P (d fx<=P)

\lemma func_positive {f : FrameHom} {x : f.Dom} (p : isPositive (f x)) : isPositive x
  => \lam P x<=P => p P (func-<= x<=P <=∘ func-Join>= <=∘ Join-univ (\lam q => top-univ <=∘ Join-cond q))

\lemma sdense_overt {f : FrameHom} (d : f.isStronglyDense) (o : isOvert {f.Cod}) : isOvert {f.Dom}
  => \lam a => d $ o _ <=∘ Join-univ (\lam h => Join-cond $ func_positive h)

\lemma sdense-fromPres {P : FramePres} {L : Locale} {f : FramePresHom P (FrameUnitalSubcat.F L)}
  (s : \Pi {Q : \Prop} {x : P} -> f x <= Join (\lam (_ : Q) => f x) -> Cover x (\lam (_ : Q) => x))
  : FrameHom.isStronglyDense {FrameReflectiveSubcat.adjointMap f}
  => \lam p {x} Ux => cover-trans (s (meet-univ <=-refl (Join-cond (later (x,Ux)) <=∘ p) <=∘ Join-ldistr>= <=∘ Join-univ (\lam q => meet-left <=∘ Join-cond q))) (\lam q => cover-inj (q,x,()) idp)

\lemma sdense-comp {L M K : Locale} (f : Hom L M) (fd : isStronglyDense {f}) (g : Hom M K) (gd : isStronglyDense {g}) : isStronglyDense {g LocaleCat.∘ f}
  => \lam p => gd (fd p)

\lemma <<-fromPres {P : FramePres} {x y : P} (x<<y : x FramePres.<< y) : embed x << {PresentedFrame P} embed y
  => \lam {J} {g} y<=Jg => \case x<<y (y<=Jg (cover-inj () idp)) \with {
       | inP (l,x<=l) => inP (map __. l, \lam c => cover-trans c \lam _ => cover-trans x<=l \lam i => cover-inj (i, (l i)., (l i).) idp)
     }

\lemma <<_<= {L : Locale} {x y : L} (x<<y : x << y) : x <= y
  => \case x<<y {\Sigma} {\lam _ => y} (Join-cond ()) \with {
       | inP (_,x<=Jy) => x<=Jy <=∘ Join-univ (\lam _ => <=-refl)
     }

\lemma <<-left {L : Locale} {x y z : L} (x<<y : x << y) (y<=z : y <= z) : x << z
  => \lam {J} {g} z<=Jg => TruncP.map (x<<y (y<=z <=∘ z<=Jg)) (\lam t => t)

\lemma <<-right {L : Locale} {x y z : L} (x<=y : x <= y) (y<<z : y << z) : x << z
  => \lam {J} {g} z<=Jg => TruncP.map (y<<z z<=Jg) (\lam t => (t., x<=y <=∘ t.))

\lemma locallyCompact-fromPres {P : FramePres} (lc : P.isLocallyCompact) : isLocallyCompact {PresentedFrame P}
  => \lam U {x} u => cover-trans (lc x) \lam t => cover-inj ((embed t., <<-left (<<-fromPres t.) (embed<= (cover-inj (x,u) idp))), t., cover-inj () idp) idp

\lemma <=<_<= {L : Locale} {x y : L} (x<=<y : x <=< y) : x <= y
  => meet-univ (top-univ <=∘ x<=<y) <=-refl <=∘ L.rdistr>= <=∘ join-univ (L.eval <=∘ bottom-univ) meet-left

\instance LocaleRatherBelow {L : Locale} : RatherBelow (L.<=<)
  | <=<_top => unfolds join-right
  | <=<-left p q => unfolds $ p <=∘ join-univ join-left (q <=∘ join-right)
  | <=<-right p q => unfolds $ q <=∘ join-univ (neg-inverse p <=∘ join-left) join-right
  | <=<_meet p q => unfolds $ meet-univ <=-refl <=-refl <=∘ MeetSemilattice.meet-monotone (unfolds in p) q <=∘ ldistr>= <=∘
      join-univ (meet-right <=∘ L.neg-inverse meet-right <=∘ join-left) (L.rdistr>= <=∘ join-univ (meet-left <=∘ L.neg-inverse meet-left <=∘ join-left) join-right)

\lemma regular-fromPres {P : FramePres} (reg : \Pi (x : P) -> FramePres.SCover x (embed __ <=< embed x)) : isRegular {PresentedFrame P}
  => \lam U {x} u => cover-trans (reg x) \lam t => cover-inj ((embed t., <=<-left t. (embed<= (cover-inj (x,u) idp))), t., cover-inj () idp) idp

-- | If {R} is a relation that satisfies conditions {basic}, {leq}, {dense}, and {comm}, then `R x y` implies `x << y`
\lemma wayBelowPredicate {P : FramePres} (R : P -> P -> \Prop) {x y : P} (Rxy : R x y) {J : \Set} {g : J -> P} (c : Cover y g)
                         (basic : \Pi {x y : P} -> R x y -> \Pi {J : \Set} {g : J -> P} -> BasicCover y g -> ∃ (l : Array J) (Cover x (\lam i => g (l i))))
                         (leq : \Pi {x y : P} -> R x y -> Cover1 x y)
                         (dense : \Pi {x z : P} -> R x z -> ∃ (y : P) (R x y) (R y z))
                         (comm : \Pi {x y : P} -> R x y -> \Pi (z : P) (l : Array P) -> Cover y (z :: l) -> ∃ (l' : Array P) (\Pi (j : Fin l'.len) -> R (l' j) z) (Cover x (l' ++ l)))
  : ∃ (l : Array J) (Cover x (\lam i => g (l i))) \elim c
  | cover-basic b => basic Rxy b
  | cover-inj j p => inP (j :: nil, cover-trans (leq Rxy) (\lam _ => cover-inj  p))
  | cover-trans {_} {f} c h =>
    \let | (inP (z,Rxz,Rzy)) => dense Rxy
         | (inP (l,z<=l)) => wayBelowPredicate R Rzy c basic leq dense comm
         | (inP (g',x<=g',Q,_)) => comm-lem R leq dense comm (DArray.len {l}) Rxz <=-refl z<=l
         | (inP S) => choice {SigmaFin (FinFin (DArray.len {l})) (\lam i => FinFin (DArray.len {g' i}))} \lam t => wayBelowPredicate R (Q t. (fin_< t.) t.) (h (l t.)) basic leq dense comm
    \in inP (Big (++) nil (\lam i => Big (++) nil (\lam j => (S (i,j)).)), cover-trans x<=g' \lam k =>
      \have (i,j,p) => split g' k
      \in rewrite p (cover-trans (S (i,j)). \lam m =>
        \have p => unsplit2 (\lam i => DArray.len {g' i}) (\lam p => (S p).) i j m
        \in cover-inj p. (pmap g p.)))
  | cover-proj1 p j q => inP (j :: nil, cover-trans (leq Rxy) \lam _ => cover-proj1 p  q)
  | cover-idemp j p => inP (j :: nil, cover-trans (leq Rxy) \lam _ => cover-idemp  p)
  | cover-comm p j q => inP (j :: nil, cover-trans (leq Rxy) \lam _ => cover-comm p  q)
  | cover-ldistr {a} {b} p {f} c h =>
    \let | (inP (b',Rb'b,x<=b')) => comm Rxy b nil (Cover.cover-proj2 p  idp)
         | (inP k) => FinSet.finiteAC \lam j => wayBelowPredicate R (Rb'b j) c basic leq dense comm
         | l' => Big (++) nil (\lam i => (k i).)
    \in inP (l', cover-trans (Cover.cover-prod (cover-trans (leq Rxy) \lam _ => cover-proj1 p () idp) (cover-inj () idp))
      \lam _ => cover-ldistr idp {\lam i => f (l' i)}
        (cover-trans (transport (\lam (l : Array P) => Cover x l.at) ++_nil x<=b') \lam i => cover-trans (k i). \lam j => \have (m,r) => unsplit (\lam j => (k j).) i j \in cover-inj m (pmap f r))
        (\lam j => h (l' j)))
  \where {
    \lemma comm-lem {P : FramePres} (R : P -> P -> \Prop)
                    (leq : \Pi {x y : P} -> R x y -> Cover1 x y)
                    (dense : \Pi {x z : P} -> R x z -> ∃ (y : P) (R x y) (R y z))
                    (comm : \Pi {x y : P} -> R x y -> \Pi (z : P) (l : Array P) -> Cover y (z :: l) -> ∃ (l' : Array P) (\Pi (j : Fin l'.len) -> R (l' j) z) (Cover x (l' ++ l)))
                    (k : Nat) {x y : P} (Rxy : R x y) {n : Nat} {g : Fin n -> P} (k<=n : k <= n) (c : Cover y g)
                    : ∃ (g' : Fin n -> Array P) (Cover x (Big (++) nil g')) (\Pi (j : Fin n) -> (j : Nat) < k -> \Pi (i : Fin (DArray.len {g' j})) -> R (g' j i) (g j)) (\Pi (j : Fin n) -> k <= j -> g' j = g j :: nil) \elim k, n
      | , _ => inP (\lam i => g i :: nil, cover-trans (leq Rxy) \lam _ => cover-trans c \lam i => transportInv (\lam (l : Array P) => Cover (g i) (\lam j => l j)) (++_singleton g) (cover-inj i idp), \lam _ => \case __ \with {}, \lam _ _ => idp)
      | _,  => inP (\case __ \with {}, cover-trans (leq Rxy) \lam _ => cover-trans c (\case __), \case __ \with {}, \case __)
      | suc k, suc n =>
        \let | (inP (z,Rxz,Rzy)) => dense Rxy
             | (inP (g',z<=g',Q,S)) => comm-lem R leq dense comm k Rzy (LinearlyOrderedSemiring.<=_+ (suc<=suc.conv k<=n) (zero<=_ {})) c
             | l => Big (++) nil (\lam i => g' (sface k i))
             | kmod=k => mod_< (id<suc <∘l k<=n)
             | (inP (l',Rl'gk,x<=l'+g')) => comm Rxz (g k) l (transport (\lam t => Cover z (t ++ l)) (S k (rewrite kmod=k <=-refl)) (cover-trans z<=g' \lam m =>
                 \have (i,j,p) => split g' m
                 \in Cover.cover-index (rewrite p (transport (\lam (x : Array P) => \Pi (j : Fin x.len) -> Index (x j) (g' k ++ l))
                                                             (pmap g' (f_sec {cyclePerm k} i))
                                                             (\lam j' => unsplit (\lam i => g' (cyclePerm k i)) (ret {cyclePerm k} i) j') j))))
             | F (j : Fin (suc n)) : Array P => \case decideEq k j \with { | yes _ => l' | no _ => g' j }
        \in inP (F,
              cover-trans x<=l'+g' \case split_++ __ \with {
                | inl (m,p) =>
                  \have s : F (k Nat.mod suc n) = l' => unfold F (rewrite (decideEq=_reduce (inv kmod=k)) idp)
                  \in transportInv (Cover __ _) p (Cover.cover-index ((rewrite s in unsplit F (k Nat.mod suc n)) m))
                | inr (m,p) =>
                  \have | (i,j,q) => split (\lam i => g' (sface k i)) m
                        | s : F (sface k i) = g' (sface k i) => unfold F (rewrite (decideEq/=_reduce {_} {k} {sface k i} (\lam p => sface-skip (fin_nat-inj (inv (kmod=k *> p))))) idp)
                  \in transportInv (Cover __ _) (p *> q) (Cover.cover-index ((rewrite s in unsplit F (sface k i)) j))
              },
              \lam j j<k+1 => unfold F (mcases \with {
                | yes k=j => rewrite (fin_nat-inj (kmod=k *> k=j)) in Rl'gk
                | no k/=j => Q j \case LinearOrder.<=-dec (<_suc_<= j<k+1) \with {
                  | inl j<k => j<k
                  | inr j=k => absurd (k/=j (inv j=k))
                }
              }),
              \lam j k+1<=j => unfold F (rewrite (decideEq/=_reduce (\lam (k=j : k = j) => <-irreflexive (id<suc <∘l (rewrite (inv k=j) in k+1<=j)))) (S j (<=-less id<suc <=∘ k+1<=j))))

    \func ++_singleton {A : \Type} (l : Array A) : Big (++) nil (map (`:: nil) l) = l \elim l
      | nil => idp
      | :: a l => pmap (a ::) (++_singleton l)

    \func split_++ {A : \Type} {l1 l2 : Array A} (k : Fin (DArray.len {l1 ++ l2}))
      : Or (\Sigma (i : Fin l1.len) ((l1 ++ l2) k = l1 i)) (\Sigma (i : Fin l2.len) ((l1 ++ l2) k = l2 i)) \elim l1, k
      | nil, k => inr (k,idp)
      | :: a l1,  => inl (,idp)
      | :: a l1, suc k => \case split_++ k \with {
        | inl (i,p) => inl (suc i, p)
        | inr (i,p) => inr (i,p)
      }

    \func split {A : \Type} {n : Nat} (g : Fin n -> Array A) (k : Fin (DArray.len {Big (++) nil (mkArray g)}))
      : \Sigma (i : Fin n) (j : Fin (DArray.len {g i})) (Big (++) nil g k = g i j) \elim n
      | suc n => \case split_++ k \with {
        | inl (j,p) => (,j,p)
        | inr (m,p) =>
          \have (i,j,q) => split (\lam i => g (suc i)) m
          \in (suc i, j, p *> q)
      }

    \func unsplit {A : \Type} {n : Nat} (S : Fin n -> Array A) (i : Fin n) (j : Fin (DArray.len {S i})) : Index (S i j) (Big (++) nil S) \elim n, i
      | suc n,  => index-left (j,idp)
      | suc n, suc i => index-right (unsplit (\lam k => S (suc k)) i j)

    \func unsplit2 {A : \Type} {n : Nat} (Q : Fin n -> Nat) (S : \Sigma (i : Fin n) (Fin (Q i)) -> Array A) (i : Fin n) (j : Fin (Q i)) (k : Fin (DArray.len {S (i,j)}))
      : Index (S (i,j) k) (Big (++) nil (\lam i => Big (++) nil (mkArray (\lam j => S (i,j))))) \elim n, i
      | suc n,  => index-left (unsplit (\lam j => S (,j)) j k)
      | suc n, suc i => index-right (unsplit2 (\lam i => Q (suc i)) (\lam p => S (suc p., p.)) i j k)

    \lemma indexing-basic {P : FramePres} {I : \Set} {h : I -> \Sigma (J : \Set) P (J -> P)} {x : P} (R : P -> P -> \Prop)
                          (p : \Pi (i : I) -> R x (h i). -> ∃ (l : Array (h i).) (Cover x (\lam j => (h i). (l j))))
                          {y : P} (Rxy : R x y) {J : \Set} {g : J -> P} (ind : FramePres.Indexing h y g) : ∃ (l : Array J) (Cover x (\lam i => g (l i)))
      => FramePres.indexing-transport (\lam {J'} y' g' =>  R x y' -> ∃ (l : Array J') (Cover x (\lam j => g' (l j)))) p ind Rxy
  }