PO.agda

module PO where

open import Level
open import Relation.Binary
open import Data.Product

module Propaties {a ℓ₁ ℓ₂} {A : Set a} {_≈_ : Rel A ℓ₁} {_≤_ : Rel A ℓ₂} (po : IsPartialOrder _≈_ _≤_ ) where

  data lower-bound-of_is_ (P : A → Set ℓ₂) : A → Set (a ⊔ ℓ₂) where
    lb : ∀ {x} → P x → (∀ x' → P x' → x ≤ x') → lower-bound-of P is x

  data _is_∨_ : A → A → A → Set (a ⊔ ℓ₂) where
    join : ∀ {x y z} → lower-bound-of (λ x' → y ≤ x' × z ≤ x') is x → x is y ∨ z