Agda UALib ↑

Relation and Quotient Types

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

← Overture.Lifts Relations.Discrete →