Legacy.Base.Categories

Categories

This is the Legacy.Base.Categories module of the Agda Universal Algebra Library.

This module is intended, not to replace or override anything in the agda-categories library, but rather to collect some experiments in the use of category theory to re-express some of the basic concepts from universal algebra developed in other modules of the agda-algebra library.

The purpose of this effort twofold. First, we hope it makes the types defined in the agda-algebras library more modular and reusable. Second, we hope that the more general language of category theory will make metaprogramming easier. Somewhat ironically, one of our main motivations for metaprogramming is to help automate the task of recognizing when we have multiple alternative definitions (or proofs) of a single concept (or theorem) in the library and to potentially remove or consolidate such redundancy.

{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Legacy.Base.Categories where

open import Legacy.Base.Categories.Functors  public