Locales

module order-theory.locales where

open import foundation.identity-types
open import foundation.propositions
open import foundation.sets
open import foundation.universe-levels

open import order-theory.frames
open import order-theory.greatest-lower-bounds-posets
open import order-theory.least-upper-bounds-posets
open import order-theory.meet-semilattices
open import order-theory.meet-suplattices
open import order-theory.posets
open import order-theory.suplattices

Idea

A locale is an object in the opposite of the category of frames. In other words, a locale is just a frame.

Definition

Locale : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
Locale l1 l2 = Frame l1 l2

module _
  {l1 l2 : Level} (L : Locale l1 l2)
  where

  meet-suplattice-Locale : Meet-Suplattice l1 l2
  meet-suplattice-Locale = meet-suplattice-Frame L

  meet-semilattice-Locale : Meet-Semilattice l1
  meet-semilattice-Locale = meet-semilattice-Frame L

  suplattice-Locale : Suplattice l1 l1 l2
  suplattice-Locale = suplattice-Frame L

  poset-Locale : Poset l1 l1
  poset-Locale = poset-Frame L

  set-Locale : Set l1
  set-Locale = set-Frame L

  type-Locale : UU l1
  type-Locale = type-Frame L

  is-set-type-Locale : is-set type-Locale
  is-set-type-Locale = is-set-type-Frame L

  leq-Locale-Prop : (x y : type-Locale) → Prop l1
  leq-Locale-Prop = leq-Frame-Prop L

  leq-Locale : (x y : type-Locale) → UU l1
  leq-Locale = leq-Frame L

  is-prop-leq-Locale : (x y : type-Locale) → is-prop (leq-Locale x y)
  is-prop-leq-Locale = is-prop-leq-Frame L

  refl-leq-Locale : (x : type-Locale) → leq-Locale x x
  refl-leq-Locale = refl-leq-Frame L

  antisymmetric-leq-Locale :
    (x y : type-Locale) → leq-Locale x y → leq-Locale y x → x ＝ y
  antisymmetric-leq-Locale = antisymmetric-leq-Frame L

  transitive-leq-Locale :
    (x y z : type-Locale) → leq-Locale y z → leq-Locale x y → leq-Locale x z
  transitive-leq-Locale = transitive-leq-Frame L

  meet-Locale : type-Locale → type-Locale → type-Locale
  meet-Locale = meet-Frame L

  is-greatest-binary-lower-bound-meet-Locale :
    (x y : type-Locale) →
    is-greatest-binary-lower-bound-Poset poset-Locale x y (meet-Locale x y)
  is-greatest-binary-lower-bound-meet-Locale =
    is-greatest-binary-lower-bound-meet-Frame L

  associative-meet-Locale :
    (x y z : type-Locale) →
    meet-Locale (meet-Locale x y) z ＝ meet-Locale x (meet-Locale y z)
  associative-meet-Locale = associative-meet-Frame L

  commutative-meet-Locale :
    (x y : type-Locale) → meet-Locale x y ＝ meet-Locale y x
  commutative-meet-Locale = commutative-meet-Frame L

  idempotent-meet-Locale :
    (x : type-Locale) → meet-Locale x x ＝ x
  idempotent-meet-Locale = idempotent-meet-Frame L

  is-suplattice-Locale :
    is-suplattice-Poset l2 poset-Locale
  is-suplattice-Locale = is-suplattice-Frame L

  sup-Locale : {I : UU l2} → (I → type-Locale) → type-Locale
  sup-Locale = sup-Frame L

  is-least-upper-bound-sup-Locale :
    {I : UU l2} (x : I → type-Locale) →
    is-least-upper-bound-family-of-elements-Poset poset-Locale x (sup-Locale x)
  is-least-upper-bound-sup-Locale = is-least-upper-bound-sup-Frame L

  distributive-meet-sup-Locale :
    distributive-law-Meet-Suplattice meet-suplattice-Locale
  distributive-meet-sup-Locale = distributive-meet-sup-Frame L