Powerset sup-lattice

Powerset.agda

{-# OPTIONS --safe #-}
module Order.SupLattice.Powerset where

open import Categories.Prelude
open import Meta.Prelude
open import Foundations.Equiv.Size

open import Data.Empty
open import Data.Unit
open import Data.Sum
open import Data.List

open import Order.Diagram.Lub
open import Order.Base
open import Order.Category
open import Order.SupLattice
open import Order.SupLattice.SmallBasis
import Order.Reasoning

private variable
  ℓᵃ ℓ  : Level
  A : 𝒰 ℓᵃ
                                    
--- example 4.5

𝒫 : 𝒰 ℓᵃ → (ℓ : Level) → 𝒰 (ℓᵃ ⊔ ℓsuc ℓ)
𝒫 A ℓ = A → Prop ℓ

_⊆ᵖ_ : ∀ {ℓ ℓᵃ} {A : 𝒰 ℓᵃ} → 𝒫 A ℓ → 𝒫 A ℓ → 𝒰 (ℓᵃ ⊔ ℓ)
X ⊆ᵖ Y = ∀ a → ⌞ X a ⌟ → ⌞ Y a ⌟

@0 pposet : {ℓᵃ : Level}
          → 𝒰 ℓᵃ
          → (ℓ : Level)
          → Poset (ℓᵃ ⊔ ℓsuc ℓ) (ℓᵃ ⊔ ℓ)
pposet A ℓ .Poset.Ob                    = 𝒫 A ℓ
pposet _ _ .Poset._≤_                   = _⊆ᵖ_
pposet _ _ .Poset.≤-thin {x} {y}        = hlevel 1
pposet _ _ .Poset.≤-refl a              = id
pposet _ _ .Poset.≤-trans f g a         = g a ∘ f a
pposet _ _ .Poset.≤-antisym {x} {y} f g = fun-ext λ a → n-path (ua (prop-extₑ! (f a) (g a)))

psup : ∀ {ℓᵃ} {ℓ} {A : 𝒰 ℓᵃ} {I : 𝒰 ℓ}
     → (I → 𝒫 A ℓ) → 𝒫 A ℓ
psup {I} F x = el! (∃[ i ꞉ I ] ⌞ F i x ⌟)
     
psuplat : {ℓᵃ ℓ : Level} {A : 𝒰 ℓᵃ}
        → is-sup-lattice (pposet A ℓ) ℓ
psuplat .is-sup-lattice.sup {I}                             = psup
psuplat .is-sup-lattice.suprema {I} F .is-lub.fam≤lub i a x = ∣ i , x ∣₁
psuplat .is-sup-lattice.suprema {I} F .is-lub.least u f a   = rec! λ i → f i a

psng : {ℓᵃ : Level} {A : 𝒰 ℓᵃ}
     → is-set A
     → A → ⌞ pposet A ℓᵃ ⌟
psng sa x y = el (x ＝ y) (sa x y)

psngbas : {ℓᵃ : Level} {A : 𝒰 ℓᵃ}
        → (sa : is-set A)
        → is-basis (pposet A ℓᵃ) (psng sa) psuplat
psngbas sa .is-basis.≤-is-small x a = ⌞ x a ⌟ , prop-extₑ! (λ xa b e → subst (n-Type.carrier ∘ x) e xa) (λ f → f a refl)
psngbas sa .is-basis.↓-is-sup x .is-lub.fam≤lub i a e  = i .snd a e
psngbas sa .is-basis.↓-is-sup x .is-lub.least u f a xa = f (a , (λ b e → subst (n-Type.carrier ∘ x) e xa)) a refl

plβ : {ℓᵃ : Level} {A : 𝒰 ℓᵃ}
    → is-set A
    → List A → A → Prop ℓᵃ
plβ {ℓᵃ} sa  []      _ = el! (Lift ℓᵃ ⊥)
plβ      sa (a ∷ as) b = el! (⌞ psng sa a b ⌟ ⊎₁ ⌞ plβ sa as b ⌟)

@0 phs : ∀ {ℓᵃ} {A : 𝒰 ℓᵃ} {sa : is-set A} {x : ⌞ pposet A ℓᵃ ⌟}
       (as : List A)
    → has-size ℓᵃ ((pposet A ℓᵃ Poset.≤ plβ sa as) x)
phs {ℓᵃ}          []       = Lift ℓᵃ ⊤ , prop-extₑ! (λ _ _ x → absurd (lower x)) (λ _ → lift tt)
phs      {sa} {x} (a ∷ as) =
  let (Y , e) = phs {sa = sa} {x} as in
  ⌞ ∥ ⌞ x a ⌟ × Y ∥₁ ⌟ , prop-extₑ! (λ c b d → rec! [ (λ eq → rec! (λ xa p → subst (n-Type.carrier ∘ x) eq xa) c)
                                                    , (λ p → rec! (λ xa y → (e $ y) b p) c)
                                                    ]ᵤ d)
                                    (λ f → ∣ f a ∣ inl refl ∣₁ , (e ⁻¹ $ (λ b c → f b ∣ inr c ∣₁)) ∣₁)

@0 plistbas : {ℓᵃ : Level} {A : 𝒰 ℓᵃ}
         → (sa : is-set A)
         → is-basis (pposet A ℓᵃ) (plβ sa) psuplat
plistbas {ℓᵃ} sa .is-basis.≤-is-small x = phs {x = x}
plistbas sa .is-basis.↓-is-sup x .is-lub.fam≤lub (il  , if) a pa = if a pa
plistbas sa .is-basis.↓-is-sup x .is-lub.least u' f a xa        =
  f ((a ∷ []) , λ b c → rec! [ (λ e → subst (n-Type.carrier ∘ x) e xa)
                             , (λ v → absurd (lower v)) ]ᵤ c) a ∣ inl refl ∣₁