Hi Serge,<br><br>(1)<br>    Yes, field identifiers do not need to be unique.<br><br>(2)<br>    Yes, this defines a setoid for every Semigroup.<br><br>(2.1)<br>    On the lines before, you will see that it says<br>        open IsSemigroup isSemigroup public<br>

    and that brings isEquivalence from IsSemigroup into scope,<br>    so that is what is on the right side of the equality.<br><br>(2.2)<br>    The other fields can be inferred because of type dependencies.<br>    It is the same thing here, proj₁ is inferred and does not<br>

    need to be spelled out:<br><br>        vector : Vec ⊤ 1<br>        vector = tt ∷ []<br><br>        vector′ : Σ ℕ (Vec ⊤)<br>        vector′ = record { proj₂ = vector }<br><br>(3) If you try this, you will get the error message:<br>

    `The record type Semigroup does not have the fields setoid&#39;<br>    If you look carefully at the definition of Semigroup, you&#39;ll see<br>    that setoid is not defined under the keyword field. Rather,<br>    if you have a Semigroup at hand, you can get the setoid of it<br>

    (for instance by opening it).<br><br>Cheers,<br>Dan<br><div class="gmail_quote">On Wed, Aug 29, 2012 at 1:43 PM, Serge D. Mechveliani <span dir="ltr">&lt;<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>&gt;</span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">People,<br>
I have a couple of a beginner questions on Semigroup in<br>
Standard library  (Agda-2.3.0.1 + lib-0.6).<br>
<br>
The library declares<br>
<br>
--------------------------------------------------<br>
record Setoid c Б└⌠ : Set (suc (c Б┼■ Б└⌠)) where<br>
  infix 4 _Б┴┬_<br>
  field<br>
    Carrier       : Set c<br>
    _Б┴┬_           : Rel Carrier Б└⌠<br>
    isEquivalence : IsEquivalence _Б┴┬_<br>
  ...<br>
--------------------------------------------------<br>
record IsSemigroup {a Б└⌠} {A : Set a} (Б┴┬ : Rel A Б└⌠)<br>
                   (Б┬≥ : OpБ┌┌ A) : Set (a Б┼■ Б└⌠) where<br>
  open FunctionProperties Б┴┬<br>
  field<br>
    isEquivalence : IsEquivalence Б┴┬<br>
    ...<br>
  ...<br>
--------------------------------------------------<br>
record Semigroup c Б└⌠ : Set (suc (c Б┼■ Б└⌠)) where<br>
  infixl 7 _Б┬≥_<br>
  infix  4 _Б┴┬_<br>
  field<br>
    Carrier     : Set c<br>
    _Б┴┬_         : Rel Carrier Б└⌠<br>
    _Б┬≥_         : OpБ┌┌ Carrier<br>
    isSemigroup : IsSemigroup _Б┴┬_ _Б┬≥_<br>
<br>
  open IsSemigroup isSemigroup public<br>
  setoid : Setoid _ _<br>
  setoid = record { isEquivalence = isEquivalence }<br>
-------------------------------------------------------<br>
<br>
And it occurs the following.<br>
(1) The  setoid  value also has operations named  Carrier and _Б┴┬_<br>
    -- as in the signature of  Semigroup.<br>
<br>
(2) The line  `setoid = record { isEquivalence = isEquivalence }&#39;<br>
    is an implementation for the operation  setoid.<br>
<br>
(2.1) What does it mean this `= isEquivalence&#39; ?<br>
      Is it  IsSemigroup.isEquivalence  produced by opening<br>
      IsSemigroup ?<br>
<br>
(2.2) This implementation for  setoid  skips the fields of<br>
      Carrier  and  _Б┴┬_  in Setoid.<br>
I try an example of<br>
  record Foo : Set where field f1 : Bool<br>
                               f2 : Б└∙<br>
  r : Foo<br>
  r = record { f1 = true }<br>
<br>
And it is not compiled -- until I add a definition for f2.<br>
How does Standard library manage here to skip the two fields in<br>
setoid ?<br>
<br>
(3) The  setoid  part in Semigroup  must agree with the Semigroup<br>
    signature values, in particular, to refer to the same<br>
    Setoid.Carrier  value that  Semigroup.Setoid.<br>
That is there must hold for each  h : Semigroup<br>
        Setoid.Carrier $ Semigroup.setoid h = Semigroup.Carrier h<br>
Right?<br>
Where is this law specified?<br>
For example, an user can define erroneousely<br>
(instead of the Library&#39;s):<br>
  integerSemigroup : Semigroup _ _<br>
  integerSemigroup = record { Carrier = Integer;<br>
                              setoid  = record { Carrier = Bool; ... }<br>
                              ...<br>
                            }.<br>
It does not agree with algebra, but Agda will take it (?).<br>
Am I missing something?<br>
<br>
Can you explain, please?<br>
Thank you in advance,<br>
<br>
------<br>
Sergei<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br>
<br>
</blockquote></div><br>