{- | 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 Category.Functor
\import Category.Topos.Sheaf.Site
\import Category.Topos.Sheaf.SiteHom
\import Data.Array
\import Data.Maybe
\import Equiv
\import Function
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Order.HeytingAlgebra
\import Order.Lattice
\import Order.Lattice.CompleteLattice
\import Order.PartialOrder
\import Paths
\import Paths.Meta
\import Set.Fin
\import Set.Fin.KFinSetOf
\import Set.Set
\import Topology.RatherBelow
\open MeetSemilattice
\open JoinSemilattice
\open Locale
\open CompleteLattice

\class Locale \extends CompleteLattice, HeytingAlebra, Site {
  | join x y => Join \lam z => (z = x) || (z = y)
  | join-left => Join-cond (byLeft idp)
  | join-right => Join-cond (byRight idp)
  | join-univ x<=z y<=z => Join-univ \case \elim __ \with {
    | byLeft p => transportInv (<= _) p x<=z
    | byRight p => transportInv (<= _) p y<=z
  }
  | Join-ldistr>= {C : E -> \Prop} {e : E} : e ∧ Join C <= SJoin (e ∧) C
  | ldistr>= => Join-ldistr>= <=∘ Join-univ (SetIm-elim $ later \case \elim __ \with {
    | byLeft p => transportInv (_ ∧ __ <= _) p join-left
    | byRight p => transportInv (_ ∧ __ <= _) p join-right
  })
  | isCover x C => x <= Join \lam y => \Sigma (p : y <= x) (C (y,p))
  | cover-stable {x} {y} x<=y {S} Sc =>
    inP (\lam px => ∃ (py : S) (px. <= py.),
         meet-univ <=-refl (x<=y <=∘ Sc) <=∘ Join-ldistr>= <=∘ Join-univ (SetIm-elim \lam s => Join-cond $ later (meet-left, inP (_, s., meet-right))),
         \lam (inP (py,Spy,px<=py)) => inP (py, Spy, px<=py, prop-pi))

  | Meet C => Join \lam x => ∀ {y : C} (x <= y)
  | Meet-cond Cx => Join-univ (__ Cx)
  | Meet-univ => Join-cond
  | --> x y => Join (__ ∧ x <= y)
  | <=-curry => Join-cond
  | <=-uncurry p => meet-monotone p <=-refl <=∘ meet-comm =<= Join-ldistr>= <=∘ Join-univ (SetIm-elim \lam {c} ca<=b => meet-comm =<= ca<=b)

  \lemma Join-ldistr {C : E -> \Prop} {e : E} : e ∧ Join C = SJoin (e ∧) C
    => <=-antisymmetric Join-ldistr>= $ SJoin-univ \lam Ca => meet-monotone <=-refl (Join-cond Ca)

  \lemma Join-rdistr>= {C : E -> \Prop} {e : E} : Join C ∧ e <= SJoin (∧ e) C
    => =_<= Join-rdistr

  \lemma Join-rdistr {C : E -> \Prop} {e : E} : Join C ∧ e = SJoin (∧ e) C
    => meet-comm *> Join-ldistr *> pmap (SJoin __ C) (ext \lam x => meet-comm)

  \lemma Join-distr>= {C D : E -> \Prop} : Join C ∧ Join D <= SJoin (\lam s => s. ∧ s.) (\lam s => \Sigma (C s.) (D s.))
    => Join-rdistr>= <=∘ SJoin-univ \lam {a} Ca => Join-ldistr>= <=∘ SJoin-univ \lam {b} Db => SJoin-conde (a,b) (Ca,Db)

  \lemma Join-distr {C D : E -> \Prop} : Join C ∧ Join D = SJoin (\lam s => s. ∧ s.) (\lam s => \Sigma (C s.) (D s.))
    => <=-antisymmetric Join-distr>= $ SJoin-univ $ later \lam s => meet-monotone (Join-cond s.) (Join-cond s.)

  \lemma SJoin-ldistr>= {A : \Type} {f : A -> E} {P : A -> \Prop} {e : E} : e ∧ SJoin f P <= SJoin (\lam x => e ∧ f x) P
    => Join-ldistr>= <=∘ SJoin-univ (SetIm-elim SJoin-cond)

  \lemma SJoin-ldistr {A : \Type} {f : A -> E} {P : A -> \Prop} {e : E} : e ∧ SJoin f P = SJoin (\lam x => e ∧ f x) P
    => <=-antisymmetric SJoin-ldistr>= $ SJoin-univ \lam Pa => meet-monotone <=-refl (SJoin-cond Pa)

  \lemma SJoin-rdistr>= {A : \Type} {f : A -> E} {P : A -> \Prop} {e : E} : SJoin f P ∧ e <= SJoin (\lam x => f x ∧ e) P
    => Join-rdistr>= <=∘ SJoin-univ (SetIm-elim SJoin-cond)

  \lemma SJoin-rdistr {A : \Type} {f : A -> E} {P : A -> \Prop} {e : E} : SJoin f P ∧ e = SJoin (\lam x => f x ∧ e) P
    => <=-antisymmetric SJoin-rdistr>= $ SJoin-univ \lam Pa => meet-monotone (SJoin-cond Pa) <=-refl

  \lemma SJoin-distr>= {A B : \Type} {f : A -> E} {g : B -> E} {P : A -> \Prop} {Q : B -> \Prop}
    : SJoin f P ∧ SJoin g Q <= SJoin {_} {\Sigma A B} (\lam s => f s. ∧ g s.) (\lam s => \Sigma (P s.) (Q s.))
    => SJoin-rdistr>= <=∘ SJoin-univ \lam {a} Pa => SJoin-ldistr>= <=∘ SJoin-univ \lam {b} Qb => SJoin-conde (a,b) (Pa,Qb)

  \lemma SJoin-distr {A B : \Type} {f : A -> E} {g : B -> E} {P : A -> \Prop} {Q : B -> \Prop}
    : SJoin f P ∧ SJoin g Q = SJoin {_} {\Sigma A B} (\lam s => f s. ∧ g s.) (\lam s => \Sigma (P s.) (Q s.))
    => <=-antisymmetric SJoin-distr>= $ SJoin-univ $ later \lam {s} PQs => meet-monotone (SJoin-cond PQs.) (SJoin-cond PQs.)

  \lemma IJoin-ldistr>= {J : \Type} {f : J -> E} {e : E} : e ∧ IJoin f <= IJoin (\lam x => e ∧ f x)
    => Join-ldistr>= <=∘ SJoin-univ (TSetIm-elim IJoin-cond)

  \lemma IJoin-ldistr {J : \Type} {f : J -> E} {e : E} : e ∧ IJoin f = IJoin (\lam x => e ∧ f x)
    => <=-antisymmetric IJoin-ldistr>= $ IJoin-univ \lam j => meet-monotone <=-refl (IJoin-cond j)

  \lemma IJoin-rdistr>= {J : \Type} {f : J -> E} {e : E} : IJoin f ∧ e <= IJoin (\lam x => f x ∧ e)
    => Join-rdistr>= <=∘ SJoin-univ (TSetIm-elim IJoin-cond)

  \lemma IJoin-rdistr {J : \Type} {f : J -> E} {e : E} : IJoin f ∧ e = IJoin (\lam x => f x ∧ e)
    => <=-antisymmetric IJoin-rdistr>= $ IJoin-univ \lam j => meet-monotone (IJoin-cond j) <=-refl

  \lemma IJoin-distr>= {J : \Type} {f : J -> E} {g : J -> E} : IJoin f ∧ IJoin g <= IJoin (\lam (s : \Sigma J J) => f s. ∧ g s.)
    => IJoin-rdistr>= <=∘ IJoin-univ \lam i => IJoin-ldistr>= <=∘ IJoin-univ \lam j => IJoin-cond (i,j)

  \lemma IJoin-distr {J : \Type} {f : J -> E} {g : J -> E} : IJoin f ∧ IJoin g = IJoin (\lam (s : \Sigma J J) => f s. ∧ g s.)
    => <=-antisymmetric IJoin-distr>= $ IJoin-univ \lam s => meet-monotone (IJoin-cond s.) (IJoin-cond s.)

  \type \infix  << (x y : E) => \Pi {U : E -> \Prop} -> y <= Join U -> ∃ (l : Array E) (∀ (a : l) (U a)) (x <= IJoin l)

  \protected \lemma <<-char {x y : E} : x << y <-> ∀ {U : E -> \Prop} (y <= Join U) ∃ (V : KFinSetOf E) (V ⊆ U) (x <= Join V)
    => (\lam x<<y y<=U => \case x<<y y<=U \with {
      | inP (l,l<=U,x<=l) => inP (KFinSetOf.fromArray l, unfolds $ TSetIm-elim l<=U, x<=l)
    }, \lam x<<y y<=U => \case x<<y y<=U \with {
      | inP (V,V<=U,x<=V) => \case V.enumerate \with {
        | inP (n,f,fs) => inP (\lam j => (f j)., \lam j => V<=U (f j)., x<=V <=∘ Join-univ \lam {y} Vy => \case fs (y,Vy) \with {
          | inP (j,p) => Join-cond $ inP (j, pmap __. p)
        })
      }
    })

  \lemma <<_join {a b c d : E} (a<<b : a << b) (c<<d : c << d) : a ∨ c << b ∨ d
    => <<-char. \lam bd<=U => \case <<-char. a<<b (join-left <=∘ bd<=U), <<-char. c<<d (join-right <=∘ bd<=U) \with {
      | inP (Va,Va<=U,a<=Va), inP (Vb,Vb<=U,b<=Vb) => inP (KFinSetOf.union Va Vb, ||.rec' Va<=U Vb<=U __,
        join-univ (a<=Va <=∘ Join-univ \lam Vw => Join-cond (byLeft Vw)) (b<=Vb <=∘ Join-univ \lam Vw => Join-cond (byRight Vw)))
    }

  \lemma <<_IJoin {x y : E} (x<<y : x << y) {J : \Type} {g : J -> E} (y<=g : y <= IJoin g) : ∃ (l : Array J) (x <= IJoin \lam j => g (l j))
    => \case x<<y y<=g \with {
      | inP (l,gl,x<=l) => \case FinSet.finiteAC (\lam j => gl j) \with {
        | inP h => inP (\lam j => (h j)., x<=l <=∘ IJoin-univ \lam j => inv (h j). =<= IJoin-cond j)
      }
    }

  \func IsCompactOpen (a : E) => a << a

  \lemma compact_bottom : IsCompactOpen bottom
    => \lam _ => inP (nil, \case __ \with {}, bottom-univ)

  \lemma compact_join {a b : E} (ac : IsCompactOpen a) (bc : IsCompactOpen b) : IsCompactOpen (a ∨ b)
    => <<_join ac bc

  \lemma compact_IJoin {l : Array E} (ac : \Pi (j : Fin l.len) -> IsCompactOpen (l j)) : IsCompactOpen (IJoin l) \elim l
    | nil => transport IsCompactOpen (<=-antisymmetric bottom-univ $ IJoin-univ $ later \case __) compact_bottom
    | a :: l => transport IsCompactOpen (<=-antisymmetric
      (join-univ (IJoin-cond $ later ) $ IJoin-univ \lam j => IJoin-cond $ later (suc j)) $ IJoin-univ $ later \case \elim __ \with {
        |  => join-left
        | suc j => IJoin-cond j <=∘ join-right
      }) $ compact_join (ac ) $ compact_IJoin \lam j => ac (suc j)

  \func IsCompact => IsCompactOpen top

  \type IsLocallyCompact => \Pi (x : E) -> x <= Join (<< x)

  \func IsAlgebraic => \Pi (a : E) -> a <= Join \lam b => \Sigma (b <= a) (IsCompactOpen b)

  \func IsCoherent => Given IsAlgebraic ∀ {a b : IsCompactOpen} (IsCompactOpen (a ∧ b))

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

  \lemma make<=< {x y : E} (p : top <= HeytingAlebra.neg x ∨ y) : x <=< y
    => p

  \lemma compact_<=< (c : IsCompact) {x y : E} (x<=<y : x <=< y) : x << y
    => \lam {C} y<=C => \have | top<=C' : top <= Join (\lam z => (HeytingAlebra.neg x = z) || C z)
                                => x<=<y <=∘ join-univ (Join-cond $ byLeft idp) (y<=C <=∘ Join-univ \lam Cw => Join-cond $ byRight Cw)
                              | (inP (l,h,top<=l)) => c top<=C'
                              | (inP (l',Cl',ll')) => chooseRight l {HeytingAlebra.neg x =} {C} h
                        \in inP (l', Cl', meet-univ <=-refl (top-univ <=∘ top<=l) <=∘ IJoin-ldistr>= <=∘ IJoin-univ \lam j => later \case ll' j \with {
                          | byLeft p => rewriteI p $ meet-comm =<= <=-eval <=∘ bottom-univ
                          | byRight s => rewrite s. $ meet-right <=∘ IJoin-cond s.
                        })

  \lemma compact-regular (c : IsCompact) (r : IsRegularLocale) : IsLocallyCompact
    => \lam x => r x <=∘ Join-univ \lam w<=<x => Join-cond (compact_<=< c w<=<x)

  -- | 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 x).map.wclosed-image <= {NucleusFrame _} open y

  \type IsRegularLocale => \Pi (x : E) -> x <= Join (<=< x)

  \type IsWeaklyRegularLocale => \Pi (x : E) -> x <= Join (<=<w x)

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

  \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

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

  \lemma pHat_meet>= {P Q : \Prop} : pHat P ∧ pHat Q <= pHat (\Sigma P Q)
    => Join-distr>= <=∘ SJoin-univ \lam pq => Join-cond pq

  \lemma pHat_meet {P Q : \Prop} : pHat P ∧ pHat Q = pHat (\Sigma P Q)
    => <=-antisymmetric pHat_meet>= $ meet-univ (pHat-impl __.) (pHat-impl __.)

  \lemma pHat-char {P : \Prop} {a : E} : pHat P <= a <-> (P -> top <= a)
    => (\lam P<=a p => Join-cond p <=∘ P<=a, \lam h => Join-univ \lam p => top-univ <=∘ h p)

  \lemma pHat-left {P : \Prop} {a : E} (p : a <= pHat P) : a <= IJoin (\lam (_ : P) => a)
    => meet-univ <=-refl p <=∘ Join-ldistr>= <=∘ SJoin-univ \lam p => meet-left <=∘ IJoin-cond p

  \type 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 q => p (a<=b <=∘ q)

  \lemma positive_Join (o : IsOvert) {P : E -> \Prop} (J>0 : IsPositive (Join P)) : ∃ (a : P) (IsPositive a)
    => J>0 $ Join-univ \lam {a} Pa => o a <=∘ pHat-impl \lam a>0 => inP $ later (a,Pa,a>0)
    \where
      \lemma conv {P : E -> \Prop} (p : ∃ (a : P) (IsPositive a)) : IsPositive (Join P) \elim p
        | inP (a,Pa,a>0) => \lam JP => a>0 $ Join-cond Pa <=∘ JP

  \lemma positive_SJoin (o : IsOvert) {A : \Type} {f : A -> E} {C : A -> \Prop} (J>0 : IsPositive (SJoin f C)) : ∃ (a : C) (IsPositive (f a))
    => \case positive_Join o J>0 \with {
      | inP (_, inP ((a,Ca),idp), fa>0) => inP (a,Ca,fa>0)
    }
    \where
      \lemma conv {A : \Type} {f : A -> E} {C : A -> \Prop} (p : ∃ (a : C) (IsPositive (f a))) : IsPositive (SJoin f C) \elim p
        | inP (a,Ca,fa>0) => positive_Join.conv $ inP (f a, SetIm-con Ca, fa>0)

  \lemma positive_cover {a : E} (p : IsPositive a) {C : E -> \Prop} (c : a <= Join C) : ∃ C
    => p $ c <=∘ Join-univ \lam {b} Cb => Join-cond (inP $ later (b,Cb))

  \func IsOvert => \Pi (a : E) -> a <= pHat (IsPositive a)

  \lemma IsOvert_IJoin (o : IsOvert) {a : E} : a <= IJoin (\lam (_ : IsPositive a) => a)
    => meet-univ <=-refl (o a) <=∘ Join-ldistr>= <=∘ Join-univ (SetIm-elim \lam a>0 => meet-left <=∘ IJoin-cond a>0)

  \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 C => (SJoin __. C, SJoin-univ \lam {s} _ => s.)
    | Join-cond Cx => SJoin-cond Cx
    | Join-univ => SJoin-univ
    | Join-ldistr>= => SJoin-ldistr>= <=∘ SJoin-univ \lam {s} Cs => SJoin-cond (SetIm-con Cs)
    \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>= => Join-rdistr>= <=∘ SJoin-univ \lam {b} Cb => SJoin-cond (SetIm-con Cb)

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

      \lemma compact-char {b : restrict a} : (restrict a).IsCompactOpen b <-> IsCompactOpen b.
        => (\lam bc {U} b<=U => \case bc {\lam x => ∃ (y : U) (x. <= y)} (meet-univ <=-refl b<=U <=∘ Join-ldistr>= <=∘ SJoin-univ \lam {c} Uc => SJoin-conde (later (b. ∧ c, meet-left <=∘ b.)) $ inP $ later (c, Uc, meet-right)) \with {
          | inP (l,l<=U,b<=l) => \case FinSet.finiteAC l<=U \with {
            | inP g => inP (\lam j => (g j)., \lam j => (g j)., b<=l <=∘ Join-univ (SetIm-elim $ TSetIm-elim \lam j => (g j). <=∘ IJoin-cond j))
          }
        }, \lam bc {U} b<=U => \case bc {\lam x => \Sigma (p : x <= a) (U (x,p))} (b<=U <=∘ SJoin-univ \lam {c} Uc => Join-cond $ later (c., Uc)) \with {
          | inP (l,l<=U,b<=l) => inP (\new Array (restrict a) l.len \lam j => (l j, (l<=U j).), \lam j => (l<=U j)., b<=l <=∘ IJoin-univ \lam j => SJoin-cond (TSetIm-con j))
        })
    }
}

