---
layout: default
file: "src/Classical/Categories.lagda.md"
title: "Classical.Categories module"
date: "2026-06-11"
author: "the agda-algebras development team"
---

### Category theory of classical structures

This is the [Classical.Categories][] module of the [Agda Universal Algebra Library][].

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

module Classical.Categories where

open import Classical.Categories.AdjoinUnit public
open import Classical.Categories.Forgetful public
```