[Agda] Accessing fields of algebra records

[N. Raghavendra]

Hi,

How do I access the inner fields of complex records, e.g., the
multiplicative identity of a commutative semiring?  If I write this:

1*n≡n : (n : ℕ) → 1 * n ≡ n
1*n≡n = CSR.isCommutativeSemiring.*-isCommutativeMonoid.identityˡ
  where
    module CSR = CommutativeSemiring Data.Nat.Properties.commutativeSemiring

I get an error.

Thanks and cheers,
Raghu.

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