\record FrameHom \extends PosetHom {
  \override Dom : Locale
  \override Cod : Locale
  | 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 {C : Dom -> \Prop} : func (Join C) = SJoin func C
  | func-Join>= {C : Dom -> \Prop} : func (Join C) <= SJoin func C

  \default func-Join>= => =_<= func-Join
  \default func-Join => <=-antisymmetric func-Join>= $ SJoin-univ \lam Ca => func-<= (Join-cond Ca)
  \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-SJoin>= {A : \Type} {f : A -> Dom} {P : A -> \Prop} : func (SJoin f P) <= SJoin (\lam a => func (f a)) P
    => func-Join>= <=∘ SJoin-univ (SetIm-elim SJoin-cond)

  \lemma func-SJoin {A : \Type} {f : A -> Dom} {P : A -> \Prop} : func (SJoin f P) = SJoin (\lam a => func (f a)) P
    => <=-antisymmetric func-SJoin>= $ SJoin-univ \lam Pa => func-<= (SJoin-cond Pa)

  \lemma func-IJoin>= {J : \Type} {f : J -> Dom} : func (IJoin f) <= IJoin (\lam a => func (f a))
    => func-Join>= <=∘ SJoin-univ (TSetIm-elim IJoin-cond)

  \lemma func-IJoin {J : \Type} {f : J -> Dom} : func (IJoin f) = IJoin (\lam a => func (f a))
    => <=-antisymmetric func-IJoin>= $ IJoin-univ \lam a => func-<= (IJoin-cond a)

  \lemma func-join>= {x y : Dom} : func (x ∨ y) <= func x ∨ func y
    => func-Join>= <=∘ SJoin-univ (later \case \elim __ \with {
      | byLeft p => rewrite p join-left
      | byRight p => rewrite p join-right
    })

  \lemma func-join {x y : Dom} : func (x ∨ y) = func x ∨ func y
    => <=-antisymmetric func-join>= $ join-univ (func-<= join-left) (func-<= join-right)

  \lemma func-bottom>= : func bottom <= bottom
    => func-Join>= <=∘ SJoin-univ (later \case __)

  \lemma func-bottom : func bottom = bottom
    => <=-antisymmetric func-bottom>= bottom-univ

  \lemma func-pHat<= {P : \Prop} : pHat P <= func (pHat P)
    => Join-univ \lam p => top-univ <=∘ func-top>= <=∘ func-<= (Join-cond p)

  \lemma func-pHat>= {P : \Prop} : func (pHat P) <= pHat P
    => func-Join>= <=∘ SJoin-univ \lam p => Join-cond p

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

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

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

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

  \lemma direct-counit {y : Cod} : func (direct y) <= y
    => func-Join>= <=∘ SJoin-univ \lam p => p

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

  \lemma direct-top : direct top = top
    => <=-antisymmetric top-univ (Join-cond 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-SJoin>=

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

  \lemma dense_direct (d : IsDense) : direct bottom <= bottom
    => Join-univ d

  \lemma direct_dense (d : direct bottom <= bottom) : IsDense
    => \lam p => Join-cond 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 => SMeet (\lam (j : Nucleus _) => j x) \lam j => \Pi {P : \Prop} {x : Dom} -> func x <= pHat P -> x <= j (pHat P)
    | nucleus-<= p => SMeet-univ \lam f => SMeet-cond f <=∘ nucleus-<= p
    | nucleus-meet>= => SMeet-univ \lam f => meet-monotone (SMeet-cond f) (SMeet-cond f) <=∘ nucleus-meet>=
    | nucleus-unit => SMeet-univ \lam _ => nucleus-unit
    | nucleus-join>= => SMeet-univ \lam f => SMeet-cond f <=∘ nucleus-<= (SMeet-cond f) <=∘ 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. (SMeet-cond {_} {_} {_} {_} {image} $ later \lam hx<=P => direct-adjoint. (hx<=P <=∘ func-pHat<=)) <=∘ func-SJoin>=

  \lemma wclosed-factor-sdense : wclosed-factor.IsStronglyDense
    => \lam c => SMeet-univ (later \lam H => H c) <=∘ =_<= (inv wclosed-image.locale_pHat)

  -- | A map is closed if and only if the image of a closed sublocale is closed.
  \protected \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) : IsEquiv factor => inP \new QEquiv {
    | ret y => (direct y, direct-<= direct-counit)
    | ret_f x => ext (<=-antisymmetric x. direct-unit)
    | f_sec y => surjective-split s y
  }

  \protected \func functor : SiteHom Dom Cod \cowith
    | F => func
    | Func => func-<=
    | Func-id => idp
    | Func-o => idp
    | Func-cover p => Covering.covering-basic $ func-<= p <=∘ func-Join>= <=∘ SJoin-univ \lam s => Join-cond $ later (func-<= s., inP (_, s., idp))
    | Func-flat-terminal => Covering.covering-id $ inP (top, top-univ <=∘ func-top>=)
    | Func-flat-pullback {x} {y1} {y2} {y1<=x} {y2<=x} {u} {u<=Fy1} {u<=Fy2} _ => Covering.covering-id $ inP (y1 ∧ y2, meet-left, meet-right, prop-pi, meet-univ u<=Fy1 u<=Fy2 <=∘ func-meet>=, prop-pi, prop-pi)
} \where {
  \protected \func id {L : Locale} : FrameHom L L \cowith
    | func x => x
    | func-top => idp
    | func-meet => idp
    | func-Join => Join_SJoin

  \protected \func compose \alias \infixl  ∘ {L M K : Locale} (g : FrameHom M K) (f : FrameHom L M) : FrameHom L K \cowith
    | 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 => pmap g func-Join *> func-SJoin

  \protected \lemma id-left {L M : Locale} {f : FrameHom L M} : id ∘ f = f
    => idp

  \protected \lemma id-right {L M : Locale} {f : FrameHom L M} : f ∘ id = f
    => idp

  \lemma direct_o {L M K : Locale} (f : FrameHom L M) (g : FrameHom M K) {x : K} : direct {g ∘ f} x = f.direct (g.direct x)
    => <=-antisymmetric (direct-adjoint. $ direct-adjoint. $ later $ direct-counit {g ∘ f}) $
        (direct-adjoint {g ∘ f}). $ g.func-<= direct-counit <=∘ direct-counit
}

