Skip to content

Classical.Small.Structures.Group

Level-fixed Group

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

Specializes Classical.Structures.Group to the common case where the universe level of both the carrier and the equivalence is 0โ„“ (i.e., Set-valued carriers with propositional or set-truncated equivalence), mirroring the analogous veneers for Magma, Semigroup, Monoid, etc.

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

module Classical.Small.Structures.Group 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.Group as Polymorphic

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

eqsToGroup : (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)
  โ†’ Group
eqsToGroup A = Polymorphic.eqsToGroup {A = A}