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>