↑ 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

We begin with a definition that is useful for defining poitwise “equality” of functions with respect to a given “equality” relation (see also the definition of _≈̇_ in the Base.Adjunction.Residuation 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

Thus, given a binary relation on ‵B, and a pair of functions f, g : A → B, we have f (Pointwise ) g provided ∀ x → f x ≋ g x`.

Here is the analogous definition for dependent functions.

 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

Next we define a type that is useful for asserting that the image of a function is contained in a particular “subset” (predicate) 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 Agda Standard Library.

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

We represent “sets” as inhabitants of such predicate types.

(In the definition of Pred above, we replaced Set with Type for consistency with our notation.)

Sometimes it is useful to obtain the underlying type (A) over which the predicates in Pred A ℓ (the “subsets” of A) are defined.

 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 relation types we define below and in the Base.Relations.Continuous module.

We import the “heterogeneous” binary relation type from the standard library and renamed BinREL.

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

A special case, the homogeneous binary relation type is also imported and renamed BinRel.

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

Occasionally it is useful to extract the universe level over which a binary relation is defined.

 Level-of-Rel : { : Level}  BinRel A   Level
 Level-of-Rel {} _ = 


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 →