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 are also developing a version of the library based on Cubical Agda, which will consist of submodules of the the Cubical module, but this work has only just begun.)

{-# OPTIONS --without-K --exact-split --safe #-} module Base where open import Base.Overture open import Base.Relations open import Base.Algebras open import Base.Equality open import Base.Homomorphisms open import Base.Terms open import Base.Subalgebras open import Base.Varieties open import Base.Structures open import Base.Adjunction open import Base.Categories open import Base.Complexity