[Agda] Semigroup declaration

[Serge D. Mechveliani]

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 
(instead of the Library's):
  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?

Can you explain, please?
Thank you in advance,

------
Sergei