Overture.Relations

Foundational relation infrastructure

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

This module collects the foundational definitions concerning binary relations on a type that are needed by both the canonical Setoid/ tree and the planned Classical/ tree. Every definition in this module takes its arguments at the level of bare types and BinaryRel; none presupposes a setoid structure. The Setoid-flavoured analogues — relations between setoid functions, kernels of setoid morphisms, etc. — live in Setoid.Relations.* and are built on top of, rather than parallel to, what is collected here.

The contents fall into four clusters.

• Equivalence. A Σ-bundle of a binary relation with a proof that it is an equivalence relation. The setoid _/_ quotient construction in Setoid.Relations.Quotients consumes this.
• Kernels and identity. kerRel, kerRelOfEquiv, kernelRel, and the trivial relation 0[_]. Used pervasively in Setoid.Homomorphisms.{Factor,Kernels} and Setoid.Congruences.
• Image-containment. Im_⊆_, the predicate that the image of a tuple lies inside a given subset. Used in Setoid.Subalgebras.Subuniverses for the ar-tuple of an operation, which is a raw function from an arity type to the algebra's carrier — not a setoid function — so the bare-types version is what's needed at the call site.
• Compatibility. _|:_ (and its long form _preserves_), expressing that an Op I A is compatible with a BinaryRel A ρ. Used in Setoid.Congruences._∣≈_ even on setoid algebras, since congruences of a setoid algebra are bare-types relations on its carrier that contain the setoid's _≈_.
• Pointwise lifting. PointWise and depPointWise, lifting a binary relation on a codomain (or a family of relations on a dependent codomain) to the function space. Generalizes stdlib's _≗_ (which fixes the codomain relation to _≡_). Used in Overture.Adjunction.Residuation to express that the composite g ∘ f ∘ g agrees pointwise with g.

This module is a Category-A relocation under #303 (M2-6). See src/Legacy/Base/DEPRECATED.md for the full inventory and migration guidance.

{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Overture.Relations where

open import Agda.Primitive   using () renaming ( Set to Type )

-- Imports from the Agda standard library ----------------------------------------------
open import Data.Product     using ( _×_ ; _,_ ; Σ-syntax )
open import Level            using ( Level ; Lift ; lift ; lower ; _⊔_ )
                             renaming ( suc to lsuc )
open import Relation.Binary  using ( IsEquivalence ; _=[_]⇒_ )
                             renaming ( Rel to BinaryRel )
open import Relation.Unary   using ( Pred ; _∈_ )

open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl ; sym ; trans )

-- Imports from agda-algebras ----------------------------------------------------------
open import Overture.Operations  using ( Op )

private variable
  a b ρ ℓ : Level
  𝓦 : Level   -- arity-tuple level, conventional name elsewhere in the library

The Equivalence Σ-bundle

Equivalence A {ρ} packages a binary relation on A with a proof that the relation is an equivalence. Compared to stdlib's Relation.Binary.Bundles.Setoid, which bundles a Carrier and an _≈_ and an IsEquivalence, Equivalence fixes the carrier as a parameter and bundles only the relation with its proof — useful when one wants to vary the equivalence relation over a fixed carrier (the situation in quotient and congruence constructions).

Equivalence : Type a → {ρ : Level} → Type (a ⊔ lsuc ρ)
Equivalence A {ρ} = Σ[ r ∈ BinaryRel A ρ ] IsEquivalence r

Given R : Equivalence A, we use (proj₁ R) for the underlying relation and (proj₂ R) for the equivalence-relation proof, following the library convention.

Equivalence classes

If R is a binary relation on A, the R-block containing u : A is the predicate that holds at v precisely when R u v. The notation [ u ] R is shorthand for that predicate.

[_] : {A : Type a} → A → {ρ : Level} → BinaryRel A ρ → Pred A ρ
[ u ] R = R u

infix  [_]

The identity relation

The identity (or zero) relation on A is λ x y → Lift ρ (x ≡ y). The Lift is there so that the relation's universe level can be parametrized independently of the carrier's level — useful when the relation has to live at a level dictated by surrounding context (e.g., congruence relations on an algebra at level α ⊔ suc ρ).

0[_] : (A : Type a) → {ρ : Level} → BinaryRel A (a ⊔ ρ)
0[ A ] {ρ} = λ x y → Lift ρ (x ≡ y)

The identity relation is, of course, an equivalence relation; we package its IsEquivalence proof and the corresponding Equivalence bundle for convenience.

0[_]IsEquivalence : (A : Type a){ρ : Level} → IsEquivalence (0[ A ] {ρ})
0[ A ]IsEquivalence .IsEquivalence.refl   = lift refl
0[ A ]IsEquivalence .IsEquivalence.sym    = λ p → lift (sym (lower p))
0[ A ]IsEquivalence .IsEquivalence.trans  = λ p q → lift (trans (lower p) (lower q))

0[_]Equivalence : (A : Type a){ρ : Level} → Equivalence A {a ⊔ ρ}
0[ A ]Equivalence {ρ} = 0[ A ] {ρ} , 0[ A ]IsEquivalence

Kernels of raw functions

