↑ Top


Properties of binary predicates

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

{-# OPTIONS --without-K --exact-split --safe #-}

module 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
 α β γ  ℓ₁ ℓ₂ ℓ₃ : Level
 A : Set α
 B : Set β
 C : Set γ

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

← Base.Relations.Continuous Base.Relations.Quotients →