↑ Top


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

In the 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 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 Relations.Quotients we define quotient types.

{-# OPTIONS --without-K --exact-split --safe #-}

module Relations where

open import Relations.Discrete
open import Relations.Continuous
open import Relations.Properties
open import Relations.Quotients
open import Relations.Func

← Overture.Func.Bijective Relations.Discrete →