module Order.Frame where

FramesπŸ”—

record is-frame {o β„“} (P : Poset o β„“) : Type (lsuc o βŠ” β„“) where
  no-eta-equality
  open Poset P
  field
    _∩_     : Ob β†’ Ob β†’ Ob
    ∩-meets : βˆ€ x y β†’ is-meet P x y (x ∩ y)
    has-top : Top P
    ⋃       : βˆ€ {I : Type o} (k : I β†’ Ob) β†’ Ob
    ⋃-lubs  : βˆ€ {I : Type o} (k : I β†’ Ob) β†’ is-lub P k (⋃ k)

  infixr 25 _∩_

  module is-lubs {I} {k : I β†’ Ob} = is-lub (⋃-lubs k)

  open Meets ∩-meets public
  open Top has-top using (top; !) public
  open Lubs P ⋃-lubs public

  field
    ⋃-distribl : βˆ€ {I} x (f : I β†’ Ob) β†’ x ∩ ⋃ f ≑ ⋃ Ξ» i β†’ x ∩ f i

  has-meet-slat : is-meet-semilattice P
  has-meet-slat .is-meet-semilattice._∩_ = _∩_
  has-meet-slat .is-meet-semilattice.∩-meets = ∩-meets
  has-meet-slat .is-meet-semilattice.has-top = has-top

  has-join-slat : is-join-semilattice P
  has-join-slat .is-join-semilattice._βˆͺ_ = _βˆͺ_
  has-join-slat .is-join-semilattice.βˆͺ-joins = βˆͺ-joins
  has-join-slat .is-join-semilattice.has-bottom = has-bottom
