<div dir="ltr"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">I think I included the raw structures to make it possible to use<br>structures that do not support all the laws, or to avoid having to prove<br>all the laws. For instance, I don't think it is possible (ignoring bugs)<br>to prove the monad laws for the TC monad (with propositional equality as<br>the equality relation).<br></blockquote><div><br></div><div>Thanks for the example! Of course, it would so happen that with propositional equality then anything would trivially still fulfil the proposed new definition of the `Raw` structures. Nonetheless I think I'm convinced that maybe we need a separate set of structures rather than simply changing the existing ones. Thanks all for the input.</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sat, Aug 17, 2019 at 6:08 PM Nils Anders Danielsson <<a href="mailto:nad@cse.gu.se">nad@cse.gu.se</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">On 05/08/2019 17.38, Jacques Carette wrote:<br>
> My understanding (which is perhaps wrong) is that the whole point of<br>
> the Raw* structures is to do Haskell-like computations, where one is<br>
> visibly not carrying around any extra proof baggage, 'by<br>
> construction'. These computations work in a 'trust me' environment.<br>
> <br>
> Ideally one would work with Magma, Monoid, Ring, etc, but without<br>
> knowing for sure that all proofs will be considered irrelevant [so<br>
> that they don't interfere with computation time], it's tempting to<br>
> just hand-erase all those pesky proofs, just to be sure.<br>
<br>
Typically one computes with the carrier type, not the full structure.<br>
<br>
I think I included the raw structures to make it possible to use<br>
structures that do not support all the laws, or to avoid having to prove<br>
all the laws. For instance, I don't think it is possible (ignoring bugs)<br>
to prove the monad laws for the TC monad (with propositional equality as<br>
the equality relation).<br>
<br>
-- <br>
/NAD<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>