Setoid.Relations.Properties¶

Properties of binary relations¶

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

The canonical home for elementary properties of binary relations — reflexivity, symmetry, transitivity, antisymmetry, irreflexivity, asymmetry, connex, totality — is Relation.Binary.Definitions in the Agda standard library. Stdlib expresses these properties for Rel A ℓ = A → A → Type ℓ (the curried form), and the canonical Setoid/ tree adopts the same convention: Setoid.Relations.Discrete and Setoid.Relations.Quotients already import their Reflexive / Transitive etc. directly from stdlib.

This module exists to give agda-algebras users a stable canonical import path that mirrors Legacy.Base.Relations.Properties in the v2.x library and that sits alongside the canonical Setoid.Relations.{Discrete,Quotients,Continuous} siblings. Its content is a thin public re-export from stdlib — no new definitions are introduced. If a genuinely Setoid-flavoured relation property surfaces later (e.g., reflexivity that respects a setoid's _≈_), it can be added here without disrupting the canonical import path.

Differences from the legacy module:

The legacy module defined its properties for Pred (A × A) ℓ (a predicate on the product type); this module uses the stdlib Rel A ℓ (the curried form). The two are interconvertible via Data.Product.curry / Data.Product.uncurry; the curried form is preferred because the rest of the canonical tree already uses it.
The legacy module bundled its own curry / uncurry definitions; stdlib's Data.Product.curry / Data.Product.uncurry cover the same ground and are not re-exported here. Consumers who need the bridge should import from Data.Product directly.

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

module Setoid.Relations.Properties where

open import Relation.Binary.Definitions public
  using  ( Reflexive    ; Sym         ; Symmetric
         ; Trans        ; TransFlip   ; Transitive
         ; Antisym      ; Antisymmetric
         ; Irreflexive  ; Asymmetric
         ; Connex       ; Total )