Skip to content

Classical.Small.Structures.AbelianGroup

Level-fixed Abelian Group

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

Specializes Classical.Structures.AbelianGroup to the 0โ„“โ€“0โ„“ case, mirroring the veneers of Monoid, CommutativeMonoid, Group, etc.

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

module Classical.Small.Structures.AbelianGroup where

open import Agda.Primitive                          using () renaming ( Set to Type )
open import Level                                   using ( 0โ„“ ; suc )
open import Relation.Binary.PropositionalEquality   using ( _โ‰ก_ )

import Classical.Structures.AbelianGroup as Polymorphic

AbelianGroup : Type (suc 0โ„“)
AbelianGroup = Polymorphic.AbelianGroup 0โ„“ 0โ„“

eqsToAbelianGroup : (A : Type 0โ„“) (_ยท_ : A โ†’ A โ†’ A) (e : A) (i : A โ†’ A)
  โ†’ (โˆ€ a b c โ†’ (a ยท b) ยท c โ‰ก a ยท (b ยท c))
  โ†’ (โˆ€ a โ†’ e ยท a โ‰ก a) โ†’ (โˆ€ a โ†’ a ยท e โ‰ก a)
  โ†’ (โˆ€ a โ†’ (i a) ยท a โ‰ก e) โ†’ (โˆ€ a โ†’ a ยท (i a) โ‰ก e)
  โ†’ (โˆ€ a b โ†’ a ยท b โ‰ก b ยท a)
  โ†’ AbelianGroup
eqsToAbelianGroup A = Polymorphic.eqsToAbelianGroup {A = A}