2 ms·

The ‘common’ strategy of going with functions first are mostly due to Type Theoretic Foundations research. The most usual presentation presents the function typ

The ‘common’ strategy of going with functions first are mostly due to Type Theoretic Foundations research. The most usual presentation presents the function type as foundational and inherent for the development. There has been some research pushing towards Function types being a specialization of Relations as types, where relations become the foundational elements. But I think the biggest point of contention in your comment is finding sets (i.e. Domains/Codomains) to be required to define functions. Most of this discussion is inspired (either implicitly or explicitly) by the type theoretic foundations. There is a fundamental difference between sets and types, but they are both used to describe the ‘inputs’ and ‘outputs’ of a function in general discussion. However, type theoretical foundations takes types to be the foundation of mathematics, so sets are then defined in terms of types and do not act as the ‘inputs’ and ‘outputs’ for functions.

layer8 4y ago
Thanks. Can you recommend where I can read up on the precise formal definition of ‘type’ in that sense, and how sets are then defined in terms of types? So far I only have seen (too) informal discussions on that.
- throwaway17_17 4y ago
  I think the first recommendation would be the SEP (Stanford Encyclopedia of Philosophy) article on Type Theory written by Couquand [1]. It is a broad but well founded walk through the basis of type theory and it’s usage as a foundation for both logic and mathematics. It also contains a section discussing Univalent Foundations, which is the foremost area for type theoretic foundations at present. The papers listed in the reference section contain most of the fundamental research results of note. I do think Aczel’s “The type theoretic interpretation of constructive set theory” (1978) and Bell’s “Types, Sets and Categories” (2012), which are both cited are good papers. 1 —- https://plato.stanford.edu/entries/type-theory/ https://plato.stanford.edu/entries/type-theory/

layer8 4y ago

Thanks. Can you recommend where I can read up on the precise formal definition of ‘type’ in that sense, and how sets are then defined in terms of types? So far I only have seen (too) informal discussions on that.

throwaway17_17 4y ago
I think the first recommendation would be the SEP (Stanford Encyclopedia of Philosophy) article on Type Theory written by Couquand [1]. It is a broad but well founded walk through the basis of type theory and it’s usage as a foundation for both logic and mathematics. It also contains a section discussing Univalent Foundations, which is the foremost area for type theoretic foundations at present. The papers listed in the reference section contain most of the fundamental research results of note. I do think Aczel’s “The type theoretic interpretation of constructive set theory” (1978) and Bell’s “Types, Sets and Categories” (2012), which are both cited are good papers. 1 —- https://plato.stanford.edu/entries/type-theory/ https://plato.stanford.edu/entries/type-theory/