\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*{structurally presented set theory}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{foundations}{}\paragraph*{{Foundations}}\label{foundations}

[[!include foundations - contents]]

\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{semiformal_definition}{Semiformal Definition}\dotfill \pageref*{semiformal_definition} \linebreak
\noindent\hyperlink{notions_of_set}{Notions of set}\dotfill \pageref*{notions_of_set} \linebreak
\noindent\hyperlink{structural_presentation}{Structural Presentation}\dotfill \pageref*{structural_presentation} \linebreak
\noindent\hyperlink{consequences_of_structural_presentation}{Consequences of structural presentation}\dotfill \pageref*{consequences_of_structural_presentation} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

A [[structural set theory]] is a set theory which describes \emph{only} structural mathematics. A \textbf{structural presentation} is an attempt to describe formally when a particular (presentation of a) set theory is \emph{structural} in this sense. Paradoxically, this is achieved by requiring that the elements of sets have \emph{no} internal structure.

\hypertarget{semiformal_definition}{}\subsection*{{Semiformal Definition}}\label{semiformal_definition}

The following is an attempted formal definition of when a set theory is structural. It should be regarded as extremely tentative.

\hypertarget{notions_of_set}{}\subsubsection*{{Notions of set}}\label{notions_of_set}

First of all, in order to give a definition pertaining to all set theories, we need to know: what is a set theory? Probably no theory can \emph{intrinsically} be called a set theory; it is only given that distinction by our intent to regard some of its objects of study as ``sets'' and others as their ``elements.'' Thus we make the following definition.

\begin{udefn}
A \textbf{notion of set} in a typed first-order theory consists of:

\begin{itemize}%
\item A type $\mathbb{S}$ called the \emph{type of potential sets}.
\item A unary predicate $set(-)$ on $\mathbb{S}$ called \emph{being a set}.
\item A type $\mathbb{E}_A$, possibly depending on $A\in\mathbb{S}$, called the \emph{type of potential elements of $A$}.
\item A unary predicate $in_A(-)$ on $\mathbb{E}_A$ called \emph{being an element of $A$}.

\end{itemize}
\end{udefn}
We have split the notions of sethood and elementhood into both a type and a predicate to allow for variation in theories which model them by one or the other method or a combination. Here are some examples.

\begin{itemize}%
\item [[ZF]] is a one-typed theory; we call the objects in the one type ``ZF-sets'' for clarity. The type of ZF-sets is the type of potential sets, and we take the predicate $set(-)$ to be $\top$ (every potential set is a set). For such a set $A$, the type of potential elements of $A$ must once again be the type of ZF-sets, and the elementhood predicate is simply $in_A(x) \equiv (x\in A)$.


\item ZF can be augmented by the presence of [[urelement|urelements]] or atoms. One way to represent this is with two types, the type of ZF-sets and the type of ZF-atoms. Again we take the type of ZF-sets to be the type of potential sets, and the sethood predicate $set(-)$ is $\top$. The type of potential elements of $A$ is now the sum type (ZF-sets + ZF-atoms), with the membership predicate again being the ordinary membership predicate of $A$.


\item Atoms can be added to ZF in another way: we maintain only a single type, say the type of ``ZF-objects,'' but we add a ``sethood'' predicate which distinguishes the sets from the atoms. Now the type of potential sets is of course the type of ZF-objects, and the predicate $set(-)$ is the ZF-sethood predicate.


\item In [[NBG]] or [[MK]] set-class theory, there are two possible ``notions of set'': the sets and the classes. The way to formalize this depends on how the set-class theory is stated. For instance, one way to state NBG is with a single type of classes, defining a class $A$ to be an NBG-set when $A\in B$ for some class $B$. In this case the sethood predicate (for the ``NBG-set'' notion of set) will be $set(A) \equiv (\exists B. A\in B)$.


\item In [[SEAR]], which is a dependently typed theory, we take the type of potential sets to be the type of SEAR-sets, with the sethood predicate $set(-)$ being again $\top$. For each set $A$, of course $\mathbb{E}_A$ is the type of SEAR-elements of $A$. (In contrast to ZF, these types are now nontrivially dependent on $A$.) The elementhood predicate is $\top$, since every object in the type of SEAR-elements of $A$ is an element of $A$ by definition (that is, in SEAR elementhood is a typing assertion).


\item In the variant of SEAR without primitive equality (and thus also in [[SEAR+ε]]), the type of potential sets is the type of ``SEAR-sets equipped with an endo-relation'' (a [[dependent sum]] type). The sethood predicate $set(A,R)$ then asserts that $R$ is an equivalence pre-relation, with the other structure as in ordinary SEAR.


\item Since [[ETCS]] is an extension of the first-order theory of a [[category]], it can be stated in several ways.

