[Agda] Raw algebraic structures in the standard library

[Nils Anders Danielsson]

On 05/08/2019 17.38, Jacques Carette wrote:
> My understanding (which is perhaps wrong) is that the whole point of
> the Raw* structures is to do Haskell-like computations, where one is
> visibly not carrying around any extra proof baggage, 'by
> construction'. These computations work in a 'trust me' environment.
> 
> Ideally one would work with Magma, Monoid, Ring, etc, but without
> knowing for sure that all proofs will be considered irrelevant [so
> that they don't interfere with computation time], it's tempting to
> just hand-erase all those pesky proofs, just to be sure.

Typically one computes with the carrier type, not the full structure.

I think I included the raw structures to make it possible to use
structures that do not support all the laws, or to avoid having to prove
all the laws. For instance, I don't think it is possible (ignoring bugs)
to prove the monad laws for the TC monad (with propositional equality as
the equality relation).

-- 
/NAD