Skip to content

Examples.Classical.Groups

Worked examples of groups

This is the Examples.Classical.Groups module of the Agda Universal Algebra Library.

Index of the worked group examples under Examples/Classical/Groups/. This module merely imports each submodule, so that the whole family type-checks at once from a single entry point; it deliberately does not open or re-export their contents. The finite examples each introduce a local operation _ยท_ and their own characteristic lemmas, which are meaningful only within their own module, so there is nothing to gain (and names to clash) from re-exporting them through a barrel.

  • CyclicGroup and AbelianGroup present (โ„ค, +, 0, -) โ€” the infinite cyclic group โ€” as a group and as an abelian group.
  • CyclicGroup3 is the cyclic group โ„ค/3โ„ค, built from a Cayley table.
  • KleinFourGroup is the Klein four-group Vโ‚„.
  • SymmetricGroup3 is the symmetric group Sโ‚ƒ, the smallest non-abelian group.
{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Examples.Classical.Groups where