<div id="compose" contenteditable="true" style="padding-left: 16px; padding-right: 16px; padding-bottom: 8px;"><div>Hey Joie, I'll cc the list because certain list members (Dan, Gershom, and others) can better clarify / expound on this topic </div><div><br></div><div>Probably the simplest example is function extensionality , that is the reasoning principle that if forall X , g X == f X , then g == f</div><div><br></div><div>My understanding is that it can be derived in a homotopy type theory setting, but in in more standard type theories like vanilla coq / Agda / lean that folks often use to model certain categorical objects, this is at best a not computable axiom. </div><div><br></div><div>The very definitions of an epimorphism and monomorphism (the categorical generalization of the dual pair of surjective and injective mappings) Have a sort of function extensional equality!</div><div><br></div><div>https://ncatlab.org/nlab/show/equality </div><div><br></div><div>Touches a wee bit On the topic of equalities. There's a number of approaches to treating / deciding when two ... Things (a very technical term š)are the same / equal. </div><div><br><div class="acompli_signature">-Carter</div><br></div></div>
<div class="gmail_quote">_____________________________<br>From: Breiner, Spencer J. (Fed) <<a dir="ltr" href="mailto:spencer.breiner@nist.gov" x-apple-data-detectors="true" x-apple-data-detectors-type="link" x-apple-data-detectors-result="0">spencer.breiner@nist.gov</a>><br>Sent: Monday, June 27, 2016 9:44 AM<br>Subject: RE: [Haskell-cafe] User Requirements Survey for CT Software (Beta)<br>To: Carter Schonwald <<a dir="ltr" href="mailto:carter.schonwald@gmail.com" x-apple-data-detectors="true" x-apple-data-detectors-type="link" x-apple-data-detectors-result="1">carter.schonwald@gmail.com</a>>, Murphy, Joie R. (Assoc) <<a dir="ltr" href="mailto:joie.murphy@nist.gov" x-apple-data-detectors="true" x-apple-data-detectors-type="link" x-apple-data-detectors-result="2">joie.murphy@nist.gov</a>><br>Cc: Subrahmanian, Eswaran (Assoc) <<a dir="ltr" href="mailto:eswaran.subrahmanian@nist.gov" x-apple-data-detectors="true" x-apple-data-detectors-type="link" x-apple-data-detectors-result="3">eswaran.subrahmanian@nist.gov</a>><br><br><br><meta content="text/html; charset=utf-8"><meta name="Generator" content="Microsoft Word 15 (filtered medium)"><style><!--/* Font Definitions */@font-face {font-family:"Cambria Math"; panose-1:2 4 5 3 5 4 6 3 2 4;}@font-face {font-family:Calibri; panose-1:2 15 5 2 2 2 4 3 2 4;}/* Style Definitions */p.MsoNormal, li.MsoNormal, div.MsoNormal {margin:0in; margin-bottom:.0001pt; font-size:12.0pt; font-family:"Times New Roman",serif;}a:link, span.MsoHyperlink {mso-style-priority:99; color:blue; text-decoration:underline;}a:visited, span.MsoHyperlinkFollowed {mso-style-priority:99; color:purple; text-decoration:underline;}p.msonormal0, li.msonormal0, div.msonormal0 {mso-style-name:msonormal; mso-margin-top-alt:auto; margin-right:0in; mso-margin-bottom-alt:auto; margin-left:0in; font-size:12.0pt; font-family:"Times New Roman",serif;}span.EmailStyle18 {mso-style-type:personal-reply; font-family:"Calibri",sans-serif; color:#1F497D;}.MsoChpDefault {mso-style-type:export-only; font-family:"Calibri",sans-serif;}@page WordSection1 {size:8.5in 11.0in; margin:1.0in 1.0in 1.0in 1.0in;}div.WordSection1 {page:WordSection1;}--></style><div class="WordSection1"><p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri",sans-serif;color:#1F497D">Carter,</span></p><p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri",sans-serif;color:#1F497D"> </span></p><p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri",sans-serif;color:#1F497D">Thanks for your reply. I removed the Haskell mailing list from the cc because I donāt know the listās etiquette, but please forward this response back to the list if you are aiming for a public discussion.</span></p><p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri",sans-serif;color:#1F497D"> </span></p><p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri",sans-serif;color:#1F497D">Iām not quite sure what you mean by āextensional elementsā? Is this extension in the sense of āone class extends anotherā (in which case this would be expressed explicitly by functors). Or extension in the (related) sense of āthe extension of a propositionā, the elements which satisfy it. These sorts of issues would probably be expressed as functors into (some computational implementation of) finite sets.</span></p><p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri",sans-serif;color:#1F497D"> </span></p><p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri",sans-serif;color:#1F497D">Let me know and Iām happy to talk some more.</span></p><p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri",sans-serif;color:#1F497D"> </span></p><p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri",sans-serif;color:#1F497D">Thanks again,</span></p><p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri",sans-serif;color:#1F497D">Spencer Breiner</span></p><p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri",sans-serif;color:#1F497D">NIST</span></p><p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri",sans-serif;color:#1F497D"> </span></p><p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri",sans-serif;color:#1F497D"> </span></p><p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri",sans-serif;color:#1F497D"> </span></p><div style="border:none;border-left:solid blue 1.5pt;padding:0in 0in 0in 4.0pt"><div><div style="border:none;border-top:solid #E1E1E1 1.0pt;padding:3.0pt 0in 0in 0in"><p class="MsoNormal"><b><span style="font-size:11.0pt;font-family:"Calibri",sans-serif">From:</span></b><span style="font-size:11.0pt;font-family:"Calibri",sans-serif"> Carter Schonwald [<a dir="ltr" href="mailto:carter.schonwald@gmail.com" x-apple-data-detectors="true" x-apple-data-detectors-type="link" x-apple-data-detectors-result="4">mailto:carter.schonwald@gmail.com</a>]<br><b>Sent:</b> Friday, June 24, 2016 8:35 PM<br><b>To:</b> Murphy, Joie R. (Assoc) <<a dir="ltr" href="mailto:joie.murphy@nist.gov" x-apple-data-detectors="true" x-apple-data-detectors-type="link" x-apple-data-detectors-result="5">joie.murphy@nist.gov</a>><br><b>Cc:</b> <a dir="ltr" href="mailto:haskell-cafe@haskell.org" x-apple-data-detectors="true" x-apple-data-detectors-type="link" x-apple-data-detectors-result="6">haskell-cafe@haskell.org</a>; Subrahmanian, Eswaran (Assoc) <<a dir="ltr" href="mailto:eswaran.subrahmanian@nist.gov" x-apple-data-detectors="true" x-apple-data-detectors-type="link" x-apple-data-detectors-result="7">eswaran.subrahmanian@nist.gov</a>>; Breiner, Spencer J. (Fed) <<a dir="ltr" href="mailto:spencer.breiner@nist.gov" x-apple-data-detectors="true" x-apple-data-detectors-type="link" x-apple-data-detectors-result="8">spencer.breiner@nist.gov</a>><br><b>Subject:</b> Re: [Haskell-cafe] User Requirements Survey for CT Software (Beta)</span></p></div></div><p class="MsoNormal"> </p><p class="MsoNormal">How do you plan to handle extensional elements of category theory? <br><br>On Friday, June 24, 2016, Murphy, Joie R. (Assoc) <<a href="mailto:joie.murphy@nist.gov">joie.murphy@nist.gov</a>> wrote:</p><blockquote style="border:none;border-left:solid #CCCCCC 1.0pt;padding:0in 0in 0in 6.0pt;margin-left:4.8pt;margin-right:0in"><div><div><p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto">Hello,</p><p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto"> </p><p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto">My name is Joie Murphy and I am a Summer Research Student at the US National Institute of Standards and Technology (NIST), working with Drs. Spencer Breiner and Eswaran Subrahmanian. We are currently gathering user requirements for category theoretic software to be developed by or with NIST in the future. This questionnaire will give us insight about your past or present use of CT software and your ideal uses for such software. Providing us with the information on how you would like to use this type of software will help us to make the right design choices in development.</p><p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto"> </p><p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto">The survey is available on Google Forms:<a href="http://goo.gl/forms/vfOgR26dHnKynHU23">http://goo.gl/forms/vfOgR26dHnKynHU23</a></p><p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto"> </p><p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto">If you have any colleagues who might be willing to fill out this survey, you can forward our message or you can provide us with their contact information at the end of the survey. If you have any questions or concerns, please feel free to contact us by replying to this email.</p><p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto"> </p><p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto">We would like to thank you for your participation in this initial step of the development process.</p><p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto"> </p><p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto">Regards,</p><p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto">Joie Murphy</p><p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto"> </p></div></div></blockquote></div></div><br><br></div>