\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*{universes in SEAR}

\hypertarget{universes_in_sear}{}\section*{{Universes in SEAR}}\label{universes_in_sear}

\noindent\hyperlink{using_families}{Using families}\dotfill \pageref*{using_families} \linebreak
\noindent\hyperlink{using_mere_sets}{Using mere sets}\dotfill \pageref*{using_mere_sets} \linebreak


This page develops a theory of universes in the [[structural set theory]] called [[SEAR]], parallel to the theory of [[Grothendieck universes]] for [[ZF]] and the theory of a [[universe in a topos]]. See also [[categories in SEAR]].

[[David Roberts]]: Can we talk about Grothendieck universes or analogous size-related mechanisms? (this is a naive question, since there may be (no need for/obvious way to do) this in a structural set theory that I am unaware of.

[[Mike Shulman]]: Universes can be defined in any structural set theory in a fairly straightforward way, modulo the usual translation from ``set of sets'' to ``family of sets.'' There is some stuff from a more ETCS-like perspective at [[universe in a topos]]; I'm sure that this can be rephrased in SEAR (if you want to take a shot, feel free!).

[[David Roberts]]: I'd certainly like to, subject to real-world time constraints. It seems to me that something could be done to the axiom of collection if we had a axiom of universes (for every set there is a universe acting as a universal family for it, or similar).

[[Mike Shulman]]: I'm not sure that Collection can really be eliminated using universes, but maybe it can.

\hypertarget{using_families}{}\subsection*{{Using families}}\label{using_families}

[[David Roberts]]: Some sketchy thoughts - a universe will be a relation $U \looparrowright E$ satisfying axioms analogous to those at [[universe in a topos]]. There are few points that need translating into SEAR-language first so we can define smallness of a family of sets $I \looparrowright A$

\begin{itemize}%
\item Pullback - unless I am mistaken, the appropriate version is this: Given a function $I \to U$, the family $I \looparrowright E$ should be regarded as the 'pullback' family. This family should be isomorphic to the family $I \looparrowright A$. This leads us to wonder how to define two families to be isomorphic.


\item Dependent product - this is tricker and I'm not going to do that right now.



\end{itemize}
Fix a [[family of sets]] $U \looparrowright E$.

\begin{defn}
\label{}\hypertarget{}{}
A family $a:I \looparrowright A$ is called \emph{$U$-small} if there is a function $f:I \to U$ such that for the composite relation $I \looparrowright E$ \ldots{}

\end{defn}
A set $A$ is called $U$-small if the relation $\mathbf{1}\looparrowright A$, which holds of $*$ and $a$ for all elements $a$ of $A$, is a $U$-small family.

For ease of language, we define a composite of families to be the composite relation of the two relations defining the families.

\begin{defn}
\label{}\hypertarget{}{}
A family of sets $U \looparrowright E$ is called a \emph{universe} if the following axioms are satisfied:

\begin{itemize}%
\item The composite of two $U$-small families is $U$-small
\item The relation $f^o:B\looparrowright A$ opposite to an injective function $f:A \to B$ is a $U$-small family
\item $P\mathbf{1}$ is a $U$-small set
\item (Something about dependent products, once these are defined)

\end{itemize}
\end{defn}
There is an optional axiom, given the axiom of infinity from before:

\begin{itemize}%
\item The [[natural numbers object]] is a $U$-small set

\end{itemize}
Without this axiom we do not have that universes contain infinite sets.

Given a universe $U \looparrowright E$, we want to define a (meta-)category $Set_U$\ldots{}

\hypertarget{using_mere_sets}{}\subsection*{{Using mere sets}}\label{using_mere_sets}

[[Mike Shulman]]: The main idea of SEAR is that in a well-pointed topos, global elements suffice for everything. In particular, we can usually dispense with families of things and consider only single ones. So here's a formulation that I think is more in the spirit of SEAR.

Given a family $E:U\looparrowright X$, recall that for $u\in U$ we let $E_u$ be a tabulation of $\{x\in X | E(u,x) \}\subseteq X$. We say that a set $A$ is \textbf{$U$-small} (although really, it would be more appropriate to say ``$E$-small'') if there exists a $u\in U$ with $A\cong E_u$. Now we say that $U$ (equipped with $E$) is a \textbf{universe} if it satisfies:

\begin{itemize}%
\item There exists an inhabited $U$-small set.
\item The tabulation of any relation between two $U$-small sets is $U$-small.
\item If $A$ is $U$-small, then so is $P A$.
\item (Replacement) If $f:A\to B$ is a function such that $B$ is $U$-small and for each $b\in B$, the set $f^{-1}(b)$ is $U$-small, then $A$ is $U$-small.
\item (Collection) If $p:B\twoheadrightarrow A$ is a surjective function where $A$ is $U$-small, then there exists a $U$-small set $C$, a surjection $q:C\twoheadrightarrow A$ and a function $f:C\to B$ such that $q = p\circ f$.

\end{itemize}
The optional axiom is the same:

\begin{itemize}%
\item There exists an infinite $U$-small set (in the sense of Axiom 4).

\end{itemize}
The first two properties of a universe clearly imply that the $U$-small sets satisfy Axioms 0--2 of SEAR all by themselves. In particular, $\emptyset$ and $1$ are $U$-small, any subset of a $U$-small set is $U$-small, and if $A$ and $B$ are small then so is $A\times B$. Thus from the additional assumption of the smallness of powersets, we can conclude that if $A$ and $B$ are small, so is the set $B^A$ of functions from $A$ to $B$. It also follows that coproducts and quotient sets preserve smallness. (For a notion of ``predicative universe'' we would replace the smallness of powersets with the smallness of function sets, and we might have to separately assume smallness of coproducts and quotients, I'm not sure.)

In order to show that the $U$-small sets model SEAR all by themselves, it remains to show:

\begin{theorem}
\label{univ-coll}\hypertarget{univ-coll}{}
The $U$-small sets for a universe $U$ satisfy the Collection axiom of SEAR.

\end{theorem}
\begin{proof}
Let $A$ be a $U$-small set and $P$ a property as in the Collection axiom. Let $P'$ be a property such that $P'(a,X)$ holds iff $P(a,X)$ holds \emph{and} $X$ is $U$-small. By the Collection axiom for all sets applied to $P'$, there exists a set $B$, a function $p:B\to A$, and a $B$-indexed family of sets $M:B\looparrowright Y$ satisfying the desired properties: (1) for any $b\in B$, we have $P(p(b),M_b)$ \emph{and} $M_b$ is $U$-small, and (2) for any $a\in A$, if there exists a $U$-small set $X$ with $P(a,X)$, then $a\in im(p)$. Our goal is to replace $B$ and $Y$ by $U$-small sets $B'$ and $Y'$ with a relation $M':B'\looparrowright Y'$ maintaining the truth of these statements.

Now the induced function $\overline{p}:B\to im(p)$ is surjective, and since $im(p)$ is a subset of $A$ it is $U$-small. Thus, by the ``Collection'' property of a universe, there exists a $U$-small set $C$, a surjection $q:C\twoheadrightarrow im(p)$ and a function $f:C\to B$ such that $q = \overline{p} \circ f$. We take $B'=C$ and the composite $C \to im(p)\to A$ as the function $p'$; we claim that the composite relation $M\circ f$ still satisfies (1) and (2) above. (We have not replaced $Y$ yet, so this is still an intermediate step.) Property (1) follows since $p'(c) = p(f(c))$ and $(M\circ f)_c \cong M_{f(c)}$, while property (2) follows since $im(p) = im(p')$ by construction.

Now consider a tabulation $B' \overset{r}{\leftarrow} Z \overset{s}{\to} Y$ of $M\circ f$. Note that for any $b\in B'$ we have $r^{-1}(b) \cong (M\circ f)_b$, and therefore in particular $r^{-1}(b)$ is $U$-small by (1). Since $B'$ is also $U$-small, the ``Replacement'' property of a universe implies that $Z$ is also $U$-small. But the family $r^o:B'\looparrowright Z$ is equivalent to $M\circ f$, in the sense that $(r^o)_b \cong (M\circ f)_b$ for all $b\in B'$, so it also satisfies (1) and (2); thus we can take $Y'=Z$ and $M'=r^o$.

\end{proof}
Note that both the ``Replacement'' and ``Collection'' properties of a universe are required to show the SEAR Collection axiom for $U$-small sets. The naming of these two properties appears to be traditional, however. See in particular the book \emph{Algebraic Set Theory} by Joyal and Moerdijk.

What about families and dependent products? We define a function, considered as a family of sets, to be \textbf{$U$-small} if each of its fibers is. Note that then we can state the Replacement property as ``the composite of $U$-small functions is $U$-small.'' Now for functions $g:C\to B$ and $f:B\to A$, the fiber of the dependent product $\Pi_f g$ over $a\in A$ is the subset of the function set $\Big((f g)^{-1}(a)\Big)^{f^{-1}(a)}$ consisting of functions $s: f^{-1}(a) \to (f g)^{-1}(a)$ such that $g\circ s = \id$. Thus, if $f$ and $g$ are $U$-small, so is $f g$ (by the ``Replacement'' property), and thus so is this fiber. Hence $U$-small functions are closed under dependent products.

Also of interest is the following, which should be compared to the ``descent'' axiom in Joyal-Moerdijk.

\begin{theorem}
\label{univ-descent}\hypertarget{univ-descent}{}
The following are equivalent for a function $f:B\to A$. 1. $f$ is $U$-small. 2. There exist a surjection $p:C\to A$ and a function $g:C\to U$ and two pullback squares

\begin{displaymath}
\itexarray{B &\overset{q}{\leftarrow} & P & \overset{k}{\to} & {|E|}\\
   ^f\downarrow && \downarrow^j && \downarrow\\
   A &\underset{p}{\twoheadleftarrow} & C & \underset{g}{\to} & U}
\end{displaymath}
\begin{enumerate}%
\item (If the axiom of choice holds) There exists a function $g:A\to U$ and a pullback square\begin{displaymath}
\itexarray{B & \overset{}{\to} & {|E|}\\
^f\downarrow && \downarrow\\
A & \underset{g}{\to} & U}
\end{displaymath}


\end{enumerate}
\end{theorem}
\begin{proof}
Clearly the third condition implies the second. The second implies the first, since pullbacks have isomorphic fibers. And in the presence of AC, the second implies the third, since the surjection $p$ has a section. Thus the difficulty is in showing that the first implies the second.

Suppose that $f:B\to A$ is $U$-small. This means that for any $a\in A$, there exists a $u\in U$ and a bijection $f^{-1}(a)\cong E_u$. Let $C$ be the subset of $A\times U\times P(B\times |E|)$ consisting of those triples $(a,u,h)$ such that $h$ is a bijection $f^{-1}(a) \overset{\cong}{\to} E_{u}$, and let $p:C\to A$ and $g:C\to U$ be the projections. Since $f$ is $U$-small, $p$ is surjective. Define $P$ to be a pullback of $f$ along $p$, with projections $q:P\to B$ and $j:P\to C$, and define $k:P\to {|E|}$ by (informally speaking) $k(x) = h(q(x))$ where $j(x) = (a,u,h)$. Since each $h$ is a bijection, $k$ makes $P$ a pullback of ${|E|}$.

\end{proof}
[[!redirects universe in SEAR]] [[!redirects universes in SEAR]] [[!redirects Grothendieck universe in SEAR]] [[!redirects Grothendieck universes in SEAR]]



\end{document}