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

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)

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