↑ Top


The Base Module of the Agda Universal Algebra Library

This module collects all submodules the library that use “bare” types, as opposed to similar versions of these submodules based on Setoids (see the Setoid module).

(We have also started developing in parallel the cubical-agda-algebras library, based on Cubical Agda.)

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

module Base where

open import Base.Relations
open import Base.Functions
open import Base.Equality
open import Base.Adjunction
open import Base.Algebras
open import Base.Homomorphisms
open import Base.Terms
open import Base.Subalgebras
open import Base.Varieties
open import Base.Structures
open import Base.Categories
open import Base.Complexity


↑ agda-algebras Base.Relations →