 ### 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
```