Setoid.Relations.Continuous

Continuous Relations on Setoids

This is the Setoid.Relations.Continuous module of the Agda Universal Algebra Library.

A continuous relation of arity I over a type A is a predicate on I-tuples drawn from A. The arity I : Type ι is an arbitrary type — not a fixed natural number — so the API generalises uniformly over finite, countable, and uncountable arities. This module is the canonical setoid-flavoured home for the continuous-relation API, ported from Legacy.Base.Relations.Continuous under #308. Three deliberate design choices distinguish it from the legacy:

• Π-setoid as the canonical I-tuple object. The natural I-tuple type whose pointwise equivalence a relation may be required to respect is the carrier of the Π-setoid ⨅ˢ 𝒜, defined below. Its level signature (α ⊔ ι, ρᵃ ⊔ ι) matches that of Setoid.Algebras.Products.⨅ exactly; in fact the inlined Domain of ⨅ is ⨅ˢ applied to the algebras' domain setoids, so ⨅ˢ and ⨅ compose by definitional unfolding. Lifting this construction to a named referent here means every downstream relational development can speak about "I-tuples up to pointwise equivalence" without re-rolling the Π-setoid inline.

• Bare carrier types in Rel/REL, with setoid-respect as an external overlay. The relation types Rel A I and REL I 𝒜 themselves take bare carrier types, exactly matching the legacy carrier shape. Setoid structure is introduced through ⨅ˢ and through the Π-Respects-* predicates, which name the property "respects pointwise equivalence" as a separate assertion. This factorisation has three concrete payoffs. (i) The consumer-side migration of existing call sites is purely an import-path change. (ii) It mirrors how Setoid.Relations.Quotients uses bare Pred types throughout. (iii) Agda's level inference works out cleanly: a setoid-parameterised Rel would force the user to disambiguate the unconstrained equivalence-level ρᵃ of every implicit setoid argument at every call site, since the projection Carrier : Setoid α ρᵃ → Type α is not injective in ρᵃ.

• Cubical-friendly by construction. ⨅ˢ is defined against Setoid's public interface (Carrier, _≈_, isEquivalence); a Cubical port replaces these with path equality, and the construction goes through with the equivalence-witness layer collapsing to triviality. The bare-types Rel/REL are independent of the equivalence story and port with no change at all.

A note on compatible-REL. The legacy Legacy.Base.Relations.Continuous.compatible-REL reads compatible-REL 𝑓 R = Π[ t ∈ … ] eval-REL R t, which is unconditional in t and never references 𝑓 — a bug, since it makes the predicate independent of the operations. The intended definition, mirroring the structure of the (correct) single-sorted compatible-Rel, is ∀ t → eval-REL R t → R (λ i → 𝑓 i (t i)). The canonical port below uses the corrected definition.

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

module Setoid.Relations.Continuous where

-- Imports from Agda primitives and the standard library.
open import Agda.Primitive    using () renaming ( Set to Type )
open import Level             using ( Level ; _⊔_ ; suc )
open import Relation.Binary   using ( Setoid ; IsEquivalence )

open Setoid         using ( Carrier ; _≈_ ) renaming ( isEquivalence to isEqv )
open IsEquivalence  using () renaming ( refl to reflᴱ ; sym to symᴱ ; trans to transᴱ )

-- Imports from agda-algebras.
open import Overture          using ( Op ; arity[_] )

private variable α ρᵃ ρ ι : Level

The Π-setoid construction

Given an indexing type I : Type ι and a family 𝒜 : I → Setoid α ρᵃ, the indexed-product setoid ⨅ˢ 𝒜 has carrier the dependent function type (i : I) → Carrier (𝒜 i) and equivalence the pointwise equivalence λ a b → ∀ i → _≈_ (𝒜 i) (a i) (b i), an equivalence relation by appeal to each isEquivalence (𝒜 i). The level signature matches Setoid.Algebras.Products.⨅ exactly; lifting the construction to a named referent means downstream consumers can reference a single canonical Π-setoid rather than rolling it inline at each use site.

⨅ˢ : {I : Type ι} → (𝒜 : I → Setoid α ρᵃ) → Setoid (α ⊔ ι) (ρᵃ ⊔ ι)
⨅ˢ {I = I} 𝒜 = record
  { Carrier        = (i : I) → Carrier (𝒜 i)
  ; _≈_            = λ a b → (i : I) → _≈_ (𝒜 i) (a i) (b i)
  ; isEquivalence  = record
      { refl   = λ i      → reflᴱ   (isEqv (𝒜 i))
      ; sym    = λ p i    → symᴱ    (isEqv (𝒜 i)) (p i)
      ; trans  = λ p q i  → transᴱ  (isEqv (𝒜 i)) (p i) (q i)
      }
  }

Continuous and dependent relations

The single-sorted continuous relation type Rel A I represents predicates of arity I over a single carrier A.

Rel : (A : Type α) (I : Type ι) → {ρ : Level} → Type (α ⊔ ι ⊔ suc ρ)
Rel A I {ρ} = (I → A) → Type ρ

