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, which we refer to 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 (general relations) and they can be defined over arbitrary families of types (dependent relations). 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