SUMMARY

• Home
• The Library
  • Overture
    • Adjunction
      • Closure
      • Galois
      • Residuation
    • Basic
    • Cayley
    • Functions
    • Operations
      • Properties
    • Preface
    • Relations
    • Signatures
      • Morphisms
    • Terms
      • Basic
      • Interpretation
      • Translation
  • Setoid
    • Algebras
      • Basic
      • Products
      • Reduct
    • Categories
      • Adjunction
      • Algebra
      • Category
      • FullSubcategory
      • Functor
      • Monad
      • NaturalTransformation
      • Reduct
    • Complexity
      • Basic
      • CSP
    • Congruences
      • Basic
      • ChainJoin
      • CompleteLattice
      • Generation
      • Lattice
      • Monolith
      • Permutability
      • Properties
    • Functions
      • Basic
      • Bijective
      • Injective
      • Inverses
      • Surjective
    • Homomorphisms
      • Basic
      • Factor
      • HomomorphicImages
      • Isomorphisms
      • Kernels
      • Noether
      • Products
      • Properties
    • Operations
      • Properties
    • Relations
      • Continuous
      • Discrete
      • Properties
      • Quotients
    • Signatures
      • Functor
    • Subalgebras
      • Basic
      • CompleteLattice
      • Properties
      • Subdirect
        • Basic
        • BirkhoffSI
        • Finite
        • Irreducible
      • Subuniverses
    • Terms
      • Basic
      • Interpretation
      • Monad
      • Operations
      • Properties
      • Translation
    • Varieties
      • Closure
      • EquationalLogic
      • FreeAlgebras
      • FreeSubstitution
      • HSP
      • Interpretation
      • Invariance
      • Invariants
      • Maltsev
        • Basic
        • Distributivity
        • Modularity
        • Permutability
      • Preservation
      • Properties
      • Reducts
      • SoundAndComplete
  • Classical
    • Bundles
      • AbelianGroup
      • CommutativeMonoid
      • CommutativeRing
      • CommutativeSemigroup
      • DistributiveLattice
      • Group
      • Lattice
      • Magma
      • Monoid
      • Ring
      • Semigroup
      • Semilattice
    • Categories
      • AdjoinUnit
      • Forgetful
    • Equations
    • Interpretations
      • Maltsev
    • Operations
    • Properties
      • Lattice
    • Signatures
      • Group
      • Lattice
      • Magma
      • Monoid
      • Ring
    • Small
      • Structures
        • AbelianGroup
        • CommutativeMonoid
        • CommutativeRing
        • CommutativeSemigroup
        • DistributiveLattice
        • Group
        • Lattice
        • Magma
        • Monoid
        • Ring
        • Semigroup
        • Semilattice
    • Structures
      • AbelianGroup
      • CommutativeMonoid
      • CommutativeRing
      • CommutativeSemigroup
      • DistributiveLattice
      • Group
      • Interpret
      • Lattice
      • Magma
      • Monoid
      • Ring
      • Semigroup
      • Semilattice
    • Theories
      • AbelianGroup
      • CommutativeMonoid
      • CommutativeRing
      • CommutativeSemigroup
      • DistributiveLattice
      • Group
      • Lattice
      • Monoid
      • Ring
      • Semigroup
      • Semilattice
  • Order
    • CompleteLattice
  • Examples
    • Classical
      • CommutativeIdempotentMagma
      • CommutativeMonoid
      • CommutativeRing
      • CommutativeSemigroup
      • Groups
        • AbelianGroup
        • CyclicGroup
        • CyclicGroup3
        • KleinFourGroup
        • SymmetricGroup3
      • Lattices
        • L2
        • L2Distributive
        • L3Heyting
        • L7
      • Magma
      • Monoid
      • Semigroup
      • Semilattice
    • FunctionTypeBijections
    • PolynomialFunctors
      • Functors
    • Setoid
      • CongruenceLattice
      • FinitarySignatures
      • FiniteQuotient
      • FreeMagma
      • FreeSemigroup
      • HSPCommutativeMonoid
      • Presentation
      • SubalgebraLattice
      • SubgroupLattice
    • Structures
      • Basic
      • Signatures
  • Exercises
    • Complexity
      • FiniteCSP
  • Demos
    • ContraX
    • GeneralOperationsAndRelations
    • HSP
  • Legacy
    • Base
      • Adjunction
        • Closure
        • Galois
        • Residuation
      • Algebras
        • Basic
        • Congruences
        • Products
      • Categories
        • Functors
      • Complexity
        • Basic
        • CSP
      • Equality
        • Extensionality
        • Truncation
        • Welldefined
      • Functions
        • Injective
        • Inverses
        • Surjective
        • Transformers
      • Homomorphisms
        • Basic
        • Factor
        • HomomorphicImages
        • Isomorphisms
        • Kernels
        • Noether
        • Products
        • Properties
      • Relations
        • Continuous
        • Discrete
        • Properties
        • Quotients
      • Structures
        • Basic
        • Congruences
        • EquationalLogic
        • Graphs
        • Homs
        • Isos
        • Products
        • Sigma
          • Basic
          • Congruences
          • Homs
          • Isos
          • Products
        • Substructures
        • Terms
      • Subalgebras
        • Properties
        • Subalgebras
        • Subuniverses
      • Terms
        • Basic
        • Operations
        • Properties
      • Varieties
        • Closure
        • EquationalLogic
        • FreeAlgebras
        • Invariants
        • Preservation
        • Properties
  • Everything (module index)
  • Classic Agda HTML ↗
• Constellation
• Project
  • Roadmap
  • Maintaining the site
  • Style Guide
  • Architecture Decisions
    • Overview
    • ADR-NNN: Short noun phrase describing the decision
    • ADR-001: Setoid as canonical development tree for 3.0
    • ADR-002: Classical structures over the universal-algebra foundation
    • ADR-003: Cubical Agda as the canonical long-term target
    • ADR-004: Markdown-literate Agda (.lagda.md) as the canonical literate format
    • ADR-005: Scope of the 𝓞 / 𝓥 universe-level variables
    • ADR-006: Signature morphisms and the self-contained Sig category
    • ADR-007: MkDocs (Material) as the documentation rendering pipeline
  • Installation
  • Contributing
  • Changelog