------------------------------------------------------------------------ -- The Agda standard library -- -- Properties of binary relations ------------------------------------------------------------------------ -- The contents of this module should be accessed via `Relation.Binary`. {-# OPTIONS --without-K --safe #-} module Relation.Binary.Core where open import Data.Product 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) ------------------------------------------------------------------------ -- Relationships between a binary relation and a unary operation ------------------------------------------------------------------------ Contractive : Rel A (A A) Set _ Contractive _≤_ f = {x} f x x Extensive : Rel A (A A) Set _ Extensive _≤_ f = {x} x f x Idempotent₁ : Rel A (A A) Set _ Idempotent₁ _≈_ f = {x} f (f x) f x -- cf. Algebra.Definitions.{_IdempotentOn_,Idempotent,IdempotentFun} -- Idempotent₁ is essentially the same as IdempotentFun except that -- here we can specify the relation `_≈_` "in place" instead of having -- to do `open import Algebra.Definitions (_≈_)` ahead of time.