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

{-# OPTIONS --without-K --exact-split --safe #-} module Relations.Discrete where -- Imports from Agda and the Agda Standard Library ---------------------------------------------- open import Agda.Primitive using ( _⊔_ ; lsuc ) 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 ) open import Relation.Binary.Core using ( _⇒_ ; _=[_]⇒_ ) 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.Preliminaries using (_≈_ ; Π-syntax) 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).

PointWise : {A : Type α}{B : Type β } (_≋_ : BinRel B ρ) → BinRel (A → B) _ PointWise {A = A}{B} _≋_ = λ (f g : A → B) → ∀ x → f x ≋ g x depPointWise : {A : Type α}{B : A → Type β } (_≋_ : {γ : Level}{C : Type γ} → BinRel C ρ) → BinRel ((a : A) → B a) _ depPointWise {A = A}{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_⊆_ : {A : Type α}{B : Type β} → (A → B) → Pred B ρ → Type (α ⊔ ρ) Im f ⊆ S = ∀ x → f x ∈ S

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 : {A : Type α} → Pred A ρ → Type α PredType {A = A} _ = 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 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 : {A : Type α}{ℓ : Level} → BinRel A ℓ → Level Level-of-Rel {A = A}{ℓ} _ = ℓ

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)

**Notation**. For consistency and readability, we reserve two universe variables for
special purposes. The first of these is 𝓞 which shall be reserved for types that
represent *operation symbols*. The second is 𝓥 which we
reserve for types representing *arities* of relations or operations.

In the next subsection, we define types that are useful for asserting and proving
facts about *compatibility* of *operations* with relations, but first we need a
general type with which to represent operations. Here is the definition, which we
justify below.

The type `Op`

encodes the arity of an operation as an arbitrary type `I : Type 𝓥`

,
which gives us a very general way to represent an operation as a function type with
domain `I → A`

(the type of “tuples”) and codomain `A`

. For example, the `I`

-*ary
projection operations* on `A`

are represented as inhabitants of the type `Op I A`

as
follows.

-- The type of operations on A of arity I Op : Type α → Type 𝓥 → Type (α ⊔ 𝓥) Op A I = (I → A) → A -- Example (projections) π : {I : Type 𝓥} {A : Type α } → I → Op A I π i x = x i -- return the arity of a given operation symbol arity[_] : {I : Type 𝓥} {A : Type α } → Op A I → Type 𝓥 arity[_] {I = I} f = I -- 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