# [Agda] Semigroup declaration

Serge D. Mechveliani mechvel at botik.ru
Wed Aug 29 13:43:06 CEST 2012

```People,
I have a couple of a beginner questions on Semigroup in
Standard library  (Agda-2.3.0.1 + lib-0.6).

The library declares

--------------------------------------------------
record Setoid c Б└⌠ : Set (suc (c Б┼■ Б└⌠)) where
infix 4 _Б┴┬_
field
Carrier       : Set c
_Б┴┬_           : Rel Carrier Б└⌠
isEquivalence : IsEquivalence _Б┴┬_
...
--------------------------------------------------
record IsSemigroup {a Б└⌠} {A : Set a} (Б┴┬ : Rel A Б└⌠)
(Б┬≥ : OpБ┌┌ A) : Set (a Б┼■ Б└⌠) where
open FunctionProperties Б┴┬
field
isEquivalence : IsEquivalence Б┴┬
...
...
--------------------------------------------------
record Semigroup c Б└⌠ : Set (suc (c Б┼■ Б└⌠)) where
infixl 7 _Б┬≥_
infix  4 _Б┴┬_
field
Carrier     : Set c
_Б┴┬_         : Rel Carrier Б└⌠
_Б┬≥_         : OpБ┌┌ Carrier
isSemigroup : IsSemigroup _Б┴┬_ _Б┬≥_

open IsSemigroup isSemigroup public
setoid : Setoid _ _
setoid = record { isEquivalence = isEquivalence }
-------------------------------------------------------

And it occurs the following.
(1) The  setoid  value also has operations named  Carrier and _Б┴┬_
-- as in the signature of  Semigroup.

(2) The line  `setoid = record { isEquivalence = isEquivalence }'
is an implementation for the operation  setoid.

(2.1) What does it mean this `= isEquivalence' ?
Is it  IsSemigroup.isEquivalence  produced by opening
IsSemigroup ?

(2.2) This implementation for  setoid  skips the fields of
Carrier  and  _Б┴┬_  in Setoid.
I try an example of
record Foo : Set where field f1 : Bool
f2 : Б└∙
r : Foo
r = record { f1 = true }

And it is not compiled -- until I add a definition for f2.
How does Standard library manage here to skip the two fields in
setoid ?

(3) The  setoid  part in Semigroup  must agree with the Semigroup
signature values, in particular, to refer to the same
Setoid.Carrier  value that  Semigroup.Setoid.
That is there must hold for each  h : Semigroup
Setoid.Carrier \$ Semigroup.setoid h = Semigroup.Carrier h
Right?
Where is this law specified?
For example, an user can define erroneousely
integerSemigroup : Semigroup _ _
integerSemigroup = record { Carrier = Integer;
setoid  = record { Carrier = Bool; ... }
...
}.
It does not agree with algebra, but Agda will take it (?).
Am I missing something?