[Agda] Re: Accessing fields of algebra records
N. Raghavendra
raghu at hri.res.in
Tue Mar 10 15:13:51 CET 2015
At 2015-03-10T16:36:05+04:00, Sergei Meshveliani wrote:
> This leads to a very large expression. And this is replaced with
>
> open Semigroup Ring.+semigroup R using () renaming (_∙_ to _+_)
If we replace Semigroup with IsCommutativeMonoid, Ring.+semigroup with
CommutativeSemiring.*-isCommutativeMonoid, and R with
NatProp.commutativeSemiring, and omit the using/renaming parts, in your
example above, it looks quite like what I'd written, namely,
1*n≡n : (n : ℕ) → 1 * n ≡ n
1*n≡n = identityˡ
where
open IsCommutativeMonoid
(CommutativeSemiring.*-isCommutativeMonoid NatProp.commutativeSemiring)
I was only wondering if there's an easier way to call the various
forgetful functors.
Cheers,
Raghu.
--
N. Raghavendra <raghu at hri.res.in>, http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/
More information about the Agda
mailing list