Hey Joie, I'll cc the list because certain list members (Dan, Gershom, and others) can better clarify / expound on this topic
Probably the simplest example is function extensionality , that is the reasoning principle that if forall X , g X == f X , then g == f
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.
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!
https://ncatlab.org/nlab/show/equality
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.
-Carter
_____________________________
From: Breiner, Spencer J. (Fed)
Sent: Monday, June 27, 2016 9:44 AM
Subject: RE: [Haskell-cafe] User Requirements Survey for CT Software (Beta)
To: Carter Schonwald , Murphy, Joie R. (Assoc)
Cc: Subrahmanian, Eswaran (Assoc)
Carter,
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.
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.
Let me know and I’m happy to talk some more.
Thanks again,
Spencer Breiner
NIST
From: Carter Schonwald [mailto:carter.schonwald@gmail.com]
Sent: Friday, June 24, 2016 8:35 PM
To: Murphy, Joie R. (Assoc)
Cc: haskell-cafe@haskell.org; Subrahmanian, Eswaran (Assoc) ; Breiner, Spencer J. (Fed)
Subject: Re: [Haskell-cafe] User Requirements Survey for CT Software (Beta)
How do you plan to handle extensional elements of category theory?
On Friday, June 24, 2016, Murphy, Joie R. (Assoc) wrote:
Hello,
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.
The survey is available on Google Forms:http://goo.gl/forms/vfOgR26dHnKynHU23
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.
We would like to thank you for your participation in this initial step of the development process.
Regards,
Joie Murphy
