Legacy.Base.Relations.Properties

Properties of binary predicates

This is the Legacy.Base.Relations.Properties module of the Agda Universal Algebra Library.

{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Legacy.Base.Relations.Properties where

-- imports from Agda and the Agda Standard Library  ---------------------------------------
open import Agda.Primitive        using () renaming ( Set to Type )
open import Data.Product          using ( _,_ ; _×_ )
open import Data.Sum.Base         using ( _⊎_ )
open import Level                 using ( Level )
open import Relation.Binary.Core  using ( ) renaming ( REL to BinREL ; Rel to BinRel )
open import Relation.Unary        using ( Pred ; _∈_ ; _∉_ )
open import Relation.Binary.PropositionalEquality
                                  using ( _≡_ )

private variable
 a b c α β γ ℓ : Level
 A : Set a
 B : Set b
 C : Set c

curry : Pred(A × B) ℓ → BinREL A B ℓ
curry P x y = (x , y) ∈ P

uncurry : BinREL A B ℓ → Pred(A × B) ℓ
uncurry _≈_ (a , b) = a ≈ b

Reflexive : Pred (A × A) ℓ → Type _
Reflexive P = ∀ {x} → (x , x) ∈ P

-- Generalised symmetry
Sym : Pred (A × B) α → Pred (B × A) β → Type _
Sym P Q = ∀ {x y} → (x , y) ∈ P → (y , x) ∈ Q

-- Symmetry
Symmetric : Pred (A × A) ℓ → Type _
Symmetric P = Sym P P

-- Generalised transitivity.
Trans : Pred (A × B) α → Pred (B × C) β → Pred (A × C) γ → Type _
Trans P Q R = ∀ {i j k} → P (i , j) → Q (j , k) → R (i , k)

-- A flipped variant of generalised transitivity.
TransFlip : Pred (A × B) α → Pred (B × C) β → Pred(A × C) γ → Type _
TransFlip P Q R = ∀ {i j k} → Q (j , k) → P (i , j) → R (i , k)

-- Transitivity.
Transitive : Pred (A × A) ℓ → Type _
Transitive P = Trans P P P

-- Generalised antisymmetry
Antisym : Pred (A × B) α → Pred (B × A) β → Pred (A × B) γ → Type _
Antisym R S E = ∀ {i j} → R (i , j) → S (j , i) → E (i , j)

-- Antisymmetry (defined terms of a given equality _≈_).
Antisymmetric : BinRel A α → Pred (A × A) β → Type _
Antisymmetric _≈_ P = Antisym P P (uncurry _≈_)

-- Irreflexivity (defined terms of a given equality _≈_).

Irreflexive : BinREL A B α → Pred (A × B) β → Type _
Irreflexive _≈_ P = ∀ {x y} → x ≈ y → (x , y) ∉ P

-- Asymmetry.

Asymmetric : Pred (A × A) ℓ → Type _
Asymmetric P = ∀ {x y} → (x , y) ∈ P → (y , x) ∉ P

-- Generalised connex - exactly one of the two relations holds.

Connex : Pred (A × B) α → Pred (B × A) β → Type _
Connex P Q = ∀ x y → (x , y) ∈ P ⊎ (y , x) ∈ Q

-- Totality.

Total : Pred (A × A) ℓ → Type _
Total P = Connex P P

{-# WARNING_ON_USAGE curry          "Use Data.Product.curry instead. Deprecated under #309; removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE uncurry        "Use Data.Product.uncurry instead. Deprecated under #309; removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE Reflexive      "Use Setoid.Relations.Properties.Reflexive instead. Note: the canonical version uses stdlib Rel A ℓ (curried) rather than Pred (A × A) ℓ. Deprecated under #309; removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE Sym            "Use Setoid.Relations.Properties.Sym instead. Deprecated under #309; removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE Symmetric      "Use Setoid.Relations.Properties.Symmetric instead. Deprecated under #309; removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE Trans          "Use Setoid.Relations.Properties.Trans instead. Deprecated under #309; removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE TransFlip      "Use Setoid.Relations.Properties.TransFlip instead. Deprecated under #309; removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE Transitive     "Use Setoid.Relations.Properties.Transitive instead. Deprecated under #309; removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE Antisym        "Use Setoid.Relations.Properties.Antisym instead. Deprecated under #309; removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE Antisymmetric  "Use Setoid.Relations.Properties.Antisymmetric instead. Deprecated under #309; removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE Irreflexive    "Use Setoid.Relations.Properties.Irreflexive instead. Deprecated under #309; removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE Asymmetric     "Use Setoid.Relations.Properties.Asymmetric instead. Deprecated under #309; removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE Connex         "Use Setoid.Relations.Properties.Connex instead. Note: the canonical (stdlib) Connex is homogeneous (Rel A ℓ on both sides) where the legacy version is heterogeneous; if you need the heterogeneous form, define it locally. Deprecated under #309; removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE Total          "Use Setoid.Relations.Properties.Total instead. Deprecated under #309; removal planned one minor cycle later." #-}