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

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

\hypertarget{topos_theory}{}\paragraph*{{Topos Theory}}\label{topos_theory}

[[!include topos theory - contents]]

\hypertarget{posites}{}\section*{{Posites}}\label{posites}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{definitions}{Definitions}\dotfill \pageref*{definitions} \linebreak
\noindent\hyperlink{ideals_and_sheaves}{Ideals and sheaves}\dotfill \pageref*{ideals_and_sheaves} \linebreak
\noindent\hyperlink{interpretations}{Interpretations}\dotfill \pageref*{interpretations} \linebreak
\noindent\hyperlink{examples}{Examples}\dotfill \pageref*{examples} \linebreak
\noindent\hyperlink{using_ideals}{Using ideals}\dotfill \pageref*{using_ideals} \linebreak
\noindent\hyperlink{using_sheaves}{Using sheaves}\dotfill \pageref*{using_sheaves} \linebreak
\noindent\hyperlink{use_in_predicative_mathematics}{Use in predicative mathematics}\dotfill \pageref*{use_in_predicative_mathematics} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


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

The notion of \emph{posite} (or \emph{$(0,1)$-site}, less properly \emph{$0$-site}) is a [[decategorification]] of the notion of \emph{[[site]]} (which may also be called an $1$-site or $(1,1)$-site). For [[categorifications]] thereof, see [[(∞,1)-site]] and [[2-site]].

Just as a site is a [[category]] with a [[coverage]], whose ([[set]]-valued) [[sheaves]] form a [[Grothendieck topos]], so a posite is a [[poset]] with a coverage, whose $(0,1)$-sheaves ([[truth value]]-valued sheaves) form a [[locale]]. On the other hand, we can also consider a posite as a site in its own right, in which case the $1$-sheaves on it form a [[localic topos]].

As locale theory serves as an approach to [[topology]] in which locales take the role traditionally held by [[topological spaces]], so posites take the role traditionally held by [[topological bases]].

A [[formal topology]] may be generated by a posite equipped with a [[positivity predicate]].

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

\begin{udefn}
A \textbf{posite} is a [[site]] whose underlying category is [[thin category|thin]].

