------------------------------------------------------------------------
-- The Agda standard library
--
-- Definitions for order-theoretic lattices
------------------------------------------------------------------------
-- The contents of this module should be accessed via
-- `Relation.Binary.Lattice`.
{-# OPTIONS --cubical-compatible --safe #-}
module Relation.Binary.Lattice.Definitions where
open import Algebra.Core using (Op₁; Op₂)
open import Data.Product.Base using (_×_; _,_)
open import Function.Base using (flip)
open import Level using (Level)
open import Relation.Binary.Core using (Rel)
private
variable
a ℓ : Level
A : Set a
------------------------------------------------------------------------
-- Relationships between orders and operators
Supremum : Rel A ℓ → Op₂ A → Set _
Supremum _≤_ _∨_ =
∀ x y → x ≤ (x ∨ y) × y ≤ (x ∨ y) × ∀ z → x ≤ z → y ≤ z → (x ∨ y) ≤ z
Infimum : Rel A ℓ → Op₂ A → Set _
Infimum _≤_ = Supremum (flip _≤_)
Exponential : Rel A ℓ → Op₂ A → Op₂ A → Set _
Exponential _≤_ _∧_ _⇨_ =
∀ w x y → ((w ∧ x) ≤ y → w ≤ (x ⇨ y)) × (w ≤ (x ⇨ y) → (w ∧ x) ≤ y)
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4