Carter, Hi. This is Spencer Breiner; I am Joie’s supervisor here at NIST. Extensionality is certainly an issue when we are talking about categorical models of type theory, but I don’t see it as such an issue here (which could just be lack of insight). Certainly it would depend on which type of functional component in the software is involved. In the simplest case, defining a finite category of paths from a directed acyclic graph poses no problems; ditto for path equations in the finite case. Of course, once we allow cyclic graphs we can get infinite categories, and (if I remember correctly) path equations becomes semi-decidable. In particular, we really need to distinguish between the abstract category and its presentation in terms of generators and relations. Whether this is a problem or not depends on what we want to do with the category. Functors out are no problem, functors in might be. The real issue seems to be whether you need and are able to check equalities between arrows. Where it does arise, I suspect the solution would be something like in HoTT, where we use computer-aided proof search to verify the equations that we need. Are there particular sorts of things that you would like to do with categories (besides modeling type theory ;-), where you think these sorts of issues would probably arise? For the work with Joie we are focused on user interface and functional requirements, but I am very interested in these sorts of questions. Thanks, Spencer From: Carter Schonwald [mailto:carter.schonwald@gmail.com] Sent: Monday, June 27, 2016 10:02 AM To: Murphy, Joie R. (Assoc) ; Breiner, Spencer J. (Fed) Cc: Subrahmanian, Eswaran (Assoc) ; haskell-cafe@haskell.org Subject: Extensionality in category theory RE: [Haskell-cafe] User Requirements Survey for CT Software (Beta) 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) mailto:spencer.breiner@nist.gov> Sent: Monday, June 27, 2016 9:44 AM Subject: RE: [Haskell-cafe] User Requirements Survey for CT Software (Beta) To: Carter Schonwald mailto:carter.schonwald@gmail.com>, Murphy, Joie R. (Assoc) mailto:joie.murphy@nist.gov> Cc: Subrahmanian, Eswaran (Assoc) mailto:eswaran.subrahmanian@nist.gov> 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) mailto:joie.murphy@nist.gov> Cc: haskell-cafe@haskell.orgmailto:haskell-cafe@haskell.org; Subrahmanian, Eswaran (Assoc) mailto:eswaran.subrahmanian@nist.gov>; Breiner, Spencer J. (Fed) mailto:spencer.breiner@nist.gov> 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) mailto:joie.murphy@nist.gov> 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