---
layout: default
title : "Legacy.Base.Relations.Continuous module (The Agda Universal Algebra Library)"
date : "2021-02-28"
author: "[agda-algebras development team][]"
---
### <a id="continuous-relations">Continuous Relations</a>
> **Deprecated**. Canonical home is now [`Setoid.Relations.Continuous`](/Setoid/Relations/Continuous/), ported under #308 (M2-7d). Importers will see `WARNING_ON_USAGE` warnings on `Rel`, `REL`, their syntactic-sugar variants, and the `eval-*`/`compatible-*` helpers; in most cases, migration is just replacing `Legacy.Base.Relations.Continuous` with `Setoid.Relations.Continuous`. The replacement `Rel`/`REL` definitions still take bare carrier types as before; only the optional setoid-respect layer (for example, `Π-Respects-Rel`/`Π-Respects-REL`) requires passing an explicit `Setoid` such as `Relation.Binary.PropositionalEquality.setoid A` for a bare type `A`. See [`src/Legacy/Base/DEPRECATED.md`](../../DEPRECATED.md). Removal is planned for v3.1.
This is the [Legacy.Base.Relations.Continuous][] module of the [Agda Universal Algebra Library][].
```agda
{-# OPTIONS --cubical-compatible --exact-split --safe #-}
module Legacy.Base.Relations.Continuous where
open import Agda.Primitive using () renaming ( Set to Type )
open import Level using ( _⊔_ ; suc ; Level )
open import Overture using ( Π ; Π-syntax ; Op ; arity[_] )
private variable a ρ : Level
```
#### <a id="motivation">Motivation</a>
In set theory, an n-ary relation on a set `A` is simply a subset of the n-fold product `A × A × ⋯ × A`. As such, we could model these as predicates over the type `A × A × ⋯ × A`, or as relations of type `A → A → ⋯ → A → Type β` (for some universe β).
To implement such a relation in type theory, we would need to know the arity in advance, and then somehow form an n-fold arrow →.
It's easier and more general to instead define an arity type `I : Type 𝓥`, and define the type representing `I`-ary relations on `A` as the function type `(I → A) → Type β`.
Then, if we are specifically interested in an n-ary relation for some natural number `n`, we could take `I` to be a finite set (e.g., of type `Fin n`).
Below we define `Rel` to be the type `(I → A) → Type β` and we call this the type of *continuous relations*. This generalizes "discrete" relations (i.e., relations of finite arity---unary, binary, etc), defined in the standard library since inhabitants of the continuous relation type can have arbitrary arity.
The relations of type `Rel` not completely general, however, since they are defined over a single type. Said another way, they are *single-sorted* relations. We will remove this limitation when we define the type of *dependent continuous relations* later in the module.
Just as `Rel A β` is the single-sorted special case of the multisorted `REL A B β` in the standard library, so too is our continuous version, `Rel I A β`, the single-sorted special case of a completely general type of relations.
The latter represents relations that not only have arbitrary arities, but also are defined over arbitrary families of types.
Concretely, given an arbitrary family `A : I → Type a` of types, we may have a relation from `A i` to `A j` to `A k` to …, where the collection represented by the "indexing" type `I` might not even be enumerable.
We refer to such relations as *dependent continuous relations* (or *dependent relations* for short) because the definition of a type that represents them requires depedent types.
The `REL` type that we define [below](/Legacy/Base/Relations/Continuous/#dependent-relations) manifests this completely general notion of relation.
**Warning**! The type of binary relations in the standard library's `Relation.Binary` module is also called `Rel`. Therefore, to use both the discrete binary relation from the standard library, and our continuous relation type, we recommend renaming the former when importing with a line like this
`open import Relation.Binary renaming ( REL to BinREL ; Rel to BinRel )`
#### <a id="continuous-and-dependent-relations">Continuous and dependent relations</a>
Here we define the types `Rel` and `REL`. The first of these represents predicates of arbitrary arity over a single type `A`. As noted above, we call these *continuous relations*.
The definition of `REL` goes even further and exploits the full power of dependent types resulting in a completely general relation type, which we call the type of *dependent relations*.
Here, the tuples of a relation of type `REL I 𝒜 β` inhabit the dependent function type `𝒜 : I → Type a` (where the codomain may depend on the input coordinate `i : I` of the domain).
Heuristically, we can think of an inhabitant of type `REL I 𝒜 β` as a relation from `𝒜 i` to `𝒜 j` to `𝒜 k` to ….
(This is only a rough heuristic since `I` could denote an uncountable collection.) See the discussion below for a more detailed explanation.
```agda
module _ {𝓥 : Level} where
ar : Type (suc 𝓥)
ar = Type 𝓥
Rel : Type a → ar → {ρ : Level} → Type (a ⊔ 𝓥 ⊔ suc ρ)
Rel A I {ρ} = (I → A) → Type ρ
Rel-syntax : Type a → ar → (ρ : Level) → Type (𝓥 ⊔ a ⊔ suc ρ)
Rel-syntax A I ρ = Rel A I {ρ}
syntax Rel-syntax A I ρ = Rel[ A ^ I ] ρ
infix 6 Rel-syntax
REL : (I : ar) → (I → Type a) → {ρ : Level} → Type (𝓥 ⊔ a ⊔ suc ρ)
REL I 𝒜 {ρ} = ((i : I) → 𝒜 i) → Type ρ
REL-syntax : (I : ar) → (I → Type a) → {ρ : Level} → Type (𝓥 ⊔ a ⊔ suc ρ)
REL-syntax I 𝒜 {ρ} = REL I 𝒜 {ρ}
syntax REL-syntax I (λ i → 𝒜) = REL[ i ∈ I ] 𝒜
infix 6 REL-syntax
```
#### <a id="compatibility-with-general-relations">Compatibility with general relations</a>
```agda
eval-Rel : {I : ar}{A : Type a} → Rel A I{ρ} → (J : ar) → (I → J → A) → Type (𝓥 ⊔ ρ)
eval-Rel R J t = ∀ (j : J) → R λ i → t i j
```
A relation `R` is compatible with an operation `f` if for every tuple `t` of tuples
belonging to `R`, the tuple whose elements are the result of applying `f` to
sections of `t` also belongs to `R`.
```agda
compatible-Rel : {I J : ar}{A : Type a} → Op J A → Rel A I{ρ} → Type (𝓥 ⊔ a ⊔ ρ)
compatible-Rel f R = ∀ t → eval-Rel R arity[ f ] t → R λ i → f (t i)
```
#### <a id="compatibility-of-operations-with-dependent-relations">Compatibility of operations with dependent relations</a>
```agda
eval-REL : {I J : ar}{𝒜 : I → Type a}
→ REL I 𝒜 {ρ}
→ ((i : I) → J → 𝒜 i)
→ Type (𝓥 ⊔ ρ)
eval-REL{I = I}{J}{𝒜} R t = ∀ j → R λ i → (t i) j
compatible-REL : {I J : ar}{𝒜 : I → Type a}
→ (∀ i → Op J (𝒜 i))
→ REL I 𝒜 {ρ}
→ Type (𝓥 ⊔ a ⊔ ρ)
compatible-REL {I = I}{J}{𝒜} 𝑓 R = Π[ t ∈ ((i : I) → J → 𝒜 i) ] eval-REL R t
```
The definition `eval-REL` denotes an *evaluation* function which lifts an `I`-ary relation to an `(I → J)`-ary relation.
The lifted relation will relate an `I`-tuple of `J`-tuples when the `I`-slices (or rows) of the `J`-tuples belong
to the original relation.
The second definition, compatible-REL, denotes compatibility of an operation with a continuous relation.
#### <a id="detailed-explanation-of-the-dependent-relation-type">Detailed explanation of the dependent relation type</a>
The last two definitions above may be hard to comprehend at first, so perhaps a more detailed explanation of the semantics of these deifnitions would help.
First, one should internalize the fact that `𝒶 : I → J → A` denotes an `I`-tuple of `J`-tuples of inhabitants of `A`.
Next, recall that a continuous relation `R` denotes a certain collection of `I`-tuples (if `x : I → A`, then `R x` asserts that `x` belongs to `R`).
For such `R`, the type `eval-REL R` represents a certain collection of `I`-tuples of `J`-tuples, namely, the tuples `𝒶 : I → J → A` for which `eval-REL R 𝒶` holds.
For simplicity, pretend for a moment that `J` is a finite set, say, `{1, 2, ..., J}`, so that we can write down a couple of the `J`-tuples as columns.
For example, here are the i-th and k-th columns (for some `i k : I`).
𝒶 i 1 𝒶 k 1
𝒶 i 2 𝒶 k 2 <-- (a row of I such columns forms an I-tuple)
⋮ ⋮
𝒶 i J 𝒶 k J
Now `eval-REL R 𝒶` is defined by `∀ j → R (λ i → 𝒶 i j)` which asserts that each row of the `I` columns shown above belongs to the original relation `R`.
Finally, `compatible-REL` takes
* an `I`-tuple (`λ i → (𝑓 i)`) of `J`-ary operations, where for each i the type of `𝑓 i` is `(J → 𝒜 i) → 𝒜 i`, and
* an `I`-tuple (`𝒶 : I → J → A`) of `J`-tuples
and determines whether the `I`-tuple `λ i → (𝑓 i) (𝑎 i)` belongs to `R`.
```agda
{-# WARNING_ON_USAGE Rel "Use Setoid.Relations.Continuous.Rel instead. Deprecated under #308; removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE Rel-syntax "Use Setoid.Relations.Continuous.Rel-syntax instead. Deprecated under #308; removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE REL "Use Setoid.Relations.Continuous.REL instead. Deprecated under #308; removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE REL-syntax "Use Setoid.Relations.Continuous.REL-syntax instead. Deprecated under #308; removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE eval-Rel "Use Setoid.Relations.Continuous.eval-Rel instead. Deprecated under #308; removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE compatible-Rel "Use Setoid.Relations.Continuous.compatible-Rel instead. Deprecated under #308; removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE eval-REL "Use Setoid.Relations.Continuous.eval-REL instead. Deprecated under #308; removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE compatible-REL "Use Setoid.Relations.Continuous.compatible-REL instead. Note: the canonical version corrects a bug in the legacy definition (see Setoid.Relations.Continuous module header). Deprecated under #308; removal planned one minor cycle later." #-}
```
--------------------------------------
[agda-algebras development team]: https://github.com/ualib/agda-algebras#the-agda-algebras-development-team