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