Group.fm

import Dependencies
import Relation
import Operation
import Magma

// ========================================================
// =                     Definition                       =
// ========================================================

T Group<A : Type, s : Setoid(A)>
| group
  ( f           : Op2(A)
  , e           : A
  , associative : Associative(A,s,f)
  , identity    : Identity(A,s,f,e)
  , inverse     : Inverse(A,s,f,e,identity)
  )

T Semigroup<A : Type, s : Setoid(A)>
| semigroup
  ( f           : Op2(A)
  , associative : Associative(A,s,f)
  )

T Monoid<A : Type, s : Setoid(A)>
| monoid
  ( f           : Op2(A)
  , e           : A
  , associative : Associative(A,s,f)
  , identity    : Identity(A,s,f,e)
  )

// A RegularSemigroup is one which has a regular inversion for every element
T RegularSemigroup<A : Type, s : Setoid(A)>
| regular_semigroup
  ( f           : Op2(A)
  , associative : Associative(A,s,f)
  , inversion   : (x : A) -> Sigma(A, (y : A) => Eq(A,s,y, f(y,f(x,y))))
  )

// An InverseSemigroup is one which has a unique inversion for every element
T InverseSemigroup<A : Type, s : Setoid(A)>
| inverse_semigroup
  ( f : Op2(A)
  , associative : Associative(A,s,f)
  , inversion : (x : A) ->
      Sigma(A, (y : A) => #{Eq(A,s,x, f(x,f(y,x))), Eq(A,s,y,f(y,f(x,y)))})
  )

T Quasigroup<A : Type, s : Setoid(A)>
| quasigroup
  ( f           : Op2(A)
  , latinSquare : LatinSquare(A,s,f)
  )

T LoopQuasigroup<A : Type, s : Setoid(A)>
| loop_quasigroup
  ( f           : Op2(A)
  , e           : A
  , identity    : Identity(A,s,f,e)
  , latinSquare : LatinSquare(A,s,f)
  )

T AbelianGroup<A : Type, s : Setoid(A)>
| abelian_group
  ( f           : Op2(A)
  , e           : A
  , associative : Associative(A,s,f)
  , identity    : Identity(A,s,f,e)
  , inverse     : Inverse(A,s,f,e,identity)
  , commutative : Commutative(A,s,f)
  )

T IdempotentGroup<A : Type, s : Setoid(A)>
| idempotent_group
  ( f           : Op2(A)
  , e           : A
  , associative : Associative(A,s,f)
  , identity    : Identity(A,s,f,e)
  , inverse     : Inverse(A,s,f,e,identity)
  , idempotent  : Idempotent(A,s,f)
  )