\begin{itemize}%
\item If ETCS is stated with two types (objects and arrows), then the type of potential sets is the type of objects (i.e. ETCS-sets) and the sethood predicate is $\top$. The type of potential elements of each set $A$ is the type of arrows (i.e. ETCS-functions), and $in_A(x)$ holds when the target of $x$ is $A$ and its source is a [[terminal object]].


\item If ETCS is stated with [[single-sorted definition of a category|one type]], then the type of potential sets is that type, the sethood predicate is $set(A) \equiv (A=s(A))$, the type of potential elements is of course again the single type, and the elementhood predicate is as in the two-typed version.


\item If ETCS is stated with dependent types (a type $hom(A,B)$ for every pair of objects $A$ and $B$), then the type of potential sets is the type of objects, the sethood predicate is $\top$, the type of potential elements of $A$ is $hom(1,A)$, and the elementhood predicate is $\top$.



\end{itemize}


\end{itemize}
\hypertarget{structural_presentation}{}\subsubsection*{{Structural Presentation}}\label{structural_presentation}

Now we make the following definition.

\begin{udefn}
A notion of set in a typed first-order theory is called \textbf{structurally presented} if for any first-order formula $\varphi$ containing free variables $A:\mathbb{S}$ and $x:\mathbb{E}_A$ (and possibly others), if the only free occurrence of $A$ in $\varphi$ is in the (possibly) dependent type $\mathbb{E}_A$ of the variable $x$, then

\begin{equation}
(\forall \vec{z})(\forall A:\mathbb{S})(\forall x,y:\mathbb{E}_A) \Big(set(A) \Rightarrow in_A(x) \Rightarrow in_A(y) \Rightarrow \big(\varphi \Leftrightarrow \varphi[y/x]\big)\Big)
\label{star}\end{equation}
holds (where $\vec{z}$ denotes all the other free variables of $\varphi$). In words, for every potential set $A$ and every potential elements $x$ and $y$ of $A$, if $A$ is a set and $x$ and $y$ are elements of $A$, then $\varphi$ holds of $x$ if and only if it holds of $y$.

\end{udefn}
Equation \eqref{star} says that all elements of any set $A$ are completely indistinguishable by the formula $\varphi$. This is intended to approximate the idea of a structural set theory: the elements of $A$ have no independent structure (and thus cannot be distinguished from each other) apart from their identity as elements of $A$. Of course, we can't do mathematics without some way to distinguish the elements of a set, but the idea of structural set theory is that this happens only through external structure imposed \emph{on} the set, such as functions and relations, rather than through intrinsic properties of the elements themselves. This is the idea behind the restrictions placed on $\varphi$.

Before we go on, let's first see that ZF is definitely \emph{not} structurally presented. Let $A=\{\emptyset, \{\emptyset\}\}$ be the von Nemuann numeral $2$, and let $\varphi \equiv (x = \emptyset)$. Clearly there are some $x\in A$ such that $\varphi$ holds and others such that it fails, so \eqref{star} is false. Moreover, $\varphi$ satisfies the condition: $A$ does not occur in it at all. For the same reasons, NBG and MK are not structurally presented.

Now, why can't we do the same thing in a structural set theory? Consider SEAR, and let $A$ be a set containing two distinct elements $a$ and $a'$. By analogy to what we did in ZF, we'd like to take $\varphi \equiv (x = a)$, but in SEAR this violates the required condition: $a$ must also be an element of $\mathbb{E}_A$, so $A$ appears elsewhere in $\varphi$ than in the type of $x$ (namely, in the type of $a$). In fact, we can show:

\begin{utheorem}
SEAR is structurally presented.

\end{utheorem}
\begin{proof}
Let $\varphi$ be a formula as in the above definition. Since it does not contain $A$ free (except in the type of $x$), it cannot contain any variables (free \emph{or} bound) denoting elements of $A$ (other than $x$) or relations whose source or target is $A$. But the only atomic formulas in the language of SEAR are equalities of set-elements, equalities of relations, and assertions that a relation holds of a pair of set-elements, and SEAR has no term constructors that could produce an element of some other set from an element of $A$. Thus, the only atomic formula involving $x$ that can appear in $\varphi$ is $x=x$, whose truth is clearly independent of the value of $x$. It follows that the truth value of $\varphi$ must also be so.

\end{proof}
For similar reasons, we have:

\begin{utheorem}
When ETCS is written with dependent hom-types, it is structurally presented.