The kernel of f : A → B is the equivalence relation on A whose blocks are the fibres of f. We give three formulations corresponding to three idiomatic uses elsewhere in the library: kerRel parametrizes the codomain equivalence (used when B has its own equivalence relation that the kernel should reflect, e.g. the carrier of a setoid algebra); kernelRel repackages the same content as a predicate on pairs (more convenient for some Pred-based constructions); and kerRelOfEquiv lifts an IsEquivalence proof on the codomain to one on the kernel.

module _ {A : Type a} {B : Type b} where

  kerRel : {ρ : Level} → BinaryRel B ρ → (A → B) → BinaryRel A ρ
  kerRel _≈_ g x y = g x ≈ g y

  kernelRel : {ρ : Level} → BinaryRel B ρ → (A → B) → Pred (A × A) ρ
  kernelRel _≈_ g (x , y) = g x ≈ g y

  kerRelOfEquiv :  {ρ : Level}{R : BinaryRel B ρ}
    → IsEquivalence R → (h : A → B) → IsEquivalence (kerRel R h)

  kerRelOfEquiv eqR h = record  { refl = reflR ; sym = symR ; trans = transR }
    where open IsEquivalence eqR renaming (refl to reflR ; sym to symR ; trans to transR)

Image-containment of a tuple

If a : I → A is a tuple of A-values indexed by I, and B is a subset of A, then Im a ⊆ B asserts that every component of the tuple lies in B. This is the bare-types form of image-containment, in which a is a raw function rather than a setoid morphism.

Im_⊆_ : {A : Type a} {I : Type 𝓦} → (I → A) → Pred A ℓ → Type (𝓦 ⊔ ℓ)
Im a ⊆ B = ∀ i → a i ∈ B

A setoid analogue of Im_⊆_, taking a setoid function rather than a raw function, is given separately in Setoid.Relations.Discrete. The two coexist because they have genuinely different type signatures and serve genuinely different call sites.

Pointwise lifting of a binary relation

If _≋_ is a binary relation on B, the pointwise lift of _≋_ to the function space A → B holds at f, g : A → B precisely when ∀ x → f x ≋ g x. This construction is foundational across the library: it is the equality used in Overture.Adjunction.Residuation to express that the composite g ∘ f ∘ g agrees pointwise with g, and is the natural generalization of stdlib's _≗_ (which fixes _≋_ = _≡_) to an arbitrary equivalence on the codomain.

module _ {A : Type a} where

  PointWise : {B : Type b} (_≋_ : BinaryRel B ρ) → BinaryRel (A → B) _
  PointWise {B = B} _≋_ = λ (f g : A → B) → ∀ x → f x ≋ g x

The dependent analogue lifts _≋_ over a family B : A → Type b.

Here _≋_ is a family of relations; for each index x : A, an instance _≋_ {x} is a binary relation on the fiber B x. This is the standard dependent generalization — the relations on distinct fibers may be unrelated — and is what makes the lift usable with fiber-specific relations rather than restricting to relations uniform across types.

  depPointWise :  {B : A → Type b} (_≋_ : ∀ {x} → BinaryRel (B x) ρ) → BinaryRel ((a : A) → B a) _
  depPointWise {B = B} _≋_ = λ (f g : (a : A) → B a) → ∀ x → f x ≋ g x

Compatibility of operations with relations

If f : Op I A is an I-ary operation on A and R is a binary relation on A, we say that f and R are compatible (equivalently, that f preserves R) when, for all tuples u v : I → A, the pointwise hypothesis ∀ i → R (u i) (v i) implies R (f u) (f v). We provide both a long-form name _preserves_ and the customary infix shorthand _|:_.

The lifting of a binary relation to the corresponding I-ary pointwise relation is itself useful and worth naming; we call it eval-rel. A predicate-of-pairs counterpart eval-pred is provided for symmetry with kernelRel.

-- Lift a binary relation to the corresponding I-ary pointwise relation.
eval-rel : {A : Type a}{I : Type 𝓦} → BinaryRel A ρ → BinaryRel (I → A) (𝓦 ⊔ ρ)
eval-rel R u v = ∀ i → R (u i) (v i)

eval-pred : {A : Type a}{I : Type 𝓦} → Pred (A × A) ρ → BinaryRel (I → A) (𝓦 ⊔ ρ)
eval-pred P u v = ∀ i → (u i , v i) ∈ P

module _ {A : Type a}{I : Type 𝓦} where

  _preserves_ : Op I A → BinaryRel A ρ → Type (a ⊔ 𝓦 ⊔ ρ)
  f preserves R = ∀ u v → (eval-rel R) u v → R (f u) (f v)

  -- Infix shorthand for `preserves`.
  _|:_ : Op I A → BinaryRel A ρ → Type (a ⊔ 𝓦 ⊔ ρ)
  f |: R = (eval-rel R) =[ f ]⇒ R

The two formulations are logically equivalent. The shorthand _|:_ is what the Setoid tree uses pervasively; the long-form _preserves_ is provided for prose-readability at consumption sites where the brevity of |: is more cryptic than helpful.

module _ {A : Type a}{I : Type 𝓦}{f : Op I A}{R : BinaryRel A ρ} where

  preserves→|: : f preserves R → f |: R
  preserves→|: c {u}{v} Ruv = c u v Ruv

  |:→preserves : f |: R → f preserves R
  |:→preserves c = λ u v Ruv → c Ruv