\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*{extensional relation}

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

\hypertarget{relations}{}\paragraph*{{Relations}}\label{relations}

[[!include relations - contents]]

\hypertarget{extensional_relations}{}\section*{{Extensional relations}}\label{extensional_relations}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{definitions}{Definitions}\dotfill \pageref*{definitions} \linebreak
\noindent\hyperlink{weak_extensionality}{Weak extensionality}\dotfill \pageref*{weak_extensionality} \linebreak
\noindent\hyperlink{finsler_extensionality}{Finsler extensionality}\dotfill \pageref*{finsler_extensionality} \linebreak
\noindent\hyperlink{scott_extensionality}{Scott extensionality}\dotfill \pageref*{scott_extensionality} \linebreak
\noindent\hyperlink{strong_extensionality}{Strong extensionality}\dotfill \pageref*{strong_extensionality} \linebreak
\noindent\hyperlink{examples}{Examples}\dotfill \pageref*{examples} \linebreak
\noindent\hyperlink{extensional_quotients}{Extensional quotients}\dotfill \pageref*{extensional_quotients} \linebreak
\noindent\hyperlink{simulations}{Simulations}\dotfill \pageref*{simulations} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


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

Given an extensional relation $\prec$ on a set, two elements are equal if they cannot be distinguished by the structure of the set of elements that they are related to, that those elements are related to, and so on forever in one direction. We generally think of $x \prec y$ as saying that $x$ is a `member' of $y$, so that $\prec$ is extensional when ``$x$ is determined by its members'' as in the [[axiom of extensionality]] for material [[set theory]].

\hypertarget{definitions}{}\subsection*{{Definitions}}\label{definitions}

We begin with the historically first definition, which is correct for [[well-founded relations]]. We then consider ways to extend this to more general relations, where the last version seems to be most correct.

\hypertarget{weak_extensionality}{}\subsubsection*{{Weak extensionality}}\label{weak_extensionality}

A relation $\prec$ on a set $S$ is \textbf{weakly extensional} if, given any elements $x$ and $y$ of $S$, $x = y$ whenever (for all $t$) $t \prec x$ if and only if $t \prec y$.

Interpreting $\prec$ as membership $\in$, this corresponds to the [[axiom of extensionality]] as usually stated for [[pure sets]]. However, it is really only appropriate when $\prec$ is [[well-founded relation|well-founded]], just as the usual axiom of extensionality must be strengthened in the absence of the [[axiom of foundation]].

However, when $\prec$ is well-founded, weak extensionality is equivalent to all the stronger notions below; thus in that case it is usually called just \textbf{extensionality}.

\hypertarget{finsler_extensionality}{}\subsubsection*{{Finsler extensionality}}\label{finsler_extensionality}

Let $\prec^*$ be the reflexive-[[transitive closure]] of the relation $\prec$ on $S$ (so $\prec^*$ is a [[preorder]]). Given an element $y$ of $S$, let $S \downarrow^* y$ be the [[downset]] of $y$ under $\prec^*$:

\begin{displaymath}
S \downarrow^* y = \{ x: S \;|\; x = t_0 \prec \cdots \prec t_n = y \}
\end{displaymath}
with $n \geq 0$. Note that $y$ itself belongs to $S \downarrow^* y$ (through $n = 0$, if in no other way), so we may take it to be a [[pointed set]]. Then $\prec$ is \textbf{Finsler-extensional} if it is weakly extensional and, given any elements $x$ and $y$ of $S$, $x = y$ whenever $S \downarrow^* x$ and $S \downarrow^* y$ are isomorphic as pointed sets equipped with a relation $\prec$.

Note that this definition includes weak extensionality, which won't follow from the other half unless $\prec$ is well-founded (see the examples below). It is possible to get weak extensionality free by using the [[transitive closure]] $\prec^+$ instead; that is, define $S \downarrow^+ y$ with $n \gt 0$ only. But then you need another step; define $(S \downarrow^+ y)^\top$ to be a pointed set with a new point $\top$ adjoined to $S \downarrow^+ y$; let $x \prec \top$ if and only if $x \prec y$ in $S$ itself. (For a well-founded relation, $(S \downarrow^+ y)^\top \cong S \downarrow^* y$; in general, however, $y$ may already belong to $S \downarrow^+ y$, yet $y \ne \top$ in $(S \downarrow^+ y)^\top$.) Then $\prec$ is Finsler-extensional on $S$ if and only if $x = y$ whenever $(S \downarrow^+ x)^\top \cong (S \downarrow^+ y)^\top$ as pointed sets equipped with $\prec$.

It is immediate that Finsler extensionality implies weak extensionality; the converse may be proved (using [[induction]]) for well-founded relations.

\hypertarget{scott_extensionality}{}\subsubsection*{{Scott extensionality}}\label{scott_extensionality}

Given an element $y$ of $S$, let a \textbf{path} to $y$ consist of a sequence

\begin{displaymath}
x = t_0 \prec \cdots \prec t_n = y
\end{displaymath}
for $n \geq 0$. Then let $T_y$ be the set of paths to $y$; given paths $\vec{t}$ and $\vec{u}$ in $N_y$, say that $\vec{t} \to \vec{u}$ if $\vec{u} = (t_1, \ldots, t_m)$ for some $m \leq n$. Then $T_y$ with the relation $\to$ is the \textbf{tree} to $y$.

$S$ is \textbf{Scott-extensional} if the only [[automorphism]] of any such tree $T_y$ (as a set equipped with a relation $\to$) is the [[identity function]] on $T_y$.

Then Scott extensionality implies Finsler extensionality, and the converse holds for well-founded relations.

\hypertarget{strong_extensionality}{}\subsubsection*{{Strong extensionality}}\label{strong_extensionality}

The strongest version of extensionality is motivated by the study of [[terminal coalgebra]]s and [[coinduction]].

Let $S$ be equipped with a binary relation $\prec$. A \textbf{[[bisimulation]]} on $(S,\prec)$ is a binary relation $\sim$ such that whenever $x \sim y$, for any $a \prec x$ there is a $b \prec y$ with $a \sim b$, and conversely for every $b \prec y$ there is an $a \prec x$ with again $a \sim b$. We then say that $\prec$ is \textbf{strongly extensional} if every bisimulation is contained in the identity relation; i.e., $x = y$ whenever $x \sim y$ for any bisimulation $\sim$. In general, this is probably the best situation in which to say that $\prec$ is simply \textbf{extensional}.

Finsler and Scott extensionality may be understood as special cases of this for particular bisimulations $\sim$. (So can strong extensionality, since any set equipped with a relation has a weakest bisimulation $\approx$.) This is the approach taken by Aczel to study all the above notions of extensionality together.

In particular, strong extensionality implies Scott extensionality, and the converse holds for well-founded relations. Thus, all forms of extensionality are equivalent for well-founded relations.

\hypertarget{examples}{}\subsection*{{Examples}}\label{examples}

\begin{itemize}%
\item The [[axiom of extensionality]] in material [[set theory]] states membership is an extensional relation on the class of [[pure sets]]. (Note that the [[axiom of foundation]] states that membership is a well-founded relation, so one usually doesn't worry about the different notions of extensionality for ill-founded relations.) More generally, the membership relation on the [[transitive closure]] or reflexive-transtive closure of a pure set is an extensional relation on a set.


\item Conversely, one can \emph{define} [[pure set]]s in \emph{structural} [[set theory]] in part as sets equipped with an extensional (and optionally well-founded) relation.


\item A [[well-order]] is precisely a well-founded, [[transitive relation|transitive]], extensional relation. Removing well-foundedness here gives a theory of ill-founded [[ordinal number]]s.


\item On the set $\mathbf{2} = \{0,1\}$, now let $0 \prec 0$ and $0 \prec 1$ (but no other relationships). This relation is not weakly extensional, although it does satisfy the other half of Finsler extensionality, since $\mathbf{2} \downarrow^* 0 \ncong \mathbf{2} \downarrow^* 1$. However, $(\mathbf{2} \downarrow^+ 0)^\top \cong (\mathbf{2} \downarrow^+ 1)^\top$; this shows the necessity of defining Finsler extensionality as we do.


\item On the set $\mathbf{2}$ again, let $0 \prec 1$ and $1 \prec 0$ (but $0 \nprec 0$ and $1 \nprec 1$). This relation is weakly extensional but not Finsler-extensional, since $\mathbf{2} \downarrow^* 0 \cong \mathbf{2} \downarrow^* 1$. Yet $0$ and $1$ can hardly be distinguished by $\prec$ when there is an [[automorphism]] of $(\mathbf{2},\prec)$ that swaps them; this and the other examples below motivate the stronger notions of extensionality.


\item On the set $\mathbf{3} = \{0,1,2\}$, let $2 \nprec 0$ and $i \nprec i$ but all other relationships hold. Then this relation is Finsler-extensional but not Scott-extensional, since $T_2 \cong T_1$.


\item Finally, on the set $\mathbf{2}$ again, let $1 \nprec 0$ but all other relationships hold. Then this relation is Scott-extensional but not strongly extensional, since $0 \approx 1$.



\end{itemize}
\hypertarget{extensional_quotients}{}\subsection*{{Extensional quotients}}\label{extensional_quotients}

Weak extensionality is a kind of [[antisymmetric relation|antisymmetry]] condition: Let $x \leq y$ mean that $t \prec y$ whenever $t \prec x$. Then $\leq$ is clearly a [[preorder]], which is antisymmetric (so a [[partial order]]) if and only if $\prec$ is weakly extensional.

Now suppose that if $t \prec x$ if and only if $t \prec y$ for all $t$, then $x \prec z$ if and only if $y \prec z$ for all $z$. Then if we define $x \equiv y$ to mean that $x \leq y$ and $y \leq x$, then $\equiv$ is an equivalence relation such that $\prec$ descends to a weakly extensional relation on the [[quotient set]] $S/{\equiv}$.

Strongly extensional quotients are even easier to construct, although they do create additional relationships. It is easy to see that the union of any family of bisimulations is a bisimulation, and therefore there is a largest bisimulation $\approx$ for any binary relation $\prec$ on $S$. Moreover, $\approx$ is an equivalence relation (though not every bisimulation need be so), and $\prec$ descends to a strongly extensional relation on the quotient $S/\approx$.

\hypertarget{simulations}{}\subsection*{{Simulations}}\label{simulations}

Given two sets $S$ and $T$, each equipped with a strongly extensional relation $\prec$, a [[function]] $f\colon S \to T$ is a \textbf{[[simulation]]} of $S$ in $T$ if

\begin{itemize}%
\item $f(x) \prec f(y)$ whenever $x \prec y$ and
\item given $t \prec f(x)$, there exists $y \prec x$ with $t = f(y)$.

\end{itemize}
Then sets so equipped form a [[category]] with simulations as [[morphism]]s.

Note that there is at most one simulation from $S$ to $T$; in fact, strong extensionality for $T$ is equivalent to saying that any two simulations $S \rightrightarrows T$ are equal. Also, any simulation from $S$ to $T$ must be an [[injection]]; in fact, strong extensionality for $S$ is equivalent to saying that any simulation $S \to T$ is injective.

Thus, we have a (large) [[poset]] of sets equipped with extensional relations, and we can consistently interpret the simulations as [[subset]] inclusion. This leads to the model of sets equipped with extensional relations as [[transitive set]]s.

\hypertarget{references}{}\subsection*{{References}}\label{references}

\begin{itemize}%
\item Peter Aczel; \href{http://standish.stanford.edu/pdf/00000056.pdf}{Non-Well-Founded Sets}, especially Chapter 4.

\end{itemize}
[[!redirects extensional relation]] [[!redirects extensional relations]]

[[!redirects extensional quotient]] [[!redirects extensional quotients]]

[[!redirects weak extensionality]] [[!redirects Finsler extensionality]] [[!redirects Scott extensionality]] [[!redirects strong extensionality]]



\end{document}