Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeApr 1st 2014
   • (edited Apr 1st 2014)
   • PermaLink
   Author: Urs
   Format: MarkdownItexI happened upon our entry _[[ETCS]]_ again (which is mostly a pointer to further entries and further resources) and found that it could do with a little bit more of an Idea-section, before it leaves the reader alone with the decision whether to follow any one of the many further links offered. I have expanded a bit, and now it reads as follows. Please feel invited to criticize and change. (And a question: didn't we have an entry on ETCC, too? Where?) *** The **Elementary Theory of the Category of Sets** ([Lawvere 65](#Lawvere65)), or _ETCS_ for short, is a formulation of [[set theory|set-theoretic]] [[foundations]] in a [[category theory|category-theoretic]] spirit. As such, it is the prototypical [[structural set theory]]. More in detail, ETCS is a [[first-order theory]] axiomatizing [[elementary toposes]] and specifically those which are [[well-pointed topos|well-pointed]], have a [[natural numbers object]] and satisfy the [[axiom of choice]]. The idea is, first of all, that traditional mathematics naturally takes place "[[internal logic|inside]]" such a topos, and second that by varying the axioms much of mathematics may be done inside more general toposes: for instance omitting the [[well-pointed topos|well-pointedness]] and the [[axiom of choice]] but adding the [[Kock-Lawvere axiom]] gives a [[smooth topos]] inside which [[synthetic differential geometry]] takes place. Modern mathematics with emphasis on concepts of [[homotopy theory]] would more directly be founded in this spirit by an axiomatization not just of [[elementary toposes]] but by [[elementary (∞,1)-toposes]]. This is roughly what [[univalence|univalent]] [[homotopy type theory]] accomplishes, for more on this see at _[relation between type theory and category theory -- Univalent HoTT and Elementary infinity-toposes](relation+between+type+theory+and+category+theory#HomotopyWithUnivalence)_. Instead of increasing the [[higher category theory|higher categorical dimension]] [[(n,r)-category|(n,r)]] in the first argument, one may also, in this context of elementary foundations, consider raising the second argument. The case $(2,2)$ is the [[elementary theory of the 2-category of categories]] (ETCC). ***

   I happened upon our entry ETCS again (which is mostly a pointer to further entries and further resources) and found that it could do with a little bit more of an Idea-section, before it leaves the reader alone with the decision whether to follow any one of the many further links offered.

   I have expanded a bit, and now it reads as follows. Please feel invited to criticize and change. (And a question: didn’t we have an entry on ETCC, too? Where?)

   ---

   The Elementary Theory of the Category of Sets (Lawvere 65), or ETCS for short, is a formulation of set-theoretic foundations in a category-theoretic spirit. As such, it is the prototypical structural set theory.

   More in detail, ETCS is a first-order theory axiomatizing elementary toposes and specifically those which are well-pointed, have a natural numbers object and satisfy the axiom of choice. The idea is, first of all, that traditional mathematics naturally takes place “inside” such a topos, and second that by varying the axioms much of mathematics may be done inside more general toposes: for instance omitting the well-pointedness and the axiom of choice but adding the Kock-Lawvere axiom gives a smooth topos inside which synthetic differential geometry takes place.

   Modern mathematics with emphasis on concepts of homotopy theory would more directly be founded in this spirit by an axiomatization not just of elementary toposes but by elementary (∞,1)-toposes. This is roughly what univalent homotopy type theory accomplishes, for more on this see at relation between type theory and category theory – Univalent HoTT and Elementary infinity-toposes.

   Instead of increasing the higher categorical dimension (n,r) in the first argument, one may also, in this context of elementary foundations, consider raising the second argument. The case $(2,2)$ is the elementary theory of the 2-category of categories (ETCC).

   ---