This is the Base.Relations module of the Agda Universal Algebra Library.
In the Base.Relations.Discrete submodule we define types that represent unary and binary relations.
We refer to these as “discrete relations” to contrast them with the “continuous,” general and dependent relations that we introduce in Base.Relations.Continuous.
We call the latter “continuous relations” because they can have arbitrary arity and they can be defined over arbitrary families of types.
Finally, in Base.Relations.Quotients we define quotient types.
{-# OPTIONS --without-K --exact-split --safe #-} module Base.Relations where open import Base.Relations.Discrete public open import Base.Relations.Continuous public open import Base.Relations.Properties public open import Base.Relations.Quotients public