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

\hypertarget{quantifiers}{}\section*{{Quantifiers}}\label{quantifiers}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{definitions}{Definitions}\dotfill \pageref*{definitions} \linebreak
\noindent\hyperlink{quantification_in_firstorder_logic}{Quantification in first-order logic}\dotfill \pageref*{quantification_in_firstorder_logic} \linebreak
\noindent\hyperlink{quantification_in_firstorder_logic_with_equality}{Quantification in first-order logic with equality}\dotfill \pageref*{quantification_in_firstorder_logic_with_equality} \linebreak
\noindent\hyperlink{lawvere_quantifiers_quantification_as_adjunction}{Lawvere quantifiers: Quantification as adjunction}\dotfill \pageref*{lawvere_quantifiers_quantification_as_adjunction} \linebreak
\noindent\hyperlink{guarded_quantification_quantifying_over_subtypes}{Guarded quantification: quantifying over subtypes}\dotfill \pageref*{guarded_quantification_quantifying_over_subtypes} \linebreak
\noindent\hyperlink{bounded_quantification_size_issues_and_predicativity}{Bounded quantification: size issues and predicativity}\dotfill \pageref*{bounded_quantification_size_issues_and_predicativity} \linebreak
\noindent\hyperlink{internalised_quantifiers}{Internalised quantifiers}\dotfill \pageref*{internalised_quantifiers} \linebreak
\noindent\hyperlink{categorified_quantifiers}{Categorified quantifiers}\dotfill \pageref*{categorified_quantifiers} \linebreak
\noindent\hyperlink{examples}{Examples}\dotfill \pageref*{examples} \linebreak
\noindent\hyperlink{RelatedConcepts}{Related concepts}\dotfill \pageref*{RelatedConcepts} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


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

A quantifier is an operation in [[logic]] that moves a statement from one [[context]] to a related context.

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

\hypertarget{quantification_in_firstorder_logic}{}\subsubsection*{{Quantification in first-order logic}}\label{quantification_in_firstorder_logic}

In [[first-order logic]], we have two basic quantifiers, each of which moves a [[predicate]] on one type to a [[proposition]] (a predicate on no types), or more generally moves a predicate on $n + 1$ types to a predicate on $n$ types.

Given a predicate $P$ on a type $T$, the \textbf{[[universal quantification]]} of $P$, denoted $\forall\, x\colon T, P(x)$ (and with many variations in punctuation), is intended to be [[true]] if and only if $P(a)$ is true for every possible element $a$ of $T$. Similarly, the \textbf{[[existential quantification]]} of $P$ (also called its \textbf{particular quantification}), denoted $\exists\, x\colon T, P(x)$, is intended to be true if and only if $P(a)$ is true for at least one element $a$ of $T$. However, it is quite possible that $P(a)$ may be provable (in a given context $\Gamma$) for every \emph{term} $a$ of type $T$ that \emph{can actually be constructed} (in $\Gamma$), yet $\forall\, x\colon T, P(x)$ cannot be proved; conversely, it is quite possible that $\exists\, x\colon T, P(x)$ can be proved (in a given context) but $P(a)$ cannot be proved for any term $a$ of type $T$ that can actually be constructed.

Therefore, we must define the quantifiers more carefully; one way to do this is as follows:

\begin{itemize}%
\item $Q \vdash_{\Gamma}\forall\, x\colon T, P(x)$ if and only if $Q \vdash_{\Gamma, x\colon T} P(x)$;
\item $\exists\, x\colon T, P(x) \vdash_{\Gamma} Q$ if and only if $P(x) \vdash_{\Gamma, x\colon T} Q$.

\end{itemize}
Here, $\Gamma$ is an arbitrary context, and $\Gamma, x\colon T$ is that context supplemented by a free variable $x$ of type $T$. Note that $Q$ is (a priori) a statement in the context $\Gamma$ but also needs to make sense in the context $\Gamma, x\colon T$; therefore, our logic needs an appropriate [[weakening rule]] for this to make sense. This definition also presumes that a statement (in any given context) can be identified precisely by placing it within the [[poset]] of statements (in that context) under entailment ($\vdash$), which is true for ordinary first-order logic.

From this definition, one can derive rules for the quantifiers in [[sequent calculus]] and [[natural deduction]].

\hypertarget{quantification_in_firstorder_logic_with_equality}{}\subsubsection*{{Quantification in first-order logic with equality}}\label{quantification_in_firstorder_logic_with_equality}

