↑ Top


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

↑ Base Base.Relations.Discrete →