\end{udefn}
In other words, a posite is a [[poset]] (or more generally a [[preordered set]]) equipped with a [[Grothendieck topology]] or a [[coverage]]. (The name is a portmanteau/blend of `poset' and `site'.)

The definition of coverage may be simplified a little in this case.

\begin{udefn}
Let $S$ be a poset (or proset). A \textbf{coverage} on $S$ is a [[binary relation]] $\lhd$ between $S$ and its [[power set]] that satisfies these conditions:

\begin{itemize}%
\item If $u \lhd V$ and $v \in V$, then $v \leq u$;
\item If $u \lhd V$ and $u' \leq u$, then $u' \lhd V'$ for some $V'$ such that, for every $v' \in V'$, there is a $v \in V$ such that $v' \leq v$.

\end{itemize}
Then a \textbf{posite} is precisely a poset (or proset) equipped with a coverage.

\end{udefn}
If $S$ is a [[meet-semilattice]], then there is another alternative defintion. (Actually, it is not necessary that the [[poset]] $S$ have \emph{all} finitary [[meets]] but only \emph{[[bounded meet|bounded]]} ones. That is, if $v, w \leq u$ for some fixed $u$, then $v \wedge w$ must exist, but not otherwise. Such a poset $S$ is a semilattice if and only if it has a [[top element]]. Compare the notion of [[locally cartesian category]].)

\begin{udefn}
Let $S$ be a poset (or proset) with all bounded binary meets. A \textbf{cartesian coverage} on $S$ is a [[binary relation]] $\lhd$ between $S$ and its [[power set]] that satisfies these conditions:

\begin{itemize}%
\item If $u \lhd V$ and $v \in V$, then $v \leq u$;
\item If $u \lhd V$ and $u' \leq u$, then $u' \lhd \{ v \wedge u' \;|\; v \in V \}$.

\end{itemize}
Then a \textbf{locally cartesian posite} is such a poset (or proset) equipped with such a coverage.

\end{udefn}
It is a theorem that every posite whose underlying poset has all bounded binary meets is equivalent (in the sense that there is an isomorphism of sites as defined below) to a locally cartesian posite.

In any case, given an element $u$ of $S$ and a [[subset]] $V$ of $S$, if

\begin{displaymath}
u \lhd V ,
\end{displaymath}
then we say that $V$ is a \textbf{basic [[cover]]} of $u$.

\begin{udefn}
Given two posites $S$ and $T$, a \textbf{morphism of posites} from $S$ to $T$ is a [[function]] $f\colon S \to T$ such that:

\begin{itemize}%
\item If $u \leq v$ in $S$, then $f(u) \leq f(v)$ in $T$;
\item Given any $u$ in $T$, for some $v$ in $S$, we have $u \leq f(v)$;
\item If $w \leq f(u), f(v)$ in $T$, then for some $x \leq u, v$ in $S$, we have $w \leq f(x)$; and
\item If $u \lhd V$, then $f(u) \lhd \{ f(v) \;|\; v \in V \}$.

\end{itemize}
\end{udefn}
Clauses (1--3) simply state that $f$ is a [[flat functor]]; when $S$ and $T$ are semilattices, we can replace this with the requirement that $f$ preserves meets (including the top element). Clause (4) requires $f$ to respect covers.

\hypertarget{ideals_and_sheaves}{}\subsection*{{Ideals and sheaves}}\label{ideals_and_sheaves}

One often looks at [[sheaves]] on [[sites]]. On posites, one can either look at sheaves or at ideals.

\begin{udefn}
Given a posite $S$, an \textbf{ideal} on $S$ (also called a \textbf{$(0,1)$-sheaf}; compare $(\infty,1)$-[[(infinity,1)-sheaf|sheaf]]) is a [[subset]] $I$ of $S$ satisfying these conditions:

\begin{enumerate}%
\item If $u \leq v$ and $v \in I$, then $u \in I$; and
\item If $u \lhd V$ and $V \subseteq I$, then $u \in I$.

\end{enumerate}
\end{udefn}
In other words, it is a [[sheaf]] valued in [[truth values]] (rather than in [[sets]] as is the default).

A subset $I$ that satisfies condition (1) alone states that $I$ is a \textbf{[[lower subset]]} (a $(0,1)$-[[presheaf]]).

The ideals on a posite form a [[frame]] $Id(S)$ (or $Sh_{0,1}(S)$) under inclusion, which may alternately be interpreted as a [[locale]].

Every element of $S$ may be interpreted as an ideal on $S$; given two elements $u,v$ of $S$, $u$ belongs to the \textbf{ideal [[represented functor|represented]]} by $v$ if and only if $u \leq v$; that is, $v$ represents its [[down set]].

The frame of ideals is given by a [[universal property]]. If $L$ is a frame, we make $L$ into a posite using its canonical coverage (see the examples below). Then the operation from elements of $S$ to ideals on $S$ is a morphism of posites; furthermore, given any morphism of posites from $S$ to a frame $L$ (with its canonical coverage), there exists a unique frame [[homomorphism]] from $Id(S)$ to $L$ that makes the obvious triangle commute.

If instead we treat a posite as a special kind of site and look at its $1$-sheaves, we have this result:

\begin{uprop}
The [[topos of sheaves]] on any posite $P$ is a [[localic topos]].

\end{uprop}
\begin{proof}
This is obvious if we use the definition of ``localic topos'' which says that it is generated by [[subterminal objects]], since the (sheafifications of) representable functors always generate a topos of sheaves, and for a posite these are subterminal.

\end{proof}
The relevant locale is precisely the locale of ideals.

\hypertarget{interpretations}{}\subsection*{{Interpretations}}\label{interpretations}

Given a posite $S$, we may think of the elements of $S$ as \textbf{basic opens} of a space which is generated from $S$ using its coverage, to produce a [[locale]]. Thus a posite is precisely a \textbf{base} for a locale. See the example coming from a topological space below to see how this can work precisely for a [[topological locale]].

A coverage can be seen as a [[sequent]] calculus; the interpretation of

\begin{displaymath}
u \lhd V
\end{displaymath}
in topology is analogous to the interpretation of

\begin{displaymath}
p \lhd Q
\end{displaymath}
in [[logic]]. Note that we have a single proposition on the left but a set of propositions (interpreted [[disjunction|disjunctively]]) on the right, the reverse of an [[intuitionistic logic|intuitionistic]] sequent.

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

\hypertarget{using_ideals}{}\subsubsection*{{Using ideals}}\label{using_ideals}

Any poset (or proset) $S$ has a \textbf{[[canonical coverage]]}, in which

\begin{itemize}%
\item $u \lhd V$ if and only if, for any $u' \leq u$, $u'$ is a [[join]] of some $V'$ such that, for every $v' \in V'$, there is a $v \in V$ such that $v' \leq v$.

\end{itemize}
If $S$ is a [[frame]], then we can simplify this condition:

\begin{itemize}%
\item $u \lhd V$ if and only if $u$ is a join of $V$;

\end{itemize}
and then the canonical coverage is cartesian. In this case, $Id(S)$ is [[natural isomorphism|naturally isomorphic]] to $S$ itself. (Analogously, if $E$ is a [[Grothendieck topos]] with its canonical coverage, then $Sh(E)$, the [[topos of sheaves]] on $E$, is naturally [[equivalence of categories|equivalent]] to $E$.)

Let $X$ be a [[topological space]], and let $S$ be a [[topological base]] of $X$. Then $S$ is a semilattice under [[intersection]]; we make $S$ into a posite by defining

\begin{itemize}%
\item $u \lhd V$ if and only if $u$ is the [[union]] of $V$ in $X$ (which is not necessarily the same as a join in $S$).

\end{itemize}
The frame generated by this posite is [[natural isomorphism|naturally isomorphic]] to the [[frame of opens]] of $X$. If $X$ is a [[sober space]], then this frame, interpreted as a [[locale]], may be identified with $X$.

The [[locale of real numbers]] is generated from the locally cartesian poset $S \coloneqq \mathbb{Q}^op \times \mathbb{Q}$, where $\mathbb{Q}$ is the usual poset of [[rational numbers]], equipped with the cartesian coverage given by

\begin{itemize}%
\item $(x,y) \lhd \empty$ whenever $x \geq y$;
\item $(w,z) \lhd \{(w,x),(y,z)\}$ whenever $w \leq y \lt x \leq z$; and
\item $(w,z) \lhd \{ (x,y) \;|\; w \lt x \lt y \lt z \}$.

\end{itemize}
Often you will see $\pm\infty$ added to $\mathbb{Q}$ in a description of this locale, which adds a [[top element]] to $S$ and so makes it into a semilattice, but that makes no difference to the generated locale in this case.

\hypertarget{using_sheaves}{}\subsubsection*{{Using sheaves}}\label{using_sheaves}

The [[double negation topology]] used in the sheaf-theoretic approach to [[forcing]] is a posite. More generally, [[classical mathematics|Classical]] [[set theory|set-theoretic]] [[forcing]] is done exclusively on posites. One ``reason'' for this (in the sense of a reason why set-theorists have not been forced to look beyond such models) is explained in \hyperlink{Freyd}{the paper by Freyd} below.

The [[semilattice of commutative subalgebras]] of a $C^*$-[[C-star algebra|algebra]] $A$ is a posite (with trivial topology) internal to whose sheaf topos we have a [[constructive Gelfand duality theorem]] for $A$, even if $A$ was externally non-commutative.

The [[classifying topos]] of any [[propositional logic|propositional]] [[geometric theory]] is localic, and can be presented as sheaves on a posite of [[propositions]].

\hypertarget{use_in_predicative_mathematics}{}\subsection*{{Use in predicative mathematics}}\label{use_in_predicative_mathematics}

We call a frame (or locale) $L$ \textbf{accessible} if it is [[isomorphism|isomorphic]] to $Id(S)$ for some [[small category|small]] posite $S$. (Compare the concept of [[accessible category]], in the case of a [[cocomplete category|cocomplete]] [[pretopos]].)

In [[classical mathematics]], an accessible frame must be small, but this fails in [[predicative mathematics]]. (Conversely, any small frame is trivially accessible; take $S$ to be $L$ with its canonical coverage.) Since many predicativists have philosophical objections to working with large objects at all, they may prefer to work with small posites directly. Whatever the philosophy, we may use small posites in place of accessible locales, or at any rate use this to prove that the category of the latter is [[essentially moderate category|essentially moderate]].

[[formal topology|Formal topology]] is a programme for [[topology]] which is based on using small posites. However, formal topologists also require a positivity predicate on their posites; the intended interpretation is that $u$ is positive iff its corresponding [[open subspace]] is [[inhabited space|inhabited]]. This seems to be needed for a good theory of [[compact spaces]] (and related notions) in a predicative constructive framework.

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

\begin{itemize}%
\item Most of this article is based on \emph{[[Stone Spaces]]}, but with a different presentation.

\end{itemize}
On [[forcing]], see:

\begin{itemize}%
\item [[Peter Freyd]], \emph{All topoi are localic or why permutation models prevail}, Journal of Pure and Applied Algebra 46 (1987) pp 49--58.

\end{itemize}
\begin{itemize}%
\item \href{http://mathoverflow.net/questions/13480/set-theoretic-forcing-over-sites}{This MO question} and its answer.

\end{itemize}
[[!redirects posite]] [[!redirects posites]] [[!redirects 0-site]] [[!redirects 0-sites]] [[!redirects (0,1)-site]] [[!redirects (0,1)-sites]]

[[!redirects 0-coverage]] [[!redirects 0-coverages]] [[!redirects (0,1)-coverage]] [[!redirects (0,1)-coverages]]

[[!redirects morphism of posites]] [[!redirects morphisms of posites]] [[!redirects morphism of 0-sites]] [[!redirects morphisms of 0-sites]] [[!redirects morphism of (0,1)-sites]] [[!redirects morphisms of (0,1)-sites]] [[!redirects posite morphism]] [[!redirects posite morphisms]] [[!redirects 0-site morphism]] [[!redirects 0-site morphisms]] [[!redirects (0,1)-site morphism]] [[!redirects (0,1)-site morphisms]]

[[!redirects 0-sheaf]] [[!redirects 0-sheaves]] [[!redirects (0,1)-sheaf]] [[!redirects (0,1)-sheaves]] [[!redirects ideal in a posite]] [[!redirects ideals in a posite]] [[!redirects ideal in a 0-site]] [[!redirects ideals in a 0-site]] [[!redirects ideal in a (0,1)-site]] [[!redirects ideals in a (0,1)-site]]

[[!redirects frame of ideals]] [[!redirects frames of ideals]] [[!redirects frame of 0-sheaves]] [[!redirects frames of 0-sheaves]] [[!redirects frame of (0,1)-sheaves]] [[!redirects frames of (0,1)-sheaves]] [[!redirects frame of sheaves]] [[!redirects frames of sheaves]] [[!redirects locale of ideals]] [[!redirects locales of ideals]] [[!redirects locale of 0-sheaves]] [[!redirects locales of 0-sheaves]] [[!redirects locale of (0,1)-sheaves]] [[!redirects locales of (0,1)-sheaves]] [[!redirects locale of sheaves]] [[!redirects locales of sheaves]]

[[!redirects localic base]] [[!redirects localic bases]] [[!redirects base of a locale]] [[!redirects bases of a locale]] [[!redirects bases of locales]]

[[!redirects accessible frame]] [[!redirects accessible frames]] [[!redirects accessible locale]] [[!redirects accessible locales]]



\end{document}