If all of our types have an [[equality predicate]], then we can construct some fancier quantifiers.

Given a predicate $P$ on a type $T$ with equality, the \textbf{uniqueness quantification} of $P$, denoted $\exists!\, x\colon T, P(x)$, may defined in terms of the universal and existential quantifiers as

\begin{displaymath}
\exists!\, x\colon T, P(x) \;\equiv\; \exists\, x\colon T, P(x) \wedge \forall\, y\colon T, P(y) \Rightarrow (x = y) .
\end{displaymath}
The intended interpretation is that $\exists!\, x\colon T, P(x)$ is true iff $P(a)$ is true for \emph{exactly} one element $a$ of $T$.

We can similarly write down quantifiers to say that $P$ holds for exactly two elements, at most three elements, at least four elements, etc. (These all require [[negation]] and therefore there are some slight variations possible when using [[intuitionistic logic]].)

With these examples, one can see quite readily that quantification is about saying how often a statement is true, that is \emph{quantifying} it.

\hypertarget{lawvere_quantifiers_quantification_as_adjunction}{}\subsubsection*{{Lawvere quantifiers: Quantification as adjunction}}\label{lawvere_quantifiers_quantification_as_adjunction}

Given two contexts $\Gamma$ and $\Delta$ and an interpretation $f\colon \Gamma \to \Delta$, we obtain an operation $f^*\colon Prop_\Delta \to Prop_\Gamma$ from the propositions in $\Delta$ to the propositions in $\Gamma$. If this operation has a [[right adjoint]], then this right adjoint is the \textbf{[[universal quantifier]]} along $f$; if it has a [[left adjoint]], then this is the \textbf{[[existential quantifier]]} along $f$. The ordinary quantifiers in first-order logic are simply special cases of this where $f$ is given by weakening.

To bring this down to earth, let $S$ and $T$ be [[sets]] and let $f\colon S \to T$ be a [[function]]. We will think of each set as defining a context with one free variable for an element of that set; then the propositions in one of those contexts correspond to the [[subsets]] of the corresponding set. In this way, we are looking at $f^*\colon \mathcal{P}T \to \mathcal{P}S$, the [[preimage]] map between [[power sets]] (often denoted $f^{-1}$). Then the adjoints $\forall_f$ and $\exists_f$ are maps from $\mathcal{P}S \to \mathcal{P}T$ as follows:

\begin{itemize}%
\item $\forall_f\, A \coloneqq \{ y\colon T \;|\; \forall\, x\colon S,\; f(x) = y \;\Rightarrow\; x \in A \}$;


\item $\exists_f\, A \coloneqq \{ y\colon T \;|\; \exists\, x\colon S,\; f(x) = y \;\wedge\; x \in A \}$.



\end{itemize}
Note that $\exists_f A$ is simply the [[image]] of $f$ restricted to $A$. Accordingly, one often denotes $\exists_f$ as $f_*$ (if not simply $f$). When using this notation, one can also denote $\forall_f$ as $f_!$.

When $f$ is the unique function from a set $X$ to the terminal set, $\mathcal{P}1$ is the two-element set and an object in $\mathcal{P}X$ is a predicate on $X$. The adjoints then map a predicate $Q$ to a truth value:

\begin{itemize}%
\item $\exists x \in X$ such that $Q(x)$;


\item $\forall x \in X, Q(x).$



\end{itemize}
\hypertarget{guarded_quantification_quantifying_over_subtypes}{}\subsubsection*{{Guarded quantification: quantifying over subtypes}}\label{guarded_quantification_quantifying_over_subtypes}

