<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
  </head>
  <body text="#000000" bgcolor="#FFFFFF">
    <p>On 2019-08-04 4:08 a.m., Matthew Daggitt wrote:<br>
    </p>
    <blockquote type="cite"
cite="mid:CAH9g8GnFNwJafUroYK2Hz5J+BEwbjjBkeGjJceFk4-AoBPcLbQ@mail.gmail.com">
      <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
      <div dir="ltr">Dear all,<br>
        <div> This is a question for anyone who uses the raw algebraic
          structures from the standard library. Currently `RawMagma`,
          `RawMonoid`, `RawRing` etc. contain no axioms whatsoever.
          We're not entirely convinced this is the right approach as
          without proofs that <span style="color:rgb(36,41,46);font-family:SFMono-Regular,Consolas,"Liberation Mono",Menlo,monospace;font-size:12px;white-space:pre">_≈_ </span>is
          an equivalence, and that <span style="color:rgb(36,41,46);font-family:SFMono-Regular,Consolas,"Liberation Mono",Menlo,monospace;font-size:12px;white-space:pre">_∙_</span> is
          congruent with respect to it then it is impossible to do any
          reasoning at all about them. In order to make them more useful
          we're considering changing their definitions so that they
          include the equality axioms above. </div>
        <div><br>
        </div>
        <div>Basically the question is does anyone have a use case for
          the raw structures in which the equality axioms would be
          problematic to provide?</div>
      </div>
    </blockquote>
    <p><br>
    </p>
    <p>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. <br>
    </p>
    <p>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.</p>
    <p>In other words, you're not supposed to reason with the Raw*
      structures. You just compute with them. And if the answer is
      wrong, well, you get what you deserve, as you skipped the proofs.
      [If you get a wrong answer from a computation that was induced
      from building a RawMonoid from a Monoid, and some kind of proper
      'function' similarly obtained by a forgetful morphism, *that*
      would be a serious bug].</p>
    <p>Jacques</p>
    <p>PS: I consider the human-written Raw* structures to be a hack for
      efficiency [possibly strongly needed]; to me, these should be
      produced by an 'erase' meta-program applied to structures and
      morphisms. Eventually, even that ought to disappear, when some
      meta-theorem can be "proved" that this is not even necessary. That
      may not be soon.<br>
    </p>
  </body>
</html>