\end{utheorem}
\begin{proof}
Let $\varphi$ be a formula as above. Similarly to the case of SEAR, $\varphi$ cannot contain any variables other than $x$ that denote functions whose source or target is $A$. Since the only term-constructor in ETCS is function composition, the only terms containing $x$ that can occur in $\varphi$ are composites ending in $x:1\to A$ followed by zero or more applications of $id_A$, such as $x$ itself, $x\circ f$, $\id_A\circ x$, $(x\circ g)\circ h$, or $(id_A\circ x)\circ (i\circ j)$. Note that all of these terms denote functions with target $A$. Moreover, the only possible terms denoting functions of target $A$ are terms of this sort, or else composites of some number of copies of $id_A$ (and nothing else).

Now the only atomic formulas of ETCS are equality between parallel function terms. Since the source of a composite involving $x$ cannot be $A$ (otherwise $A$ would have to occur as the source of the first function-variable in that composite), the only possible such formulas involving $x$ will be equality between two composites containing $x$. But since $1$ is a terminal object, any two functions that factor through it will always be equal. Thus, the truth value of such an atomic formula is independent of the value of $x$, and so the truth value of $\varphi$ must also be so.

\end{proof}
However, if ETCS is written using a two-sorted or one-sorted definition of a category, then it is not structurally presented. For instance, we can take the formula

\begin{displaymath}
\varphi \equiv \big((s(f)=t(x)) \wedge (f\circ x = z)\big)
\end{displaymath}
for variables $f$ and $z$ of type ``arrow''. This formula does not contain $A$ at all, yet its truth value (for a fixed $f$ and $z$) is not independent of $x$. This is why we have defined ``structurally presented'' rather than ``structural''---the presentation matters.

It is, however, easy to modify the two- or one-sorted version of ETCS to make it structurally presented: we simply require the equality relation on functions to be decorated by the source and target sets, and the composition operation on functions to be decorated with the set along which composition occurs. That is, instead of $f=g$ we write $equal(f,g,A,B)$ (which can only hold when $s(f)=s(g)=A$ and $t(f)=t(g)=B$), and instead of $g\circ f$ we write $g\circ_B f$ where $t(f)=s(g)=B$. Now the same argument as for the dependently-typed version applies.

It would be nice to have a definition according to which any ``presentation'' of ETCS would be structural; intuitively, a theory should be structural if it is ``equivalent'' in some sense to a structurally presented one. However, I haven't yet been able to come up with a notion of ``equivalence'' which includes the above modifications of ETCS, yet excludes the equivalence between ETCS and BZC (or ZFC and ETCS+R or SEARC).

\hypertarget{consequences_of_structural_presentation}{}\subsubsection*{{Consequences of structural presentation}}\label{consequences_of_structural_presentation}

From our definition of structural presentation we can deduce some of the other standard properties of structural set theories. The first is that ``elements of different sets cannot be compared for equality.''

\begin{utheorem}
If a structurally presented notion of set includes a notion of equality between the elements of distinct sets, which is symmetric and transitive, then all of its sets are [[subsingletons]].

\end{utheorem}
\begin{proof}
Suppose that we have an equality relation that can relate elements of two distinct sets $A$ and $B$. Thus, for variables $x$ of type $A$ and $z$ of type $B$, we would have an formula $x=z$. By symmetry and transitivity, if $x=z$ and $x'=z$, then $x=x'$. But then \eqref{star} applied to $\varphi\equiv (x=z)$ implies that for any $x,y\colon A$ we have $x=y$, so $A$ must be a subsingleton. Since $A$ was arbitrary, all sets must be subsingletons.

\end{proof}
The second is ``elements of sets are not themselves sets.''

\begin{utheorem}
Suppose that a structurally presented notion of set includes relations $is_A:\mathbb{E}_A\looparrowright\mathbb{S}$, which we regard as giving a way to interpret some elements as sets. Suppose moreover that each $\mathbb{E}_A$ has an equality relation $=_A$, and that $is_A(x,B)$ and $is_A(y,B)$ imply $x =_A y$. Then for any set $A$, if there exist $a:\mathbb{E}_A$ and $B:\mathbb{S}$ such that $is_A(a,B)$, then $A$ must be a subsingleton.

\end{utheorem}
\begin{proof}
Suppose that $is_A(a,B)$ and choose $\varphi\equiv is_A(x,B)$. By \eqref{star} it follows that $is_A(x,B)$ holds for all $x:\mathbb{E}_A$, hence $x =_A y$ for all $x,y:\mathbb{E}_A$, i.e. $A$ is a subsingleton.

\end{proof}
Note that the assumption about equality is quite reasonable if we want to interpret ``$is_A$'' as asserting that a given element \emph{is} a given set (rather than merely being related to one in some way).

[[!redirects structurally presented set theory]] [[!redirects structurally presented set theories]] [[!redirects structurally-presented set theory]] [[!redirects structurally-presented set theories]]



\end{document}