Recall that, given a type $T$ and a predicate $Q$ on $T$, the \textbf{[[subtype]]} of $T$ defined by $Q$ is a type $S$ whose elements $x$ are thought of as elements of $T$ such that $Q(x)$ holds. Many type theories do not include subtypes. However, we can mimic quantification over subtypes by using so-called `guarded' quantifiers.

Specifically, given a type $T$, a predicate $Q$ on $T$, and a predicate $P$ on $T$, the \textbf{guarded quantifications} of $P$ relative to $Q$ are these propositions:

\begin{itemize}%
\item $\forall x\colon T, Q(x) \Rightarrow P(x)$,
\item $\exists x\colon T, Q(x) \wedge P(x)$.

\end{itemize}
We have already had an example of these on this page, in the discussion of the Lawvere quantifiers along a function.

When the notation for $Q$ makes the type $T$ obvious, and especially when the variable appears only at beginning in this notation, it is quite common to suppress mention of $T$ and write $\forall Q(x), P(x)$ and $\exists Q(x), P(x)$. This is particularly common in untyped theories where $T$ would be suppressed anyway; for example, this is almost always how one writes guarded quantifiers in [[material set theory]].

\hypertarget{bounded_quantification_size_issues_and_predicativity}{}\subsubsection*{{Bounded quantification: size issues and predicativity}}\label{bounded_quantification_size_issues_and_predicativity}

When [[type theory]] is used as a [[foundation of mathematics]], we have a freely generated [[universe]] of types (see also at \emph{[[type of types]]}) and can also consider quantification over these. Similarly, when [[set theory]] is used as a foundation, we have a type of all sets and can consider quantification over this type. Such quantification is called \textbf{unbounded} and often forbidden in the [[axiom of separation]] (if it can be stated in the language at all), especially in [[predicative mathematics]] but also in some impredicative foundations, such as [[ETCS]]. Even if we allow unbounded quantification, if we wish to refer to large objects using the language of [[proper classes]], this introduces the possibility of quantification over all classes, and this is forbidden even in [[ZFC]] and [[SEAR]] (although it is allowed in Morse--Kelley class theory).

In contrast, quantification over variables from \emph{small} types (for a suitable notion of smallness) is called \textbf{bounded quantification}.

In the usual formulations of [[material set theory]], there is only one type (the type of sets), which is not small. However, we can consider quantification over small subtypes using the trick of guarded quantification (above). So the axiom of separation in so-called `bounded' variations of ZFC allows only statements in which all quantifiers are guarded by a set.

In classical mathematics, at least, formulas with unbounded quantifiers can be classified into the [[Lévy hierarchy]], whose bottom level $\Delta_0$ consists of the formulas with only bounded quantifiers.

\hypertarget{internalised_quantifiers}{}\subsubsection*{{Internalised quantifiers}}\label{internalised_quantifiers}

\ldots{} [[Heyting category]] \ldots{}

\hypertarget{categorified_quantifiers}{}\subsubsection*{{Categorified quantifiers}}\label{categorified_quantifiers}

\ldots{} [[dependent product]] \ldots{} [[dependent sum]] \ldots{}

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

\begin{itemize}%
\item [[existential quantifier]], [[dependent sum]]


\item [[universal quantifier]], [[dependent product]]



\end{itemize}
\hypertarget{RelatedConcepts}{}\subsection*{{Related concepts}}\label{RelatedConcepts}

\begin{itemize}%
\item [[de dicto and de re]]


\item [[Lévy hierarchy]]


\item [[elimination of quantifiers]]


\item [[generalized quantifier]]



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

The identification of universal/existential quantification with [[adjoints]] of [[substitution]]/[[context extension]] ([[dependent product]]/[[dependent sum]]) originates around

\begin{itemize}%
\item [[Bill Lawvere]], \emph{Adjointness in Foundations}, (\href{http://www.emis.de/journals/TAC/reprints/articles/16/tr16abs.html}{TAC}), Dialectica 23 (1969), 281-296


\item [[Bill Lawvere]], \emph{Quantifiers and sheaves}, Actes, Congr\`e{}s intern, math., 1970. Tome 1, p. 329 \`a{} 334 (\href{https://pdfs.semanticscholar.org/6630/846a00261a071b71e264e0f532e29cd9152f.pdf}{pdf})



\end{itemize}
[[!redirects quantifier]] [[!redirects quantifiers]] [[!redirects quantification]] [[!redirects quantifications]]

[[!redirects uniqueness quantifier]] [[!redirects uniqueness quantifiers]] [[!redirects uniqueness quantification]] [[!redirects uniqueness quantifications]] [[!redirects unicity quantifier]] [[!redirects unicity quantifiers]] [[!redirects unicity quantification]] [[!redirects unicity quantifications]]

[[!redirects Lawvere quantifier]] [[!redirects Lawvere quantifiers]] [[!redirects Lawvere quantification]] [[!redirects Lawvere quantifications]]

[[!redirects guarded quantifier]] [[!redirects guarded quantifiers]] [[!redirects guarded quantification]] [[!redirects guarded quantifications]]

[[!redirects bounded quantifier]] [[!redirects bounded quantifiers]] [[!redirects bounded quantification]] [[!redirects bounded quantifications]] [[!redirects quantifier]]



\end{document}