------------------------------------------------------------------------ -- 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.Definitions where open import Agda.Builtin.Equality using (_≡_) open import Data.Maybe.Base using (Maybe) open import Data.Product using (_×_) open import Data.Sum.Base using (_⊎_) open import Function.Base using (_on_; flip) open import Level open import Relation.Binary.Core open import Relation.Nullary using (Dec; ¬_) private variable a b c ℓ₁ ℓ₂ ℓ₃ : Level A : Set a B : Set b C : Set c ------------------------------------------------------------------------ -- Definitions ------------------------------------------------------------------------ -- Reflexivity - defined without an underlying equality. It could -- alternatively be defined as `_≈_ ⇒ _∼_` for some equality `_≈_`. -- Confusingly the convention in the library is to use the name "refl" -- for proofs of Reflexive and `reflexive` for proofs of type `_≈_ ⇒ _∼_`, -- e.g. in the definition of `IsEquivalence` later in this file. This -- convention is a legacy from the early days of the library. Reflexive : Rel A Set _ Reflexive _∼_ = {x} x x -- Generalised symmetry. Sym : REL A B ℓ₁ REL B A ℓ₂ Set _ Sym P Q = P flip Q -- Symmetry. Symmetric : Rel A Set _ Symmetric _∼_ = Sym _∼_ _∼_ -- Generalised transitivity. Trans : REL A B ℓ₁ REL B C ℓ₂ REL A C ℓ₃ Set _ Trans P Q R = {i j k} P i j Q j k R i k TransCycle : REL A B ℓ₁ REL B C ℓ₂ REL C A ℓ₃ Set _ TransCycle P Q R = {i j k} P i j Q j k R k i -- A flipped variant of generalised transitivity. TransFlip : REL A B ℓ₁ REL B C ℓ₂ REL A C ℓ₃ Set _ TransFlip P Q R = {i j k} Q j k P i j R i k -- Transitivity. Transitive : Rel A Set _ Transitive _∼_ = Trans _∼_ _∼_ _∼_ -- Generalised antisymmetry Antisym : REL A B ℓ₁ REL B A ℓ₂ REL A B ℓ₃ Set _ Antisym R S E = {i j} R i j S j i E i j -- Antisymmetry. Antisymmetric : Rel A ℓ₁ Rel A ℓ₂ Set _ Antisymmetric _≈_ _≤_ = Antisym _≤_ _≤_ _≈_ -- Irreflexivity - this is defined terms of the underlying equality. Irreflexive : REL A B ℓ₁ REL A B ℓ₂ Set _ Irreflexive _≈_ _<_ = {x y} x y ¬ (x < y) -- Asymmetry. Asymmetric : Rel A Set _ Asymmetric _<_ = {x y} x < y ¬ (y < x) -- Generalised connex - exactly one of the two relations holds. Connex : REL A B ℓ₁ REL B A ℓ₂ Set _ Connex P Q = x y P x y Q y x -- Totality. Total : Rel A Set _ Total _∼_ = Connex _∼_ _∼_ -- Generalised trichotomy - exactly one of three types has a witness. data Tri (A : Set a) (B : Set b) (C : Set c) : Set (a b c) where tri< : ( a : A) (¬b : ¬ B) (¬c : ¬ C) Tri A B C tri≈ : (¬a : ¬ A) ( b : B) (¬c : ¬ C) Tri A B C tri> : (¬a : ¬ A) (¬b : ¬ B) ( c : C) Tri A B C -- Trichotomy. Trichotomous : Rel A ℓ₁ Rel A ℓ₂ Set _ Trichotomous _≈_ _<_ = x y Tri (x < y) (x y) (x > y) where _>_ = flip _<_ -- Generalised maximum element. Max : REL A B B Set _ Max _≤_ T = x x T -- Maximum element. Maximum : Rel A A Set _ Maximum = Max -- Generalised minimum element. Min : REL A B A Set _ Min R = Max (flip R) -- Minimum element. Minimum : Rel A A Set _ Minimum = Min -- Unary relations respecting a binary relation. _⟶_Respects_ : (A Set ℓ₁) (B Set ℓ₂) REL A B ℓ₃ Set _ P Q Respects _∼_ = {x y} x y P x Q y -- Unary relation respects a binary relation. _Respects_ : (A Set ℓ₁) Rel A ℓ₂ Set _ P Respects _∼_ = P P Respects _∼_ -- Right respecting - relatedness is preserved on the right by equality. _Respectsʳ_ : REL A B ℓ₁ Rel B ℓ₂ Set _ _∼_ Respectsʳ _≈_ = {x} (x ∼_) Respects _≈_ -- Left respecting - relatedness is preserved on the left by equality. _Respectsˡ_ : REL A B ℓ₁ Rel A ℓ₂ Set _ P Respectsˡ _∼_ = {y} (flip P y) Respects _∼_ -- Respecting - relatedness is preserved on both sides by equality _Respects₂_ : Rel A ℓ₁ Rel A ℓ₂ Set _ P Respects₂ _∼_ = (P Respectsʳ _∼_) × (P Respectsˡ _∼_) -- Substitutivity - any two related elements satisfy exactly the same -- set of unary relations. Note that only the various derivatives -- of propositional equality can satisfy this property. Substitutive : Rel A ℓ₁ (ℓ₂ : Level) Set _ Substitutive {A = A} _∼_ p = (P : A Set p) P Respects _∼_ -- Decidability - it is possible to determine whether a given pair of -- elements are related. Decidable : REL A B Set _ Decidable _∼_ = x y Dec (x y) -- Weak decidability - it is sometimes possible to determine if a given -- pair of elements are related. WeaklyDecidable : REL A B Set _ WeaklyDecidable _∼_ = x y Maybe (x y) -- Propositional equality is decidable for the type. DecidableEquality : (A : Set a) Set _ DecidableEquality A = Decidable {A = A} _≡_ -- Irrelevancy - all proofs that a given pair of elements are related -- are indistinguishable. Irrelevant : REL A B Set _ Irrelevant _∼_ = {x y} (a b : x y) a b -- Recomputability - we can rebuild a relevant proof given an -- irrelevant one. Recomputable : REL A B Set _ Recomputable _∼_ = {x y} .(x y) x y -- Universal - all pairs of elements are related Universal : REL A B Set _ Universal _∼_ = x y x y -- Non-emptiness - at least one pair of elements are related. record NonEmpty {A : Set a} {B : Set b} (T : REL A B ) : Set (a b ) where constructor nonEmpty field {x} : A {y} : B proof : T x y ------------------------------------------------------------------------ -- DEPRECATED NAMES ------------------------------------------------------------------------ -- Please use the new names as continuing support for the old names is -- not guaranteed. -- Version 1.1 Conn = Connex {-# WARNING_ON_USAGE Conn "Warning: Conn was deprecated in v1.1. Please use Connex instead." #-}