↑ Top


Relations

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


← Base.Overture.Transformers Base.Relations.Discrete →