record
  is-frame-hom
    {P : Poset o β„“} {Q : Poset o β„“'}
    (f : Monotone P Q)
    (P-frame : is-frame P)
    (Q-frame : is-frame Q)
    : Type (lsuc o βŠ” β„“') where

  private
    module P = Poset P
    module PαΆ  = is-frame P-frame
    module Q = Order.Reasoning Q
    module QαΆ  = is-frame Q-frame
    open is-lub

  field
    ∩-≀ : βˆ€ x y β†’ (f # x) QαΆ .∩ (f # y) Q.≀ f # (x PαΆ .∩ y)
    top-≀ : QαΆ .top Q.≀ f # PαΆ .top
    ⋃-≀ : βˆ€ {I : Type o} (k : I β†’ ⌞ P ⌟) β†’ (f # PαΆ .⋃ k) Q.≀ QαΆ .⋃ (apply f βŠ™ k)

  has-meet-slat-hom : is-meet-slat-hom f PαΆ .has-meet-slat QαΆ .has-meet-slat
  has-meet-slat-hom .is-meet-slat-hom.∩-≀ = ∩-≀
  has-meet-slat-hom .is-meet-slat-hom.top-≀ = top-≀

  open is-meet-slat-hom has-meet-slat-hom hiding (∩-≀; top-≀) public

  pres-⋃ : βˆ€ {I : Type o} (k : I β†’ ⌞ P ⌟) β†’ (f # PαΆ .⋃ k) ≑ QαΆ .⋃ (apply f βŠ™ k)
  pres-⋃ k =
    Q.≀-antisym
      (⋃-≀ k)
      (QαΆ .⋃-universal _ (Ξ» i β†’ f .pres-≀ (PαΆ .⋃-inj i)))

  pres-lubs
    : βˆ€ {I : Type o} {k : I β†’ ⌞ P ⌟} {l}
    β†’ is-lub P k l
    β†’ is-lub Q (apply f βŠ™ k) (f # l)
  pres-lubs {k = k} {l = l} l-lub .fam≀lub i = f .pres-≀ (l-lub .fam≀lub i)
  pres-lubs {k = k} {l = l} l-lub .least ub p =
    f # l              Q.β‰€βŸ¨ f .pres-≀ (l-lub .least _ PαΆ .⋃-inj) ⟩
    f # PαΆ .⋃ k         Q.β‰€βŸ¨ ⋃-≀ k ⟩
    QαΆ .⋃ (apply f βŠ™ k) Q.β‰€βŸ¨ QαΆ .⋃-universal ub p ⟩
    ub                 Q.β‰€βˆŽ

  opaque
    unfolding Lubs.βˆͺ-joins Lubs.has-bottom

    has-join-slat-hom : is-join-slat-hom f PαΆ .has-join-slat QαΆ .has-join-slat
    has-join-slat-hom .is-join-slat-hom.βˆͺ-≀ x y =
      Q.≀-trans (⋃-≀ _) $ QαΆ .⋃-universal _ Ξ» where
        (lift true) β†’ QαΆ .⋃-inj (lift true)
        (lift false) β†’ QαΆ .⋃-inj (lift false)
    has-join-slat-hom .is-join-slat-hom.bot-≀ =
      Q.≀-trans (⋃-≀ _) (QαΆ .⋃-universal _ (Ξ» ()))

  open is-join-slat-hom has-join-slat-hom public

open is-frame-hom
id-frame-hom
  : βˆ€ (PαΆ  : is-frame P)
  β†’ is-frame-hom idβ‚˜ PαΆ  PαΆ 
id-frame-hom {P = P} PαΆ  .∩-≀ x y =
  Poset.≀-refl P
id-frame-hom {P = P} PαΆ  .top-≀ =
  Poset.≀-refl P
id-frame-hom {P = P} PαΆ  .⋃-≀ k =
  Poset.≀-refl P

∘-frame-hom
  : βˆ€ {Pβ‚— Qβ‚— Rβ‚—} {f : Monotone Q R} {g : Monotone P Q}
  β†’ is-frame-hom f Qβ‚— Rβ‚—
  β†’ is-frame-hom g Pβ‚— Qβ‚—
  β†’ is-frame-hom (f βˆ˜β‚˜ g) Pβ‚— Rβ‚—
∘-frame-hom {R = R} {f = f} {g = g} f-pres g-pres .∩-≀ x y =
  R .Poset.≀-trans (f-pres .∩-≀ (g # x) (g # y)) (f .pres-≀ (g-pres .∩-≀ x y))
∘-frame-hom {R = R} {f = f} {g = g} f-pres g-pres .top-≀ =
  R .Poset.≀-trans (f-pres .top-≀) (f .pres-≀ (g-pres .top-≀))
∘-frame-hom {R = R} {f = f} {g = g} f-pres g-pres .⋃-≀ k =
  R .Poset.≀-trans (f .pres-≀ (g-pres .⋃-≀ k)) (f-pres .⋃-≀ (Ξ» i β†’ g # k i))

Frame-subcat : βˆ€ o β„“ β†’ Subcat (Posets o β„“) _ _
Frame-subcat o β„“ .Subcat.is-ob = is-frame
Frame-subcat o β„“ .Subcat.is-hom = is-frame-hom
Frame-subcat o β„“ .Subcat.is-hom-prop = hlevel!
Frame-subcat o β„“ .Subcat.is-hom-id = id-frame-hom
Frame-subcat o β„“ .Subcat.is-hom-∘ = ∘-frame-hom

Frames : βˆ€ o β„“ β†’ Precategory _ _
Frames o β„“ = Subcategory (Frame-subcat o β„“)

module Frames {o} {β„“} = Cat.Reasoning (Frames o β„“)

Frame : βˆ€ o β„“ β†’ Type _
Frame o β„“ = Frames.Ob {o} {β„“}

Power framesπŸ”—

A canonical source of frames are power sets: The power set of any type is a frame, because it is a complete lattice satisfying the infinite distributive law; This can be seen by some computation, as is done below.

open is-frame
open is-meet-semilattice

Power-frame : βˆ€ {β„“} (A : Type β„“) β†’ Frame β„“ β„“
Power-frame {β„“ = β„“} A .fst = Subsets A
Power-frame A .snd ._∩_ P Q i = P i ∧Ω Q i
Power-frame A .snd .∩-meets P Q =
  is-meet-pointwise Ξ» _ β†’ Props-has-meets (P _) (Q _)
Power-frame A .snd .has-top =
  has-top-pointwise Ξ» _ β†’ Props-has-top
Power-frame A .snd .⋃ k i = βˆƒΞ© _ (Ξ» j β†’ k j i)
Power-frame A .snd .⋃-lubs k = is-lub-pointwise _ _ Ξ» _ β†’
  Props-has-lubs Ξ» i β†’ k i _
Power-frame A .snd .⋃-distribl x f = funext Ξ» i β†’ Ξ©-ua
  (Ξ» (x , i) β†’ β–‘-map (Ξ» (y , z) β†’ _ , x , z) i)
  (Ξ» r β†’ β–‘-rec! (Ξ» { (x , y , z) β†’ y , inc (_ , z) }) r)