\documentclass[12pt,titlepage]{article} \usepackage{amsmath} \usepackage{mathrsfs} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsthm} \usepackage{mathtools} \usepackage{graphicx} \usepackage{color} \usepackage{ucs} \usepackage[utf8x]{inputenc} \usepackage{xparse} \usepackage{hyperref} %----Macros---------- % % Unresolved issues: % % \righttoleftarrow % \lefttorightarrow % % \color{} with HTML colorspec % \bgcolor % \array with options (without options, it's equivalent to the matrix environment) % Of the standard HTML named colors, white, black, red, green, blue and yellow % are predefined in the color package. Here are the rest. \definecolor{aqua}{rgb}{0, 1.0, 1.0} \definecolor{fuschia}{rgb}{1.0, 0, 1.0} \definecolor{gray}{rgb}{0.502, 0.502, 0.502} \definecolor{lime}{rgb}{0, 1.0, 0} \definecolor{maroon}{rgb}{0.502, 0, 0} \definecolor{navy}{rgb}{0, 0, 0.502} \definecolor{olive}{rgb}{0.502, 0.502, 0} \definecolor{purple}{rgb}{0.502, 0, 0.502} \definecolor{silver}{rgb}{0.753, 0.753, 0.753} \definecolor{teal}{rgb}{0, 0.502, 0.502} % Because of conflicts, \space and \mathop are converted to % \itexspace and \operatorname during preprocessing. % itex: \space{ht}{dp}{wd} % % Height and baseline depth measurements are in units of tenths of an ex while % the width is measured in tenths of an em. \makeatletter \newdimen\itex@wd% \newdimen\itex@dp% \newdimen\itex@thd% \def\itexspace#1#2#3{\itex@wd=#3em% \itex@wd=0.1\itex@wd% \itex@dp=#2ex% \itex@dp=0.1\itex@dp% \itex@thd=#1ex% \itex@thd=0.1\itex@thd% \advance\itex@thd\the\itex@dp% \makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}} \makeatother % \tensor and \multiscript \makeatletter \newif\if@sup \newtoks\@sups \def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}% \def\reset@sup{\@supfalse\@sups={}}% \def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else% \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}% \else \append@sup#2 \@suptrue \fi% \expandafter\mk@scripts\fi} \def\tensor#1#2{\reset@sup#1\mk@scripts#2_/} \def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2% \reset@sup\mk@scripts#3_/} \makeatother % \slash \makeatletter \newbox\slashbox \setbox\slashbox=\hbox{$/$} \def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$} \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa \copy\slashbox \kern-\@tempdima \box\@tempboxa} \def\slash{\protect\itex@pslash} \makeatother % math-mode versions of \rlap, etc % from Alexander Perlis, "A complement to \smash, \llap, and lap" % http://math.arizona.edu/~aprl/publications/mathclap/ \def\clap#1{\hbox to 0pt{\hss#1\hss}} \def\mathllap{\mathpalette\mathllapinternal} \def\mathrlap{\mathpalette\mathrlapinternal} \def\mathclap{\mathpalette\mathclapinternal} \def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}} \def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}} \def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}} % Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2} \let\oldroot\root \def\root#1#2{\oldroot #1 \of{#2}} \renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}} % Manually declare the txfonts symbolsC font \DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n} \SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n} \DeclareFontSubstitution{U}{txsyc}{m}{n} % Manually declare the stmaryrd font \DeclareSymbolFont{stmry}{U}{stmry}{m}{n} \SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n} % Manually declare the MnSymbolE font \DeclareFontFamily{OMX}{MnSymbolE}{} \DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n} \SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n} \DeclareFontShape{OMX}{MnSymbolE}{m}{n}{ <-6> MnSymbolE5 <6-7> MnSymbolE6 <7-8> MnSymbolE7 <8-9> MnSymbolE8 <9-10> MnSymbolE9 <10-12> MnSymbolE10 <12-> MnSymbolE12}{} % Declare specific arrows from txfonts without loading the full package \makeatletter \def\re@DeclareMathSymbol#1#2#3#4{% \let#1=\undefined \DeclareMathSymbol{#1}{#2}{#3}{#4}} \re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116} \re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116} \re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117} \re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117} \re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118} \re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118} \re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119} \re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119} \re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46} \re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121} \re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121} \re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12} \re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64} \re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6} \re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77} \re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77} \makeatother % \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE \makeatletter \def\Decl@Mn@Delim#1#2#3#4{% \if\relax\noexpand#1% \let#1\undefined \fi \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}} \def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}} \def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}} \Decl@Mn@Open{\llangle}{mnomx}{'164} \Decl@Mn@Close{\rrangle}{mnomx}{'171} \Decl@Mn@Open{\lmoustache}{mnomx}{'245} \Decl@Mn@Close{\rmoustache}{mnomx}{'244} \makeatother % Widecheck \makeatletter \DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}} \def\@widecheck#1#2{% \setbox\z@\hbox{\m@th$#1#2$}% \setbox\tw@\hbox{\m@th$#1% \widehat{% \vrule\@width\z@\@height\ht\z@ \vrule\@height\z@\@width\wd\z@}$}% \dp\tw@-\ht\z@ \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@ \setbox\tw@\hbox{% \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box \tw@}}}% {\ooalign{\box\tw@ \cr \box\z@}}} \makeatother % \mathraisebox{voffset}[height][depth]{something} \makeatletter \NewDocumentCommand\mathraisebox{moom}{% \IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{% \IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}% }{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}% \mathpalette\@temp{#4}} \makeatletter % udots (taken from yhmath) \makeatletter \def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.} \mkern2mu\raise4\p@\hbox{.}\mkern1mu \raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}} \makeatother %% Fix array \newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}} %% \itexnum is a noop \newcommand{\itexnum}[1]{#1} %% Renaming existing commands \newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}} \newcommand{\widevec}{\overrightarrow} \newcommand{\darr}{\downarrow} \newcommand{\nearr}{\nearrow} \newcommand{\nwarr}{\nwarrow} \newcommand{\searr}{\searrow} \newcommand{\swarr}{\swarrow} \newcommand{\curvearrowbotright}{\curvearrowright} \newcommand{\uparr}{\uparrow} \newcommand{\downuparrow}{\updownarrow} \newcommand{\duparr}{\updownarrow} \newcommand{\updarr}{\updownarrow} \newcommand{\gt}{>} \newcommand{\lt}{<} \newcommand{\map}{\mapsto} \newcommand{\embedsin}{\hookrightarrow} \newcommand{\Alpha}{A} \newcommand{\Beta}{B} \newcommand{\Zeta}{Z} \newcommand{\Eta}{H} \newcommand{\Iota}{I} \newcommand{\Kappa}{K} \newcommand{\Mu}{M} \newcommand{\Nu}{N} \newcommand{\Rho}{P} \newcommand{\Tau}{T} \newcommand{\Upsi}{\Upsilon} \newcommand{\omicron}{o} \newcommand{\lang}{\langle} \newcommand{\rang}{\rangle} \newcommand{\Union}{\bigcup} \newcommand{\Intersection}{\bigcap} \newcommand{\Oplus}{\bigoplus} \newcommand{\Otimes}{\bigotimes} \newcommand{\Wedge}{\bigwedge} \newcommand{\Vee}{\bigvee} \newcommand{\coproduct}{\coprod} \newcommand{\product}{\prod} \newcommand{\closure}{\overline} \newcommand{\integral}{\int} \newcommand{\doubleintegral}{\iint} \newcommand{\tripleintegral}{\iiint} \newcommand{\quadrupleintegral}{\iiiint} \newcommand{\conint}{\oint} \newcommand{\contourintegral}{\oint} \newcommand{\infinity}{\infty} \newcommand{\bottom}{\bot} \newcommand{\minusb}{\boxminus} \newcommand{\plusb}{\boxplus} \newcommand{\timesb}{\boxtimes} \newcommand{\intersection}{\cap} \newcommand{\union}{\cup} \newcommand{\Del}{\nabla} \newcommand{\odash}{\circleddash} \newcommand{\negspace}{\!} \newcommand{\widebar}{\overline} \newcommand{\textsize}{\normalsize} \renewcommand{\scriptsize}{\scriptstyle} \newcommand{\scriptscriptsize}{\scriptscriptstyle} \newcommand{\mathfr}{\mathfrak} \newcommand{\statusline}[2]{#2} \newcommand{\tooltip}[2]{#2} \newcommand{\toggle}[2]{#2} % Theorem Environments \theoremstyle{plain} \newtheorem{theorem}{Theorem} \newtheorem{lemma}{Lemma} \newtheorem{prop}{Proposition} \newtheorem{cor}{Corollary} \newtheorem*{utheorem}{Theorem} \newtheorem*{ulemma}{Lemma} \newtheorem*{uprop}{Proposition} \newtheorem*{ucor}{Corollary} \theoremstyle{definition} \newtheorem{defn}{Definition} \newtheorem{example}{Example} \newtheorem*{udefn}{Definition} \newtheorem*{uexample}{Example} \theoremstyle{remark} \newtheorem{remark}{Remark} \newtheorem{note}{Note} \newtheorem*{uremark}{Remark} \newtheorem*{unote}{Note} %------------------------------------------------------------------- \begin{document} %------------------------------------------------------------------- \section*{set} \hypertarget{context}{}\subsubsection*{{Context}}\label{context} \hypertarget{foundations}{}\paragraph*{{Foundations}}\label{foundations} [[!include foundations - contents]] \hypertarget{category_theory}{}\paragraph*{{Category theory}}\label{category_theory} [[!include category theory - contents]] \hypertarget{mathematics}{}\paragraph*{{Mathematics}}\label{mathematics} [[!include mathematicscontents]] \hypertarget{sets}{}\section*{{Sets}}\label{sets} \noindent\hyperlink{what_should_a_set_be}{What should a set be?}\dotfill \pageref*{what_should_a_set_be} \linebreak \noindent\hyperlink{what_is_a_set}{What is a set?}\dotfill \pageref*{what_is_a_set} \linebreak \noindent\hyperlink{in_category_theory}{In category theory}\dotfill \pageref*{in_category_theory} \linebreak \noindent\hyperlink{InHoTT}{In homotopy type theory}\dotfill \pageref*{InHoTT} \linebreak \noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak \noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak \noindent\hyperlink{general}{General}\dotfill \pageref*{general} \linebreak \noindent\hyperlink{history}{History}\dotfill \pageref*{history} \linebreak \hypertarget{what_should_a_set_be}{}\subsection*{{What should a set be?}}\label{what_should_a_set_be} The concept of \emph{set} appears in several different guises in [[mathematics]], and particularly in [[category theory]]. It is common to use [[foundations of mathematics]] in which `set' is an undefined term; this is [[set theory]] as a foundation. In a [[pure set|pure]] [[material set theory]] like [[ZFC]], every object is a set. Even in a [[structural set theory|structural approach]] such as [[ETCS]], it is common for every object to be a [[structured set]] in some way or another. Even if sets are not at the bottom of your foundations, still they are probably close. For instance, in [[type theory]] sometimes sets are defined as [[predicates]] on [[types]], or as [[setoids]]. In [[homotopy type theory]], sets are defined as [[truncated object|0-truncated]] homotopy types; see below. Material set theory conflates two notions of sets, which were elegantly (but not first) described by [[Mathieu Dupont]] in \href{http://math.breckes.org/2009/03/the-two-meanings-of-the-word-%E2%80%9Cset%E2%80%9D-in-mathematics/}{a blog post} as `set$^1$' and `set$^2$', which we will here call `abstract set' and `concrete set'. In the latter case (set$^2$), we have some fixed [[universe of discourse]] (say, consisting of all real numbers), and a \textbf{concrete set} is a set of elements of this universe (so a set of real numbers, such as $\{5\}$, $\{ x | x \gt 2 \}$, or $\empty$). In the former case (set$^1$), an \textbf{abstract set} is a purely abstract concept, an unstructured (except perhaps for the [[equality relation]]) collection of unlabelled elements. Arguably (this argument goes back at least to [[Bill Lawvere|Lawvere]]), [[Georg Cantor|Cantor]]'s original concept of [[cardinal number]] (Kardinalzahl) was the abstraction from a concrete set to its underlying abstract set. Here we adopt a structural approach, in which a \textbf{set} is an abstract set, a (mostly) unstructured [[collection]]. For concrete sets, see [[subset]]; if the fixed universe of discourse is an abstract set $S$, then a concrete set will be a subset of $S$. In material set theory (as usually conceived), the fixed universe of discourse is an abstract set (or [[proper class]]) $V$, an abstract set (internal to the theory) is an element of $V$, and a concrete set is a sufficiently [[small set|small]] subset of $V$; the concepts may be identified because $V$ comes with an [[bijection|isomorphism]] to its class of small subsets. \hypertarget{what_is_a_set}{}\subsection*{{What is a set?}}\label{what_is_a_set} We still need to clarify exactly what sort of collection a set is. Although most foundations leave this unspecified, we may (perhaps circularly, and perhaps controversially) define it in various ways, as follows: \hypertarget{in_category_theory}{}\subsubsection*{{In category theory}}\label{in_category_theory} \begin{udefn} A \textbf{set} is a [[category]] (or instead an $\infty$-[[infinity-groupoid|groupoid]] or even an $\infty$-[[infinity-category|category]]) that is [[small category|small]], [[discrete category|discrete]], and [[skeletal category|skeletal]]. \end{udefn} Each of these three adjectives describes a different aspect of what makes something a `set', and they serve different purposes, which should not be conflated. That a set is (in the category-theoretic sense) [[discrete category|discrete]] is the most important point; nobody would call a category a `set' merely because it is small and skeletal. (This clause is also the reason why it makes no difference whether we start from categories, $\infty$-groupois, or $\infty$-categories; discreteness immediately limits us to $0$-[[0-groupoid|groupoids]].) The discreteness of a set reflects its lack of internal structure; while a category may have much structure relating its objects, the only structure remaining in a discrete category is whether any two given objects are [[isomorphism|isomorphic]] (and the fact that isomorphism is an [[equivalence relation]]); if (and only if) they are, then they are considered \textbf{[[equality|equal]]} as elements of the set. That a set is [[small category|small]] allows there to be a collection of `all' sets; this collection is not itself small, but we still have a [[large category]] of all sets, [[Set]]. A category that is merely discrete and skeletal may be called a \textbf{[[class]]} instead. But notice that the difference between a set and a class is a rather technical one; a class is just like a set, only (possibly) larger. Indeed, not everyone would agree with the requirement that a set must be small; although that is probably the most common way of talking to deal with size issues, it is not the only way. Another way, used by no less an authority than \emph{[[Categories Work]]}, is to posit the existence of a strongly [[inaccessible cardinal]] $\kappa$ and define a \textbf{[[small set]]} to be a set whose [[cardinality]] is less than $\kappa$. That a set is [[skeletal category|skeletal]] is arguably the least important requirement; in fact, it is `evil' in the technical sense of violating the [[principle of equivalence]]. A category that is merely small and discrete may be called a \textbf{[[setoid]]} instead. However, if you forbid yourself from referring to [[equality]] of elements of the setoid (which are the objects of the small discrete category) --- or, equivalently, interpret ``equality'' to mean ``isomorphism'' therein --- then you cannot distinguish the setoid from a set; each is merely a (small) collection of elements with an equivalence relation (called `equivalence' in the setoid and `equality' in the set, in both cases corresponding to isomorphism in a small discrete category). While [[size issues]] are real and cannot be ignored completely, it is possible to adopt foundations in which the issue of skeletality simply does not appear. \hypertarget{InHoTT}{}\subsubsection*{{In homotopy type theory}}\label{InHoTT} As [[homotopy type theory]] may be viewed as a theory of $\infty$-[[infinity-groupoid|groupoids]], it falls under the preceding section; but since the language of HoTT is important to learn, let us look at it explicitly: \begin{defn} \label{}\hypertarget{}{} A \textbf{set} is a [[type]] in which there is an operation connecting any two parallel [[identity type|paths]] by a 2-path: \begin{verbatim}Definition is_set A := forall (x y : A) (p q : x == y), p == q\end{verbatim} (There are numerous other equivalent definitions; see [[h-set]].) \end{defn} Because this operation is defined internally, it acts on paths as well as points and implies that, for any two points of $A$, the [[identity type|type of paths]] between them is [[contractible space|contractible]] as soon as it is [[inhabited]]. Regarding types as [[∞-groupoids]], this definition takes care only of the discreteness requirement. Regarding smallness, HoTT is usually formulated in [[Martin-Löf type theory]] with [[universes]] ([[type of types]]). If we have chosen one particular universe as the universe of ``small'' things, then ``setness'' could be restricted to types belonging to that universe. Finally, skeletality is mostly meaningless in HoTT because paths are the only notion of (propositional) [[equality]] which we have to reason with. (There is also the notion of ``definitional'' equality, but as we cannot assert or prove statements of the form ``$x$ and $y$ are definitionally equal'' inside the theory, this is mostly not relevant for the purposes of setness.) \hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts} \begin{itemize}% \item [[Bishop set]], [[setoid]] \item [[definable set]], [[constructible set]] \item [[recursive subset]] \item [[finite set]], [[hereditarily finite set]] \end{itemize} [[!include homotopy n-types - table]] \hypertarget{references}{}\subsection*{{References}}\label{references} \hypertarget{general}{}\subsubsection*{{General}}\label{general} Formalization of sets in [[homotopy type theory]] (via [[h-sets]]) is discussed in \begin{itemize}% \item [[Egbert Rijke]], [[Bas Spitters]], \emph{Sets in homotopy type theory} (\href{http://arxiv.org/abs/1305.3835}{arXiv:1305.3835}) \end{itemize} \hypertarget{history}{}\subsubsection*{{History}}\label{history} An early definition of ``set'' appears in \begin{itemize}% \item Bernard Bolzano, \emph{Paradoxien des Unendlichen} (1847) \end{itemize} where in section 4 it says in translation \begin{quote}% There are wholes which, although they contain the same parts A, B, C, D, \ldots{}, nevertheless present themselves as different when seen from our point of view or conception (this kind of difference we call `essential'), e.g. a complete and a broken glass viewed as a drinking vessel. \ldots{} A whole whose basic conception renders the arrangement of its parts a matter of indifference (and whose rearrangement therefore changes nothing essential from our point of view, if only that changes), I call a set. \end{quote} [[!redirects set]] [[!redirects sets]] [[!redirects abstract set]] [[!redirects abstract sets]] \end{document}