[Agda] Inheriting fields

[N. Raghavendra]

The Algebra module of stdlib defines

--8<---------------cut here---------------start------------->8---
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 }
--8<---------------cut here---------------end--------------->8---

and Relation.Binary defines

--8<---------------cut here---------------start------------->8---
record Setoid c ℓ : Set (suc (c ⊔ ℓ)) where
  infix 4 _≈_
  field
    Carrier       : Set c
    _≈_           : Rel Carrier ℓ
    isEquivalence : IsEquivalence _≈_
--8<---------------cut here---------------end--------------->8---

So to specify setoid within the Semigroup definition, we don't need to
write

--8<---------------cut here---------------start------------->8---
...
  setoid : Setoid
  setoid = record { Carrier = Carrier
                  ; _≈_ = _≈_
                  ; isEquivalence = isEquivalence
                  }
--8<---------------cut here---------------end--------------->8---

The Carrier and _≈_ fields in setoid seem to be inherited from the
Semigroup.  Is there some document which describes such inheritance?
I've seen the records section and tutorial in the reference manual, but
couldn't find this.

Thanks,
Raghu.

-- 
N. Raghavendra <raghu at hri.res.in>, http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/