This is the UALib.Relations module of the Agda Universal Algebra Library.
In Relations.Discrete 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 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).
{-# OPTIONS --without-K --exact-split --safe #-}
module Relations where open import Relations.Discrete open import Relations.Continuous open import Relations.Quotients open import Relations.Truncation open import Relations.Extensionality