\func LocaleHom (L M : Locale) => FrameHom M L
  \where {
    \func id {L : Locale} : LocaleHom L L
      => FrameHom.id

    \func compose \alias \infixl  ∘ {L M K : Locale} (g : LocaleHom M K) (f : LocaleHom L M) : LocaleHom L K
      => f FrameHom.∘ g
  }

-- | 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
    => <=-curry $ meet-monotone <=-refl nucleus-unit <=∘ nucleus-meet>= <=∘ nucleus-<= L.<=-eval <=∘ p

  \lemma exponent-func {x y : L} : x --> y <= nucleus x --> nucleus y
    => Join-univ \lam p => <=-curry $ 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 C => (nucleus $ SJoin (later __.) C, nucleus-join>=)
    | Join-cond Cx => SJoin-cond Cx <=∘ nucleus-unit
    | Join-univ {C} {e} c => nucleus-<= (SJoin-univ c) <=∘ e.
    | Join-ldistr>= => meet-monotone nucleus-unit <=-refl <=∘ nucleus-meet>= <=∘ nucleus-<= (SJoin-ldistr>= <=∘ SJoin-univ \lam Ca => SJoin-cond $ SetIm-con Ca)

  \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 Cw => nucleus-unit <=∘ SJoin-cond (SetIm-con Cw)
    \where {
      \lemma surjective : IsSurj map
        => \lam y => inP (y., ext $ <=-antisymmetric y. nucleus-unit)
    }

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

  \protected \func lift {M : Locale} (f : LocaleHom M L) (f<=j : \Pi {x : L} -> f (nucleus x) <= f x) : LocaleHom M locale \cowith
    | func s => f s.
    | func-Join>= => f<=j <=∘ func-SJoin>=
    | func-meet => func-meet
    | func-top>= => func-top>=

  \protected \lemma lift_map {M : Locale} {f : LocaleHom M L} (f<=j : \Pi {x : L} -> f (nucleus x) <= f x) : map LocaleHom.∘ lift f f<=j = f
    => exts \lam x => <=-antisymmetric f<=j (func-<= nucleus-unit)

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

  \lemma locale_pHat {P : \Prop} : (locale.pHat P). = nucleus (pHat P)
    => pmap nucleus $ <=-antisymmetric (SJoin-univ \lam p => Join-cond p) $ Join-univ \lam p => top-univ <=∘ SJoin-conde (later (top,top-univ)) p

  \lemma locale_IJoin {J : \Type} {g : J -> Subtype} : (locale.IJoin g). = nucleus (IJoin \lam j => (g j).)
    => pmap nucleus $ <=-antisymmetric (SJoin-univ $ TSetIm-elim IJoin-cond) (IJoin-univ \lam j => SJoin-cond $ TSetIm-con j)

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

  \protected \func IsDense => nucleus bottom <= bottom
} \where {
  \protected \func exp {L : Locale} (j j' : Nucleus L) : Nucleus L \cowith
    | nucleus x => SMeet (\lam y => j y --> j' y) (x <=)
    | nucleus-meet>= {a} {b} =>
      \have lem {x y z : L} : (x ∧ y) ∧ z = (x ∧ z) ∧ (y ∧ z) => equation
      \in SMeet-univ \lam {c} ab<=c => meet-monotone (SMeet-cond join-left) (SMeet-cond join-left) <=∘
        <=-curry (lem =<= meet-monotone (meet-monotone <=-refl (nucleus-<= join-right) <=∘ L.<=-eval) (meet-monotone <=-refl (nucleus-<= join-right) <=∘ L.<=-eval) <=∘
                                 nucleus-meet>= <=∘ nucleus-<= (ldistr>= <=∘ join-univ (L.rdistr>= <=∘ join-univ ab<=c meet-left) meet-right))
    | nucleus-<= x<=y => SMeet-univ \lam y<=a => SMeet-cond (x<=y <=∘ y<=a)
    | nucleus-unit => SMeet-univ \lam x<=a => later $ <=-curry $ meet-left <=∘ x<=a <=∘ nucleus-unit
    | nucleus-join>= => SMeet-univ \lam x<=a => SMeet-cond (SMeet-cond x<=a) <=∘ L.exponent-monotone <=-refl (Nucleus.nucleus_exponent nucleus-join>=) <=∘
        inv L.curry =<= later (L.exponent-monotone (meet-univ (nucleus-<= $ <=-curry $ meet-left <=∘ nucleus-unit) <=-refl) <=-refl)

  \protected \lemma exp-univ1 {L : Locale} {j k n : Nucleus L} (p : \Pi {x : L} -> (NucleusFrame L).join j k x <= n x) {x : L} : j x <= exp k n x
    => SMeet-univ \lam x<=a => later $ <=-curry $ meet-monotone (nucleus-<= x<=a) <=-refl <=∘ SMeet-univ (later \lam {m} => \case \elim m, \elim __ \with {
      | _, byLeft idp => meet-left
      | _, byRight idp => meet-right
    }) <=∘ p

  \protected \lemma exp-univ2 {L : Locale} {k n : Nucleus L} {x y : L} (p : y <= exp k n x) : y ∧ k x <= n x
    => <=-uncurry $ p <=∘ SMeet-cond <=-refl

  \lemma open_exp {L : Locale} {a : L} (x y : (open a).locale) : (x --> {(open a).locale} y). = x. --> y.
    => <=-antisymmetric
      (Join-univ \lam p => <=-curry $ <=-curry ((meet-assoc *> pmap (_ ∧) meet-comm *> inv meet-assoc) =<= meet-monotone p <=-refl <=∘ SJoin-rdistr>= <=∘ SJoin-univ \lam p => p) <=∘ y.)
      (Join-univ \lam {w} p => <=-curry $ <=-curry (meet-left <=∘ meet-left) <=∘ SJoin-conde (later (a --> w, nucleus-join>=)) (<=-curry (meet-univ (meet-monotone meet-left <=-refl <=∘ L.<=-eval) (meet-left <=∘ meet-right) <=∘ p) <=∘ y.))

  \lemma open-isOpen {L : Locale} (a : L) : (open a).map.IsOpen
    => \lam x => inP (a ∧ x., \lam y => rewrite Nucleus.map_direct $ open_exp x (a --> y, nucleus-join>=) *> inv L.curry *> pmap (__ --> y) meet-comm)

  \lemma open_IsPositive {L : Locale} {a : L} {b : (open a).locale} : IsPositive (b. ∧ a) <-> (open a).locale.IsPositive b
    => (\lam ba>0 b<=P => ba>0 $ <=-uncurry $ b<=P <=∘ =_<= (open a).locale_pHat,
        \lam b>0 ba<=P => b>0 $ <=-curry ba<=P L.<=∘ =_<= (inv (open a).locale_pHat))

  \lemma open_IsOvert {L : Locale} (Lo : L.IsOvert) {a : L} : (open a).locale.IsOvert
    => \lam b => unfolds $ <=-curry (Lo _ <=∘ pHat-impl open_IsPositive.) <=∘ =_<= (inv (open a).locale_pHat)

  \func idNucleus {L : Locale} : Nucleus L \cowith
    | nucleus x => x
    | nucleus-unit => <=-refl
    | nucleus-join>= => <=-refl
    | nucleus-meet => idp

  \func topNucleus {L : Locale} : Nucleus L \cowith
    | nucleus x => top
    | nucleus-<= _ => top-univ
    | nucleus-unit => top-univ
    | nucleus-join>= => top-univ
    | nucleus-meet>= => top-univ
}

\instance NucleusFrame (L : Locale) : CompleteLattice (Nucleus L)
  | <= j j' => \Pi {x : L} -> j' x <= j x
  | <=-refl => <=-refl
  | <=-transitive p q {x} => <=-transitive q p
  | <=-antisymmetric p q => exts (\lam x => <=-antisymmetric q p)
  | Join C => \new Nucleus L {
    | nucleus x => SMeet (\lam (j : Nucleus L) => j x) C
    | nucleus-<= x<=y => SMeet-univ \lam Ca => SMeet-cond Ca <=∘ nucleus-<= x<=y
    | nucleus-meet>= => SMeet-univ \lam Ca => meet-monotone (SMeet-cond Ca) (SMeet-cond Ca) <=∘ nucleus-meet>=
    | nucleus-unit => SMeet-univ \lam Ca => nucleus-unit
    | nucleus-join>= => SMeet-univ \lam Ca => SMeet-cond Ca <=∘ nucleus-<= (SMeet-cond Ca) <=∘ nucleus-join>=
  }
  | Join-cond {C} {j} Cj {x} => SMeet-cond Cj
  | Join-univ h {x} => SMeet-univ \lam Ca => h Ca
  \where {
    \open Topology.Locale(NucleusFrame)

    \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-<= (SJoin-univ \lam Ca => nucleus-unit <=∘ SJoin-cond (SetIm-con Ca))
      \where
        \lemma surjective (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} (k<=j : k <= j) (x : L) : k (j x) = k x
      => <=-antisymmetric (k.nucleus-univ k<=j) (nucleus-<= nucleus-unit)

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

    \lemma wclosure_<= {j : Nucleus} : j <= {NucleusFrame _} j.map.wclosed-image
      => \lam {x} => SMeet-cond $ later \lam p => nucleus-unit <=∘ p <=∘ nucleus-<= (SJoin-univ \lam p => Join-cond p)

    \lemma wclosure-sdense {j : Nucleus} : IsStronglyDense {<=-map j.map.wclosed-image j wclosure_<=}
      => wclosed-factor-sdense

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

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

\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 L.<=-eval
  \where
    \lemma conv {L : Locale} {c a : L} (p : closed c <= open a) : top <= c ∨ a
      => L.top_exponent <=-refl <=∘ p

\lemma open<=closed {L : Locale} {c a : L} (p : c ∧ a <= bottom) : open a <= closed c
  => \lam {x} => unfold (join-univ (<=-curry (p <=∘ bottom-univ)) (<=-curry meet-left))
  \where
    \lemma conv {L : Locale} {c a : L} (p : open a <= closed c) : c ∧ a <= bottom
      => meet-monotone join-left <=-refl <=∘ <=-uncurry 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 {C} top<=C =>
      \let | g (j : Maybe (Given C)) : L => \case \elim j \with { | nothing => N bottom | just j => j.. }
           | top<=g : top <= IJoin g => top<=C <=∘ c <=∘ join-univ (IJoin-cond nothing) (SJoin-univ \lam {a} Ca => IJoin-cond $ just $ later (a,Ca))
           | (inP (l,a<=gl)) => <<_IJoin w top<=g
           | l' => filterMap (\lam x => x) l
      \in inP (map __. l', \lam j => (l' j)., unfold $ L.top_exponent a<=gl <=∘ b <=∘ N.nucleus-univ (IJoin-univ \lam j' => later $ cases (l j' arg addPath) \with {
        | nothing, _ => N.nucleus-<= bottom-univ
        | just j, p => \have (k,q) => filterMap-index (\lam x => x) l p
                       \in rewriteI q (IJoin-cond k) <=∘ nucleus-unit
      }) <=∘ =_<= (inv N.locale_IJoin))

\func discreteLocale (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 C x => ∃ (U : C) (U x)
  | Join-cond {C} {U} CU Ux => inP (U,CU,Ux)
  | Join-univ {C} {W} p (inP (U,CU,Ux)) => p CU Ux
  | Join-ldistr>= {C} {W} (Wx, inP (U,CU,Ux)) => inP (\lam x => \Sigma (W x) (U x), SetIm-con CU, (Wx,Ux))
  \where {
    \lemma exponent {X : \Set} (P Q : X -> \Prop) : P --> {discreteLocale X} Q = (\lam x => P x -> Q x)
      => ext \lam x => ext (\lam (inP (U,UP<=Q,Ux)) Px => UP<=Q (Ux,Px), \lam P=>Q => inP (\lam x => P x -> Q x, \lam p => p. p., P=>Q))

    \func terminalMap (L : Locale) : FrameHom (discreteLocale (\Sigma)) L \cowith
      | func P => pHat (P ())
      | func-<= p => pHat-impl p
      | func-top>= => Join-cond ()
      | func-meet>= => pHat_meet>=
      | func-Join>= => pHat-char. $ later \lam (inP (P,CP,p)) => Join-cond p <=∘ SJoin-cond CP
  }

\open FrameHom

-- | 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 <-> (discreteLocale.terminalMap L).IsOpen
  => (\lam o a => inP (\lam _ => IsPositive a, \lam P => ext \lam _ => propExt
        (\lam (inP (Q,Q<=a-->P,q)) => inP (\lam _ => \Sigma, \lam (_,a>0) => a>0 $ meet-univ (Join-cond q) <=-refl <=∘ <=-uncurry Q<=a-->P, ()))
        (\lam (inP (Q,a<=P,q)) => inP (Q, <=-curry $ meet-right <=∘ L.IsOvert_IJoin o <=∘ IJoin-univ \lam a>0 => Join-cond $ a<=P $ later (q,a>0), q))),
      \lam o a => \case o a \with {
        | inP (P,h) => \case propExt.conv (path \lam i => h P i ()) (inP (\lam _ => \Sigma, __., ())) \with {
          | inP (Q,t,q) => meet-univ (Join-cond q) <=-refl <=∘ <=-uncurry t <=∘ unfold (pHat-impl $ later \lam p {R} a<=R => later \case propExt.dir (path \lam i => h (\lam _ => R) i ()) $ inP (\lam _ => \Sigma, <=-curry $ meet-right <=∘ a<=R, ()) \with {
            | inP (S,SP<=R,s) => SP<=R (s,p)
          })
        }
      })

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

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

\lemma direct_positive {f : FrameHom} (d : f.IsStronglyDense) {x : f.Cod} (p : IsPositive (f.direct x)) : IsPositive x
  => positive_<= (sdense_positive d p) direct-counit

\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 <<_<= {L : Locale} {x y : L} (x<<y : x << y) : x <= y
  => \case x<<y {= y} (Join-cond idp) \with {
    | inP (l,h,x<=l) => x<=l <=∘ IJoin-univ \lam j => =_<= (h j)
  }

\lemma <<-left {L : Locale} {x y z : L} (x<<y : x << y) (y<=z : y <= z) : x << z
  => \lam z<=C => x<<y (y<=z <=∘ z<=C)

\lemma <<-right {L : Locale} {x y z : L} (x<=y : x <= y) (y<<z : y << z) : x << z
  => \lam z<=C => \case y<<z z<=C \with {
    | inP (l,h,y<=l) => inP (l, h, x<=y <=∘ y<=l)
  }

\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 (L.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)