↑ Top


Discrete Relations

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

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

module Base.Relations.Discrete 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 Function.Base                using ( _∘_ )
open import Level                        using ( _⊔_ ; Level ; Lift )
open import Relation.Binary              using ( IsEquivalence ; _⇒_ ; _=[_]⇒_ )
                                      renaming ( REL to BinREL ; Rel to BinRel )
open import Relation.Binary.Definitions  using ( Reflexive ; Transitive )
open import Relation.Unary               using ( _∈_; Pred )
open import Relation.Binary.PropositionalEquality using ( _≡_ )

-- Imports from agda-algebras -------------------------------------------------------------------
open import Overture using (_≈_ ; Π-syntax ; Op)

private variable α β ρ 𝓥 : Level

Here is a function that is useful for defining poitwise equality of functions wrt a given equality (see, e.g., the definition of _≈̇_ in the [Residuation.Properties][] module).

module _ {A : Type α} where

 PointWise : {B : Type β } (_≋_ : BinRel B ρ)  BinRel (A  B) _
 PointWise {B = B} _≋_ = λ (f g : A  B)   x  f x  g x

 depPointWise :  {B : A  Type β }
                 (_≋_ : {γ : Level}{C : Type γ}  BinRel C ρ)
                BinRel ((a : A)  B a) _
 depPointWise {B = B} _≋_ = λ (f g : (a : A)  B a)   x  f x  g x

Here is useful notation for asserting that the image of a function (the first argument) is contained in a predicate, the second argument (a “subset” of the codomain).

 Im_⊆_ : {B : Type β}  (A  B)  Pred B ρ  Type (α  ρ)
 Im f  S =  x  f x  S

Operation symbols, unary relations, binary relations

The unary relation (or “predicate”) type is imported from Relation.Unary of the std lib.

Pred : ∀ {a} → Set a → (ℓ : Level) → Set (a ⊔ suc ℓ)
Pred A ℓ = A → Set ℓ

Sometimes it is useful to obtain the underlying type of a predicate.

 PredType : Pred A ρ  Type α
 PredType _ = A

The binary relation types are called Rel and REL in the standard library, but we will call them BinRel and BinREL and reserve the names Rel and REL for the more general types of relations we define below and in the Base.Relations.Continuous module.

The heterogeneous binary relation type is imported from the standard library and renamed BinREL.

BinREL : ∀ {ℓ} (A B : Type ℓ) (ℓ' : Level) → Type (ℓ-max ℓ (ℓ-suc ℓ'))
BinREL A B ℓ' = A → B → Type ℓ'

The homogeneous binary relation type is imported from the standard library and renamed BinRel.

BinRel : ∀{ℓ} → Type ℓ → (ℓ' : Level) → Type (ℓ ⊔ lsuc ℓ')
BinRel A ℓ' = REL A A ℓ'
 Level-of-Rel : { : Level}  BinRel A   Level
 Level-of-Rel {} _ = 

Kernels

The kernel of f : A → B is defined informally by {(x , y) ∈ A × A : f x = f y}. This can be represented in type theory and Agda in a number of ways, each of which may be useful in a particular context. For example, we could define the kernel to be an inhabitant of a (binary) relation type, or a (unary) predicate type.

module _ {A : Type α}{B : Type β} where

 ker : (A  B)  BinRel A β
 ker g x y = g x  g y

 kerRel : {ρ : Level}  BinRel B ρ  (A  B)  BinRel A ρ
 kerRel _≈_ g x y = g x  g y

 kernelRel : {ρ : Level}  BinRel B ρ  (A  B)  Pred (A × A) ρ
 kernelRel _≈_ g (x , y) = g x  g y

 open IsEquivalence

 kerRelOfEquiv :  {ρ : Level}{R : BinRel B ρ}
                 IsEquivalence R  (h : A  B)  IsEquivalence (kerRel R h)

 kerRelOfEquiv eqR h = record  { refl = refl eqR
                               ; sym = sym eqR
                               ; trans = trans eqR
                               }

 kerlift : (A  B)  (ρ : Level)  BinRel A (β  ρ)
 kerlift g ρ x y = Lift ρ (g x  g y)

 ker' : (A  B)  (I : Type 𝓥)  BinRel (I  A) (β  𝓥)
 ker' g I x y = g  x  g  y

 kernel : (A  B)  Pred (A × A) β
 kernel g (x , y) = g x  g y

-- The *identity relation* (equivalently, the kernel of a 1-to-1 function)
0[_] : (A : Type α)  {ρ : Level}  BinRel A (α  ρ)
0[ A ] {ρ} = λ x y  Lift ρ (x  y)

module _ {A : Type (α  ρ)} where

 -- Subset containment relation for binary realtions
 _⊑_ : BinRel A ρ  BinRel A ρ  Type (α  ρ)
 P  Q =  x y  P x y  Q x y

 ⊑-refl : Reflexive _⊑_
 ⊑-refl = λ _ _ z  z

 ⊑-trans : Transitive _⊑_
 ⊑-trans P⊑Q Q⊑R x y Pxy = Q⊑R x y (P⊑Q x y Pxy)

Compatibility of operations and relations

Recall, from the [Overture.Signatures][] and [Overture.Operations][] modules which established our convention of reserving the sybmols 𝓞 and 𝓥 for types that represent operation symbols and arities, respectively.

In the present subsection, we define types that are useful for asserting and proving facts about compatibility of operations and relations

-- lift a binary relation to the corresponding `I`-ary relation.

eval-rel : {A : Type α}{I : Type 𝓥}  BinRel A ρ  BinRel (I  A) (𝓥  ρ)
eval-rel R u v =  i  R (u i) (v i)

eval-pred : {A : Type α}{I : Type 𝓥}  Pred (A × A) ρ  BinRel (I  A) (𝓥  ρ)
eval-pred P u v =  i  (u i , v i)  P

If f : Op I and R : Rel A β, then we say f and R are compatible just in case ∀ u v : I → A, Π i ꞉ I , R (u i) (v i) → R (f u) (f v).

_preserves_ : {A : Type α}{I : Type 𝓥}  Op A I  BinRel A ρ  Type (α  𝓥  ρ)
f preserves R  =  u v  (eval-rel R) u v  R (f u) (f v)

--shorthand notation for preserves
_|:_ : {A : Type α}{I : Type 𝓥}  Op A I  BinRel A ρ  Type (α  𝓥  ρ)
f |: R  = (eval-rel R) =[ f ]⇒ R

-- predicate version of the compatibility relation
_preserves-pred_ : {A : Type α}{I : Type 𝓥}  Op A I  Pred ( A × A ) ρ  Type (α  𝓥  ρ)
f preserves-pred P  =  u v  (eval-pred P) u v  (f u , f v)  P

_|:pred_ : {A : Type α}{I : Type 𝓥}  Op A I  Pred (A × A) ρ  Type (α  𝓥  ρ)
f |:pred P  = (eval-pred P) =[ f ]⇒ λ x y  (x , y)  P


-- The two types just defined are logically equivalent.
module _ {A : Type α}{I : Type 𝓥}{f : Op A I}{R : BinRel A ρ} where
 compatibility-agreement : f preserves R  f |: R
 compatibility-agreement c {x}{y} Rxy = c x y Rxy
 compatibility-agreement' : f |: R  f preserves R
 compatibility-agreement' c = λ u v x  c x

↑ Base.Relations Base.Relations.Continuous →