Classical.Small

Level-fixed veneers of classical structures

This is the Classical.Small module of the Agda Universal Algebra Library.

The Classical/Small/ subtree houses level-fixed specializations of the polymorphic structure cores in Classical/Structures/. For each concrete X, the small veneer Classical/Small/Structures/X.lagda.md fixes both the carrier-level α and the equivalence-level ρ to ℓ₀, giving a one-import path for downstream consumers that do not need universe polymorphism.

The intended audience is the family of downstream developments where most concrete instances live at Set rather than at a polymorphic Set α / Set ρ family: the finite-template constraint-satisfaction work in M7, the finite cases that motivate FLRP intuition in M6, and the tutorial-pedagogical contexts in Examples/ and Demos/. The polymorphism in the core is necessary for the substantive theorems but is a distraction at use sites for the small case; pulling the level-fixed specialization into its own subtree keeps the polymorphic core unencumbered while giving small-case users a flat import. The design rationale is recorded in ADR-002.

This file is the umbrella for the subtree, the submodules of which include fixed-universe-level veneers; these are paired with polymorphic cores in Classical/Structures/.

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

module Classical.Small where

open import Classical.Small.Structures public