------------------------------------------------------------------------ -- The Agda standard library -- -- Properties of binary relations ------------------------------------------------------------------------ -- The contents of this module should be accessed via `Relation.Binary`. {-# OPTIONS --cubical-compatible --safe #-} module Relation.Binary.Core where open import Data.Product.Base using (_×_) open import Function.Base using (_on_) open import Level using (Level; _⊔_; suc) private variable a b c ℓ ℓ₁ ℓ₂ ℓ₃ : Level A : Set a B : Set b C : Set c ------------------------------------------------------------------------ -- Definitions ------------------------------------------------------------------------ -- Heterogeneous binary relations REL : Set a → Set b → (ℓ : Level) → Set (a ⊔ b ⊔ suc ℓ) REL A B ℓ = A → B → Set ℓ -- Homogeneous binary relations Rel : Set a → (ℓ : Level) → Set (a ⊔ suc ℓ) Rel A ℓ = REL A A ℓ ------------------------------------------------------------------------ -- Relationships between relations ------------------------------------------------------------------------ infix 4 _⇒_ _⇔_ _=[_]⇒_ -- Implication/containment - could also be written _⊆_. -- and corresponding notion of equivalence _⇒_ : REL A B ℓ₁ → REL A B ℓ₂ → Set _ P ⇒ Q = ∀ {x y} → P x y → Q x y _⇔_ : REL A B ℓ₁ → REL A B ℓ₂ → Set _ P ⇔ Q = P ⇒ Q × Q ⇒ P -- Generalised implication - if P ≡ Q it can be read as "f preserves P". _=[_]⇒_ : Rel A ℓ₁ → (A → B) → Rel B ℓ₂ → Set _ P =[ f ]⇒ Q = P ⇒ (Q on f) -- A synonym for _=[_]⇒_. _Preserves_⟶_ : (A → B) → Rel A ℓ₁ → Rel B ℓ₂ → Set _ f Preserves P ⟶ Q = P =[ f ]⇒ Q -- A binary variant of _Preserves_⟶_. _Preserves₂_⟶_⟶_ : (A → B → C) → Rel A ℓ₁ → Rel B ℓ₂ → Rel C ℓ₃ → Set _ _∙_ Preserves₂ P ⟶ Q ⟶ R = ∀ {x y u v} → P x y → Q u v → R (x ∙ u) (y ∙ v)