[Agda] small oddity of DistributesOver in the standard library 0.7

[Nils Anders Danielsson]

On 2014-06-02 13:14, Kenichi Asai wrote:
> Why is M.distrib^l not provided for (B)?

When I wrote that code I included distribʳ as a field, but not distrib,
because distrib can be proved as a derived property. I don't remember
why I chose distribʳ over distribˡ.

The name distribʳ doesn't really match the style used in the library. I
think my idea was that this name shouldn't be used as a projection
(except in the definition of distrib), but only to define records.

-- 
/NAD