-- single-sorted: ρ explicit, syntax binds it
Rel-syntax : (A : Type α) (I : Type ι) (ρ : Level) → Type (α ⊔ ι ⊔ suc ρ)
Rel-syntax A I ρ = Rel A I {ρ}

syntax Rel-syntax A I ρ = Rel[ A ^ I ] ρ
infix  Rel-syntax

The multi-sorted (or dependent) continuous relation type REL I 𝒜 represents predicates over an indexed family 𝒜 : I → Type α of carriers. Inhabitants are predicates on dependent I-tuples — i.e. on (i : I) → 𝒜 i. When 𝒜 i = Carrier (𝒮 i) for an indexed family 𝒮 : I → Setoid α ρᵃ, this is definitionally the same as a predicate on Carrier (⨅ˢ 𝒮), which is the bridge to the Π-setoid story.

REL : (I : Type ι) → (I → Type α) → {ρ : Level} → Type (α ⊔ ι ⊔ suc ρ)
REL I 𝒜 {ρ} = ((i : I) → 𝒜 i) → Type ρ

-- multi-sorted: ρ implicit, syntax does NOT bind it
REL-syntax : (I : Type ι) → (I → Type α) → {ρ : Level} → Type (α ⊔ ι ⊔ suc ρ)
REL-syntax I 𝒜 {ρ} = REL I 𝒜 {ρ}

syntax REL-syntax I (λ i → 𝒜) = REL[ i ∈ I ] 𝒜
infix  REL-syntax

Respecting pointwise equivalence

A continuous relation R on the carrier of a setoid 𝐴 respects pointwise equivalence on tuples if R f and f ≈ g (the pointwise lift of _≈_ 𝐴 to tuples) imply R g. Equivalently, R Respects (_≈_ (⨅ˢ {I = I} (λ _ → 𝐴))) against stdlib's Relation.Unary._Respects_.

The predicates Π-Respects-Rel and Π-Respects-REL below name this property as an explicit assertion rather than bundling it into the relation type itself, leaving consumers free to demand it where it matters and ignore it elsewhere — for the polymorphism-clone machinery in #274, the infinitary-CSP work in #281, and the Scott-continuous-DCPO work in #282 it is load-bearing; for transient working relations it is overhead. The setoid argument is explicit in both predicates: the projection Carrier : Setoid α ρᵃ → Type α is not injective in ρᵃ, so an implicit setoid argument would be undetermined at every call site.

Π-Respects-Rel :  (𝐴 : Setoid α ρᵃ){I : Type ι}{ρ : Level}
  →                Rel (Carrier 𝐴) I {ρ} → Type (ι ⊔ α ⊔ ρᵃ ⊔ ρ)
Π-Respects-Rel 𝐴 {I = I} R =
  ∀ {f g} → ((i : I) → _≈_ 𝐴 (f i) (g i)) → R f → R g

Π-Respects-REL :  {I : Type ι}(𝒜 : I → Setoid α ρᵃ){ρ : Level}
  →                REL I (λ i → Carrier (𝒜 i)) {ρ} → Type (ι ⊔ α ⊔ ρᵃ ⊔ ρ)
Π-Respects-REL {I = I} 𝒜 R =
  ∀ {f g} → ((i : I) → _≈_ (𝒜 i) (f i) (g i)) → R f → R g

Compatibility of operations with continuous relations

The operation eval-Rel lifts an I-ary relation to an (I → J)-ary relation: the lifted relation relates an I-tuple of J-tuples just in case each J-indexed row of the tuple-of-tuples (viewed as a J-indexed family of I-tuples) belongs to the original relation.

eval-Rel :  {A : Type α}{I : Type ι}
  →          Rel A I {ρ} → (J : Type ι) → (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 : Op J A if, for every I-tuple-of-J-tuples whose J-indexed rows lie in R, applying f columnwise yields a tuple in R.

compatible-Rel :  {A : Type α}{I J : Type ι}
  →                Op J A → Rel A I {ρ} → Type (ι ⊔ α ⊔ ρ)
compatible-Rel f R = ∀ t → eval-Rel R arity[ f ] t → R (λ i → f (t i))

Compatibility of operations with dependent relations

The multi-sorted analogues eval-REL and compatible-REL mirror the single-sorted versions exactly, with Rel A I replaced by REL I 𝒜 and tuple types replaced by their dependent counterparts. The definition of compatible-REL corrects the buggy form in the legacy module; see the module header.

eval-REL :  {I : Type ι}{𝒜 : I → Type α}{J : Type ι}
  →          REL I 𝒜 {ρ}
  →          ((i : I) → J → 𝒜 i)
  →          Type (ι ⊔ ρ)
eval-REL {J = J} R t = (j : J) → R (λ i → t i j)

compatible-REL :  {I J : Type ι}{𝒜 : I → Type α}
  →                (∀ i → Op J (𝒜 i))
  →                REL I 𝒜 {ρ}
  →                Type (ι ⊔ α ⊔ ρ)
compatible-REL 𝑓 R = ∀ t → eval-REL R t → R (λ i → 𝑓 i (t i))