\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*{geometry of physics - cohesive toposes}

\hypertarget{GrosToposes}{}\subsection*{{Gros toposes}}\label{GrosToposes}

We have seen roughly two different kinds of [[sheaf toposes]]:

\begin{itemize}%
\item [[categories of sheaves on a topological space|categories of sheaves on a given space]] $X$ (Example \ref{SheafOnATopologicalSpace}), which, by [[localic reflection]] (Prop. \ref{LocalicReflection}), really are just a reflection of the space $X$ in the [[category]] of [[toposes]],

these are called \emph{[[petit toposes]]};


\item [[categories of sheaves]] whose [[objects]] are [[generalized spaces]] (Example \ref{SmoothSetAnnounced})

these are called \emph{[[gros toposes]]}.



\end{itemize}
\begin{remark}
\label{CohesiveGeneralizedSpacesAsFoundations}\hypertarget{CohesiveGeneralizedSpacesAsFoundations}{}
\textbf{([[cohesion|cohesive]] [[generalized spaces]] as [[foundations|foundations]] of [[geometry]])}

If we aim to lay [[foundations]] for [[geometry]], then we are interested in isolating those kinds of [[generalized spaces]] which have foundational \emph{a priori} meaning, independent of an otherwise pre-configured notion of space. Hence we would like to first characterize suitable [[gros toposes]], extract concepts of [[space]] from these, and only then, possibly, consider the [[localic reflection|petit topos-reflections]] of these (Prop. \ref{LocalicReflection} below).

The [[gros toposes]] of such foundational [[generalized spaces]] ought to have an \emph{[[internal logic]]} that knows about \emph{[[modalities]] of [[geometry]]} such as \emph{[[discrete object|discreteness]]} or \emph{[[concrete object|concreteness]]}. Via the formalization of [[modalities]] in Def. \ref{ModalOperator} this leads to the definiton of [[cohesive toposes]] (Def. \ref{CohesiveTopos}, Prop. \ref{PiecesHavePoints} below, due to [[Some Thoughts on the Future of Category Theory|Lawvere 91]], \hyperlink{cohesive+topos#LawvereAxiomatic}{Lawvere 07}).

\end{remark}
\newline | $\phantom{A}$[[solid topos|solidity]]$\phantom{A}$ | Def. \ref{SuperDifferentialCohesion} | $\phantom{A}$principles of [[supergeometry]]$\phantom{A}$ | $\phantom{A}$[[geometry of physics -- supergeometry|SuperFormalSmoothSet]]$\phantom{A}$ |

$\,$

\hypertarget{Cohesive}{}\subsubsection*{{Cohesive toposes}}\label{Cohesive}

\begin{defn}
\label{CohesiveTopos}\hypertarget{CohesiveTopos}{}
\textbf{([[cohesive topos]])}

A [[sheaf topos]] $\mathbf{H}$ (Def. \ref{Sheaf}) is called a \emph{[[cohesive topos]]} if there is a [[adjoint quadruple|quadruple]] (Remark \ref{AdjointTriples}) of [[adjoint functors]] (Def. \ref{AdjointFunctorsInTermsOfNaturalBijectionOfHomSets}) to the [[category of sets]] (Example \ref{CategoryOfSets})

\begin{equation}
\Pi \dashv Disc \dashv \Gamma \dashv coDisc
  \;\;\colon\;\;
  \mathbf{H}
    \itexarray{
      \overset{\phantom{AAA} \Pi \phantom{AAA}}{\longrightarrow}
      \\
      \overset{\phantom{AA} Disc \phantom{AA} }{\hookleftarrow}
      \\
      \overset{\phantom{AAA} \Gamma \phantom{AAA} }{\longrightarrow}
      \\
      \overset{\phantom{AA} coDisc \phantom{AA} }{\hookleftarrow}
    }
  Set
\label{CohesopmAdjointQuadruple}\end{equation}
such that:

\begin{enumerate}%
\item $Disc$ and $coDisc$ are [[full and faithful functors]] (Def. \ref{FullyFaithfulFunctor})


\item $\Pi$ [[preserved limit|preserves]] [[finite products]].



\end{enumerate}
\end{defn}
\begin{example}
\label{PresheavesAdjointQuadrupleOnSiteWithTerminalObject}\hypertarget{PresheavesAdjointQuadrupleOnSiteWithTerminalObject}{}
\textbf{([[adjoint quadruple]] of [[presheaves]] over [[site]] with [[finite products]])}

Let $\mathcal{C}$ be a [[small category]] (Def. \ref{SmallCategory}) with [[finite products]] (hence with a [[terminal object]] $\ast \in \mathcal{C}$ and for any two [[objects]] $X,Y \in \mathcal{C}$ their [[Cartesian product]] $X \times Y \in \mathcal{C}$).

Then there is an [[adjoint quadruple]] (Remark \ref{AdjointTriples}) of [[functors]] between the [[category of presheaves]] over $\mathcal{C}$ (Example \ref{CategoryOfPresheaves}), and the [[category of sets]] (Example \ref{CategoryOfSets})

\begin{equation}
[\mathcal{C}^{op}, Set]
    \itexarray{
      \overset{\phantom{AAA} \Pi \phantom{AAA}}{\longrightarrow}
      \\
      \overset{\phantom{AA} Disc \phantom{AA} }{\hookleftarrow}
      \\
      \overset{\phantom{AAA} \Gamma \phantom{AAA} }{\longrightarrow}
      \\
      \overset{\phantom{AA} coDisc \phantom{AA} }{\hookleftarrow}
    }
  Set
\label{PreaheafAdjointQuadruple}\end{equation}
such that:

\begin{enumerate}%
\item the functor $\Gamma$ sends a [[presheaf]] $\mathbf{Y}$ to its set of [[global sections]], which here is its value on the [[terminal object]]:

\begin{equation}
\begin{aligned}
    \Gamma \mathbf{Y}
    & =
    \underset{\underset{\mathcal{C}}{\longleftarrow}}{\lim}
    \mathbf{Y}
    \\
    & \simeq
    \mathbf{Y}(\ast)
  \end{aligned}
\label{CohesiveGlobalSectionsGivenByPointEvaluation}\end{equation}

\item $Disc$ and $coDisc$ are [[full and faithful functors]] (Def. \ref{FullyFaithfulFunctor}).


\item $\Pi$ preserves [[finite products]]:

for $\mathbf{X}, \mathbf{Y} \in [\mathcal{C}^{op}, Set]$, we have a [[natural bijection]]

\begin{displaymath}
\Pi(\mathbf{X} \times \mathbf{Y})
  \;\simeq\;
  \Pi(\mathbf{X}) \times \Pi(\mathbf{Y})
  \,.
\end{displaymath}


\end{enumerate}
Hence the [[category of presheaves]] over a [[small category]] with [[finite products]], hence the [[category of sheaves]] for the [[trivial coverage]] (Example \ref{TrivialCoverage}) is a [[cohesive topos]] (Def. \ref{CohesiveTopos}).

\end{example}
\begin{proof}
The existence of the [[terminal object]] in $\mathcal{C}$ means equivalently (by Example \ref{InitialCategoryAndTerminalCategory}) that there is an [[adjoint pair]] of [[functors]] between $\mathcal{C}$ and the [[terminal category]] (Example \ref{InitialCategoryAndTerminalCategory}):

\begin{displaymath}
\ast
    \underoverset
    {\underset{}{\hookrightarrow}}
    {\overset{p}{\longleftarrow}}
    {\bot}
   \mathcal{C}
\end{displaymath}
whose [[right adjoint]] takes the unique object of the terminal category to that terminal object.

From this it follows, by Example \ref{KanExtensionOfAdjointPairIsAdjointQuadruple}, that [[Kan extension]] produces an [[adjoint quadruple]] (Remark \ref{AdjointTriples}) of functors between the [[category of presheaves]] $[\mathcal{C}^{op}, Set]$ and $[\ast, Set] \simeq Set$, as shown, where

\begin{enumerate}%
\item $\Gamma$ is the operation of pre-composition with the terminal object inclusion $\ast \hookrightarrow \mathcal{C}$


\item $Disc$ is the [[left Kan extension]] along the inclusion $\ast \hookrightarrow \mathcal{C}$ of the terminal object.



\end{enumerate}
The former is manifestly the operation of evaluating on the terminal object. Moreover, since the terminal object inclusion is manifestly a [[fully faithful functor]] (Def. \ref{FullyFaithfulFunctor}), it follows that also its [[left Kan extension]] $Disc$ is fully faithful (Prop. \ref{LeftKanExtensionAlongFullyFaithfulFunctor}). This implies that also $coDisc$ is fully faithful, by (Prop. \ref{FullyFaithfulAdjointTriple}).

Equivalently, $Disc \simeq p^\ast$ is the [[constant functor|constant]] [[diagram]]-assigning functor. By uniqueness of adjoints (Prop. \ref{UniquenessOfAdjoints}) implies that $\Pi$ is the functor that sends a presheaf, regarded as a [[functor]] $\mathbf{Y} \;\colon\; \mathcal{C}^{op} \to Set$, to its [[colimit]]

\begin{equation}
\Pi(\mathbf{Y})
  \;=\;
  \underset{\underset{\mathcal{C}^{op}}{\longrightarrow}}{\lim} \mathbf{Y}
  \,.
\label{Pi0IsColimit}\end{equation}
The fact that this indeed preserves products follows from the assumption that $\mathcal{C}$ has [[finite products]], since [[categories with finite products are cosifted]] (Prop. \ref{CategoriesWithFiniteProductsAreCosifted})

\end{proof}
Example \ref{PresheavesAdjointQuadrupleOnSiteWithTerminalObject} suggests to ask for [[coverages]] on categories with [[finite products]] which are such that the [[adjoint quadruple]] \eqref{PreaheafAdjointQuadruple} on the [[category of presheaves]] ([[corestriction|co-]])[[restriction|restricts]] to the corresponding [[category of sheaves]]. The following Definition \ref{OneCohesiveSite} states a sufficient condition for this to be the case:

\begin{defn}
\label{OneCohesiveSite}\hypertarget{OneCohesiveSite}{}
\textbf{([[cohesive site]])}

We call a [[site]] $\mathcal{C}$ (Def. \ref{Coverage}) \emph{[[cohesive site|cohesive]]} if the following conditions are satisfied:

\begin{enumerate}%
\item The [[category]] $\mathcal{C}$ has [[finite products]] (as in Example \ref{PresheavesAdjointQuadrupleOnSiteWithTerminalObject}).


\item For every [[covering]] family $\{U_i \to X\}_i$ in the given [[coverage]] on $\mathcal{C}$ the induced [[Cech groupoid]] $C(\{U_i\}_i) \in [C^{op}, Grpd]$ (Def. \ref{CechGroupoid}) satisfies the following two conditions:

\begin{enumerate}%
\item the set of [[connected components]] of the [[groupoid]] obtained as the [[colimit]] over the [[Cech groupoid]] is the [[singleton]]:

\begin{displaymath}
\pi_0
  \underset{\underset{\mathcal{C}^{op}}{\longrightarrow}}{\lim}
   C(\{U_i\})
   \;\simeq\;
   \ast
\end{displaymath}

\item the set of [[connected components]] of the [[groupoid]] obtained as the [[limit]] of the [[Cech groupoid]] is [[equivalence of categories|equivalent]] to the set of points of $X$, regarded as a groupoid:

\begin{displaymath}
\pi_0
  \underset{\underset{\mathcal{C}^{op}}{\longleftarrow}}{\lim} C(\{U_i\})
 \simeq
  Hom_{\mathcal{C}}(\ast,X)
  \,.
\end{displaymath}


\end{enumerate}


\end{enumerate}
\end{defn}
This definition is designed to make the following true:

\begin{prop}
\label{CategoriesOfSheavesOnCohesiveSiteIsCohesive}\hypertarget{CategoriesOfSheavesOnCohesiveSiteIsCohesive}{}
\textbf{([[category of sheaves]] on a [[cohesive site]] is a [[cohesive topos]])}

Let $\mathcal{C}$ be a [[cohesive site]] (Def. \ref{OneCohesiveSite}). Then the [[adjoint quadruple]] on the [[category of presheaves]] over $\mathcal{C}$, from Example \ref{PresheavesAdjointQuadrupleOnSiteWithTerminalObject} (given that a [[cohesive site]] by definition has [[finite products]]) ([[corestriction|co-]])[[restriction|restricts]] from the [[category of presheaves]] over $\mathcal{C}$, to the [[category of sheaves]] (Def. \ref{Sheaf}) and hence exhibits $Sh(\mathcal{C})$ as a [[cohesive topos]] (Def. \ref{CohesiveTopos}):

\begin{equation}
Sh(\mathcal{C})
    \itexarray{
      \overset{\phantom{AAA} \Pi \phantom{AAA}}{\longrightarrow}
      \\
      \overset{\phantom{AA} Disc \phantom{AA} }{\hookleftarrow}
      \\
      \overset{\phantom{AAA} \Gamma \phantom{AAA} }{\longrightarrow}
      \\
      \overset{\phantom{AA} coDisc \phantom{AA} }{\hookleftarrow}
    }
  Set
\label{SheafToposAdjointQuadruple}\end{equation}
\end{prop}
\begin{proof}
By example \ref{PresheavesAdjointQuadrupleOnSiteWithTerminalObject} we alreaday have the analogous statement for the [[categories of presheaves]]. Hence it is sufficient to show that the functors $Disc$ and $coDisc$ from Example \ref{PresheavesAdjointQuadrupleOnSiteWithTerminalObject} factor through the definition inclusion of the [[category of sheaves]], hence that for each [[set]] $S$ the [[presheaves]] $Disc(S)$ and $coDisc(S)$ are indeed [[sheaves]] (Def. \ref{Sheaf}).

By the formulaton of the [[sheaf|sheaf condition]] via the [[Cech groupoid]] (Prop. \ref{CechGroupoidCoRepresents}), and using the [[adjunction]] hom-isomorphisms (\href{geometry+of+physics+--+categories+and+toposes#eq:HomIsomorphismForAdjointFunctors}{here}) this is readily seen to be equivalent to the two further conditions on a cohesive site (Def. \ref{OneCohesiveSite}):

Let $\{U_i \to X\}$ be a [[covering]] family.

The sheaf condition \eqref{SheafIsLocalObjectWithRespectToCechCovers} for $Disc(S)$ says that

\begin{displaymath}
\left[
    C(\{U_i\}) \overset{p_{\{U_i\}_i}}{\to} y(X)
    \,,\,
    Disc(S)
  \right]
\end{displaymath}
is an [[isomorphism]] of [[groupoids]], which by adjunction and using \eqref{Pi0IsColimit} means equivalently that

\begin{displaymath}
\left[
    \underset{\underset{\mathcal{C}^{op}}{\longrightarrow}}{\lim}
    \left( C(\{U_i\}) \right) \to
    \ast
    \,,\,
    S
  \right]
\end{displaymath}
is an isomorphism of groupoids, where we used that colimits of representables are [[singletons]] (Lemma \ref{ColimitOfRepresentableIsSingleton}) to replace $\underset{\underset{\mathcal{C}^{op}}{\longrightarrow}}{\lim} y(X) \simeq \ast$.

But now in this [[internal hom]] of [[groupoids]], the set $S$ is really a groupoid in the image of the [[reflective subcategory|reflective embedding]] of sets into groupoids, whose [[left adjoint]] is the [[connected components]]-functor $\pi_0$ (Example \ref{ReflectiveSubcategoryInclusionOfSetsIntoGroupoids}). Hence by another adjunction isomoprhism this is equivalent to

\begin{displaymath}
\left[
    \pi_0
    \underset{\underset{\mathcal{C}^{op}}{\longrightarrow}}{\lim}
    \left( C(\{U_i\}) \right) \to
    \ast
    \,,\,
    S
  \right]
\end{displaymath}
being an isomorphism (a [[bijection]] of [[sets]], now). This is true for all $S \in Set$ precisely if (by the [[Yoneda lemma]], if you wish) the morphism

\begin{displaymath}
\pi_0
    \underset{\underset{\mathcal{C}^{op}}{\longrightarrow}}{\lim}
    \left( C(\{U_i\}) \right) \to
    \ast
\end{displaymath}
is already an isomorphism (here: [[bijection]]) itself.

Similarly, the sheaf condition \eqref{SheafIsLocalObjectWithRespectToCechCovers} for $coDisc(S)$ says that

\begin{displaymath}
\left[
    C(\{U_i\}) \overset{p_{\{U_i\}_i}}{\to} y(X)
    \,,\,
    coDisc(S)
  \right]
\end{displaymath}
is an [[isomorphism]], and hence by [[adjunction]] and using \eqref{CohesiveGlobalSectionsGivenByPointEvaluation}, this is equivalent to

\begin{displaymath}
\left[
    \pi_0
    \underset{\underset{\mathcal{C}^{op}}{\longleftarrow}}{\lim}
    C(\{U_i\})
    \overset{p_{\{U_i\}_i}}{\to}
    Hom_{\mathcal{C}}(\ast, X)
    \,,\,
    S
  \right]
\end{displaymath}
being an isomorphism. This holds for all $S \in Set$ if (by the [[Yoneda lemma]], if you wish)

\begin{displaymath}
\pi_0
    \underset{\underset{\mathcal{C}^{op}}{\longleftarrow}}{\lim}
    C(\{U_i\})
    \overset{p_{\{U_i\}_i}}{\to}
    Hom_{\mathcal{C}}(\ast, X)
\end{displaymath}
is an isomorphism.

\end{proof}
\begin{defn}
\label{CohesiveModalities}\hypertarget{CohesiveModalities}{}
\textbf{([[adjoint triple]] of [[adjoint modality|adjoint]] [[modal operators]] on [[cohesive topos]])}

Given a [[cohesive topos]] (Def. \ref{CohesiveTopos}), its [[adjoint quadruple]] (Remark \ref{AdjointTriples}) of functors to and from [[Set]]

\begin{equation}
\Pi \dashv Disc \dashv \Gamma \dashv coDisc
  \;\;\colon\;\;
  \mathbf{H}
    \itexarray{
      \overset{\phantom{AAA} \Pi \phantom{AAA}}{\longrightarrow}
      \\
      \overset{\phantom{AA} Disc \phantom{AA} }{\hookleftarrow}
      \\
      \overset{\phantom{AAA} \Gamma \phantom{AAA} }{\longrightarrow}
      \\
      \overset{\phantom{AA} coDisc \phantom{AA} }{\hookleftarrow}
    }
  Set
\label{CohesopmAdjointQuadruple}\end{equation}
induce, by [[composition]] of functors, an [[adjoint triple]] (Remark \ref{AdjointTriples}) of [[adjoint modalities]] (Def. \ref{AdjointModality}):

\begin{displaymath}
&#643; \dashv \flat \dashv \sharp
  \;\;\colon\;\;
  \mathbf{H}
    \itexarray{
      \overset{ &#643; \;\coloneqq\; Disc \circ \Pi  }{\hookleftarrow}
      \\
      \overset{\flat \;\coloneqq\; Disc \circ \Gamma  }{\longrightarrow}
      \\
      \overset{ \sharp \;\coloneqq\; coDisc\circ \Gamma }{\hookleftarrow}
    }
  \mathbf{H}
  \,.
\end{displaymath}
Since $Disc$ and $coDisc$ are [[fully faithful functors]] by assumption, these are ([[comodal operator|co-]])[[modal operators]] (Def. \ref{ModalOperator}) on the [[cohesive topos]], by (Prop. \ref{ModalOperatorsEquivalentToReflectiveSubcategories}).

We pronounce these as follows:

\begin{tabular}{l|l|l}
$\phantom{A}$ [[shape modality]] $\phantom{A}$&$\phantom{A}$ [[flat modality]] $\phantom{A}$&$\phantom{A}$ [[sharp modality]] $\phantom{A}$\\
\hline 
$\phantom{A}$ $&#643; \;\coloneqq\; Disc \circ \Pi$ $\phantom{A}$&$\phantom{A}$ $\flat \;\coloneqq\; Disc \circ \Gamma$ $\phantom{A}$&$\phantom{A}$ $\sharp \;\coloneqq\; coDisc \circ \Gamma$ $\phantom{A}$\\
\end{tabular}

and we refer to the corresponding [[modal objects]] (Def. \ref{ModalObjects}) as follows:

\begin{itemize}%
\item a [[flat modality|flat]]-[[comodal object]]

\begin{displaymath}
\flat X \underoverset{\simeq}{\phantom{A}\epsilon^\flat_X \phantom{A}}{\longrightarrow} X
\end{displaymath}
is called a \emph{[[discrete object]]};


\item a [[sharp modality|sharp]]-[[modal object]]

\begin{displaymath}
X \underoverset{\simeq}{\phantom{A}\eta^\sharp_X\phantom{A}}{\longrightarrow} \sharp X
\end{displaymath}
is called a \emph{[[codiscrete object]]};


\item a [[sharp modality|sharp]]-[[modal objects|submodal object]]

\begin{displaymath}
X \underoverset{mono}{\phantom{A}\eta^\sharp_X\phantom{A}}{\longrightarrow} \sharp X
\end{displaymath}
is a \emph{[[concrete object]]}.



\end{itemize}
\end{defn}
\begin{prop}
\label{PiecesHavePoints}\hypertarget{PiecesHavePoints}{}
\textbf{([[pieces have points]] $\simeq$ [[discrete objects are concrete]] $\simeq$ [[Aufhebung]] of [[bottom]] [[adjoint modality]])}

Let $\mathbf{H}$ be a [[cohesive topos]] (Def. \ref{CohesiveTopos}). Then the following conditions are equivalent:

\begin{enumerate}%
\item \textbf{[[pieces have points]]}: For every [[object]] $X \in \mathbf{H}$, \emph{comparison of extremes}-transformation \eqref{OppositeExtrmeComparison} for the $(&#643;, \dashv \flat)$-[[adjoint modality]] \eqref{OppositeExtrmeComparison}, hence the $\flat$-[[counit of an adjunction]] [[composition|composed]] with the -[[unit of an adjunction|unit]]

\begin{displaymath}
\flat X
    \overset{ \phantom{AA} \epsilon^\flat_X \phantom{AA} }{\longrightarrow}
  X
    \overset{ \phantom{AA} \epsilon^&#643;_X \phantom{AA} }{\longrightarrow}
  &#643; X
\end{displaymath}
is an [[epimorphism]] (Def. \ref{Monomorphism})


\item \textbf{[[discrete objects are concrete]]}: For every [[object]] $X \in \mathbf{H}$, we have that its [[discrete object]] $\flat X$ is a [[concrete object]] (Def. \ref{CohesiveModalities}).


\item \textbf{[[Aufhebung]] of [[bottom]] [[adjoint modality]]}

The [[adjoint modality]] $\flat \dashv \sharp$ exhibits [[Aufhebung]] (Def. \ref{Aufhebung}) of the [[bottom]] [[adjoint modality]] (Example \ref{InitialAndFinalAdjointModality}), i.e. the [[initial object]] (Def. \ref{InitialObject}) is [[codiscrete object|codiscrete]] (Def. \ref{CohesiveModalities}):

\begin{displaymath}
\sharp \emptyset \;\simeq\; \emptyset
  \,.
\end{displaymath}


\end{enumerate}
\end{prop}
\begin{proof}
The comparison morphism $ptp_{\mathbf{H}}$ is a special case of that discussed in Prop. \ref{ComparisonMorphismBetweenOppositeExtremes}. First observe, in the notation there, that

\begin{displaymath}
ptp_{\mathbf{H}} \;\; \text{is epi}
  \phantom{AAA}
  \text{iff}
  \phantom{AAA}
  ptp_{\mathbf{B}} \;\; \text{is epi}
  \,.
\end{displaymath}
In one direction, assume that $ptp_{\mathbf{B}}$ is an epimorphism. By \eqref{PiecesToPointsFromBase} we have $ptp_{\mathbf{H}} = Disc(ptp_{\mathbf{B}})$, but $Disc$ is a [[left adjoint]] and left adjoints preserve monomorphisms (Prop. \ref{LeftAdjointFunctorPreservesEpi}).

In the other direction, assume that $ptp_{\mathbf{H}}$ is an epimorphism. By \eqref{PointsToPiecesInTheBase} and \eqref{AdjunctOfptpH} we see that $ptp_{\mathbf{B}}$ is re-obtained from this by applying $\Gamma$ and then composition with isomorphisms. But $\Gamma$ is again a left adjoint, and hence preserves epimorphism by Prop. \ref{LeftAdjointFunctorPreservesEpi}, as does composition with isomorphisms.

By applying \eqref{PointsToPiecesInTheBase} again, we find in particular that \emph{[[pieces have points]]} is also equivalent to $\Pi \epsilon^\flat_{Disc S}$ being an epimorphism, for all $S \in \mathbf{B}$. But this is equivalent to

\begin{displaymath}
Hom_{\mathbf{B}}(\Pi \epsilon^\flat_{\mathbf{X}}, S)
  =
  Hom_{\mathbf{\mathbf{H}}}(\epsilon^\flat_{\mathbf{X}}, Disc(S))
\end{displaymath}
being a [[monomorphism]] for all $S$ (by adjunction isomorphism \eqref{HomIsomorphismForAdjointFunctors} and definition of [[epimorphism]], Def. \ref{Monomorphism}).

Now by Lemma \ref{ReExpressingMiddleFunctorInAdjointTriple}, this is equivalent to

\begin{displaymath}
Hom_{\mathbf{H}}( \mathbf{X}, \eta^\sharp_{Disc(S)} )
\end{displaymath}
being an injection for all $\mathbf{X}$, which, by Def. \ref{Monomorphism}, is equivalent to $\eta^\sharp_{Disc(S)}$ being a monomorphism, hence to \emph{[[discrete objects are concrete]]}.

This establishes the equivalence between the first two items.

\end{proof}
\begin{prop}
\label{CohesiveSiteSuchThatDiscreteObjectsAreConcrete}\hypertarget{CohesiveSiteSuchThatDiscreteObjectsAreConcrete}{}
\textbf{([[cohesive site]] such that [[pieces have points]]/[[discrete objects are concrete]])}

Let $\mathcal{C}$ be a [[cohesive site]] (Def. \ref{OneCohesiveSite}), such that

\begin{itemize}%
\item for every [[object]] $X \in \mathcal{C}$, there is at least one [[morphism]] $\ast \overset{\exists}{\to} X$ from [[generalized the|the]] [[terminal object]] to $X$, hence such that the [[hom set]] $Hom_{\mathcal{C}}(\ast, X)$ is [[inhabited set|non-empty]].

\end{itemize}
Then the [[cohesive topos]] $Sh(\mathcal{C})$, according to Prop. \ref{CategoriesOfSheavesOnCohesiveSiteIsCohesive}, satisfies the equivalent conditions from Prop. \ref{PiecesHavePoints}:

\begin{enumerate}%
\item [[pieces have points]],


\item [[discrete objects are concrete]].



\end{enumerate}
\end{prop}
\begin{proof}
By Prop. \ref{PiecesHavePoints} it is sufficient to show the second condition, hence to check that for each [[set]] $S \in Set$, the canonical morphism

\begin{displaymath}
Disc(S) \longrightarrow coDisc(S)
\end{displaymath}
is a [[monomorphism]]. By Prop. \ref{RecognitionOfEpimorphisms} this means equivalently that for each [[object]] $X \in \mathcal{C}$ in the site, the component function

\begin{displaymath}
Disc(S)(X) \longrightarrow coDisc(S)(X)
\end{displaymath}
is an [[injective function]].

Now, by the proof of Prop. \ref{CategoriesOfSheavesOnCohesiveSiteIsCohesive}, this is the [[diagonal]] function

\begin{displaymath}
\itexarray{
    S
     & \longrightarrow&
    Hom_{Set}\left( Hom_{\mathcal{C}}(\ast, X), S \right)
    \\
    s &\mapsto& const_s
  }
\end{displaymath}
This function is [[injective function|injective]] precisely if $Hom_{\mathcal{C}}(\ast, X)$ is [[inhabited set|non-empty]], which is true by assumption.

\end{proof}
\begin{prop}
\label{QuasitoposOfConcreteObjects}\hypertarget{QuasitoposOfConcreteObjects}{}
\textbf{([[quasitopos]] of [[concrete objects]] in a [[cohesive topos]])}

For $\mathbf{H}$ a [[cohesive topos]] (Def. \ref{CohesiveTopos}), write

\begin{displaymath}
\mathbf{H}_{conc}
  \overset{ \phantom{AAAA} }{\hookrightarrow}
  \mathbf{H}
\end{displaymath}
for its [[full subcategory]] (Example \ref{FullSubcategoryOnClassOfObjects}) of [[concrete objects]] (Def. \ref{CohesiveModalities}).

Then there is a sequence of [[reflective subcategory]]-inclusions (Def. \ref{ReflectiveSubcategory}) that factor the $(\Gamma \dashv coDisc)$-adjunction as

\begin{displaymath}
\Gamma \;\dashv\; coDisc
  \;\;\colon\;\;
  \mathbf{H}
  \itexarray{
    \overset{\phantom{AA} conc \phantom{AA}}{\longrightarrow}
    \\
    \overset{\phantom{AA} \iota_{conc} \phantom{AA}}{\hookleftarrow}
  }
  \mathbf{H}_{conc}
  \itexarray{
    \overset{\phantom{AA}\Gamma \phantom{AA}}{\longrightarrow}
    \\
    \overset{\phantom{AA}coDisc\phantom{AA}}{\hookleftarrow}
  }
  Set
\end{displaymath}
If in addition [[discrete objects are concrete]] (Prop. \ref{PiecesHavePoints}), then the full [[adjoint quadruple]] factors through the [[concrete objects]]:

\begin{displaymath}
\itexarray{
     \\
     \phantom{a}
     \\
     \phantom{A}
     \\
     \Gamma \;\dashv\; coDisc
  }
  \;\;\colon\;\;
  \mathbf{H}
  \itexarray{
    \phantom{\overset{ \phantom{AA} \Pi \phantom{AA} }{\longrightarrow}}
    \\
    \phantom{\overset{ \phantom{AA} Disc \phantom{AA} }{\hookleftarrow}}
    \\
    \overset{\phantom{AA} conc \phantom{AA}}{\longrightarrow}
    \\
    \overset{\phantom{AA} \iota_{conc} \phantom{AA}}{\hookleftarrow}
  }
  \mathbf{H}_{conc}
  \itexarray{
    \overset{ \phantom{AA} \Pi \phantom{AA} }{\longrightarrow}
    \\
    \overset{ \phantom{AA} Disc \phantom{AA} }{\hookleftarrow}
    \\
    \overset{\phantom{AA}\Gamma \phantom{AA}}{\longrightarrow}
    \\
    \overset{\phantom{AA}coDisc\phantom{AA}}{\hookleftarrow}
  }
  Set
\end{displaymath}
\end{prop}
\begin{proof}
For the adjunction on the right, we just need to observe that for every [[set]] $S \in Set$, the [[codiscrete object]] $coDisc(S)$ is [[concrete object|concrete]], which is immediate by [[idempotent monad|idempotency]] of $\sharp$ (Prop. \ref{ModalOpIdempotent}) and the fact that every [[isomorphism]] is also a [[monomorphism]]. Similarly, the assumption that [[discrete objects are concrete]] says exactly that also $Disc$ factors through $\mathbf{H}_{conc}$.

For the adjunction on the left we claim that the [[left adjoint]] $conc$, (to be called \emph{[[concretification]]}), is given by sending each [[object]] to the [[image]] (Def. \ref{SheafToposEpiMonoFactorization}) of its $(\Gamma \dashv coDisc)$ [[adjunction unit]] $\eta^\sharp$:

\begin{displaymath}
conc \;\colon\; X \mapsto im(\eta^\sharp_X)
  \,,
\end{displaymath}
hence to the object which exhibits the [[(epi, mono) factorization system|epi/mono-factorization]] (Prop. \ref{SheafToposEpiMonoFactorization}) of $\eta^\sharp_X$

\begin{equation}
\eta^\sharp_X
  \;\colon\;
  X
    \underoverset{epi}{ \eta^{conc}_X }{\longrightarrow}
  conc X
    \underoverset{mono}{}{\longrightarrow}
  \sharp X
  \,.
\label{ConcretificationUnitFromEpiMonoFactorization}\end{equation}
First we need to show that $conc X$, thus defined, is indeed [[concrete object|concrete]], hence that $\eta^\sharp_{im(\eta^\sharp_X)}$ is a [[monomorphism]] (Def. \ref{Monomorphism}). For this, consider the following [[naturality square]] \eqref{NaturalitySquareForAdjointnessOfFunctors} of the $\Gamma \dashv coDisc$-adjunction hom-isomorphism

\begin{equation}
\itexarray{
    Hom_{Set}( \Gamma im(\eta^\sharp_X), \Gamma im(\eta^\sharp_X) )
    &\simeq&
    Hom_{\mathbf{H}}( im(\eta^\sharp_X), \sharp im(\eta^\sharp_X) )
    \\
    {}^{ \mathllap{ (-) \circ \Gamma(\eta^{conc}_X) } }\big\downarrow
      &&
    \big\downarrow^{
      \mathrlap{ (-) \circ \eta^{conc}_X }
    }
    \\
    Hom_{Set}( \Gamma X, \Gamma im(\eta^\sharp_X) )
    &\simeq&
    Hom_{\mathbf{H}}( X, \sharp im(\eta^\sharp_X) )
  }
  \phantom{AAAA}
  \itexarray{
    \left\{ id_{\Gamma im(\eta^\sharp_X)} \right\}
      &\longrightarrow&
    \phantom{\sharp(\eta^{conc}_X) \circ \eta^\sharp_{ X }}
    \left\{ \eta^{\sharp}_{im(\eta^\sharp_X)} \right\}
    \\
    \big\downarrow
      &&
    \phantom{\sharp(\eta^{conc}_X) \circ \eta^\sharp_{ X }}
    \big\downarrow
    \\
    \left\{ \Gamma(\eta^{conc}_X) \right\}
      &\longrightarrow&
    \left\{
      \underset{
        iso
      }{
      \underbrace{
         \sharp(\eta^{conc}_X)
      }}
      \circ \eta^\sharp_{ X }
      \;=\;
    \eta^{\sharp}_{ im(\eta^\sharp_X) } \circ \eta^{conc}_X
    \right\}
  }
\label{ConcNatur}\end{equation}
By chasing the [[identity morphism]] on $\Gamma im(\eta^\sharp_X)$ through this diagram, as shown by the diagram on the right, we obtain the equality displayed in the bottom right entry, where we used the general formula for [[adjuncts]] (Prop. \ref{GeneralAdjunctsInTermsOfAdjunctionUnitCounit}) and the definition $\sharp \coloneqq coDisc \circ \Gamma$ (Def. \ref{CohesiveModalities}).

But observe that $\Gamma (\eta^{conc}_X)$, and hence also $\sharp(\eta^{conc}_X)$, is an [[isomorphism]] (Def. \ref{Isomorphism}), as indicated above: Since $\Gamma$ is both a [[left adjoint]] as well as a [[right adjoint]], it preserves both [[epimorphisms]] as well as [[monomorphisms]] (Prop. \ref{LeftAdjointFunctorPreservesEpi}), hence it preserves [[image]] factorizations (Prop. \ref{SheafToposEpiMonoFactorization}). This implies that $\Gamma \eta^{conc}_X$ is the epimorphism onto the image of $\Gamma( \eta^\sharp_X )$. But by [[idempotent monad|idempotency]] of $\sharp$, the latter is an [[isomorphism]], and hence so is the epimorphism in its image factorization.

Therefore the equality in \eqref{ConcNatur} says that

\begin{displaymath}
\begin{aligned}
    \eta^\sharp_{ X }
      & =
    \left(
      iso \circ \eta^{\sharp}_{ im(\eta^\sharp_X)}
    \right)
      \circ
    \eta^{conc}_X
    \\
    & =
    mono \circ \eta^{conc}_X
    \,,
  \end{aligned}
\end{displaymath}
where in the second line we remembered that $\eta^{conc}_X$ is, by definition, the epimorphism in the epi/mono-factorization of $\eta^\sharp_X$.

Now the defining property of epimorphisms (Def. \ref{Monomorphism}) allows to cancel this commmon factor on both sides, which yields

\begin{displaymath}
\eta^{\sharp}_{ im(\eta^\sharp_X) }
  \;=\;
  iso \circ mono
  \;=\;
  mono.
\end{displaymath}
This shows that $conc X \coloneqq im(\eta^\sharp_X)$ is indeed concret.

$\,$

It remains to show that this construction is [[left adjoint]] to the inclusion. We claim that the [[adjunction unit]] (Def. \ref{AdjunctionUnitFromHomIsomorphism}) of $(conc \dashv \iota_{conc})$ is provided by $\eta^{conc}$ \eqref{ConcretificationUnitFromEpiMonoFactorization}.

To see this, first notice that, since the [[(epi, mono) factorization system|epi/mono-factorization]] (Prop. \ref{SheafToposEpiMonoFactorization}) is [[orthogonal factorization system|orthogonal]] and hence [[functorial factorization|functorial]], we have [[commuting diagrams]] of the form

\begin{equation}
\itexarray{
    X_1
      &\underoverset{epi}{\eta^{conc}_{X_1}}{\longrightarrow}&
    im(\eta^\sharp_{X_1})
      &\underset{mono}{\longrightarrow}&
    \sharp X_1
    \\
    \big\downarrow && \big\downarrow && \big\downarrow
    \\
    X_2
      &\underoverset{epi}{\eta^{conc}_{X_2}}{\longrightarrow}&
    im(\eta^\sharp_{X_2})
      &\underset{mono}{\longrightarrow}&
    \sharp X_2
  }
\label{NaturalitySquareForConcretificationUnit}\end{equation}
Now to demonstrate the adjunction it is sufficient, by Prop. \ref{CollectionOfUniversalArrowsEquivalentToAdjointFunctor}, to show that $\eta^{conc}$ is a [[universal morphism]] in the sense of Def. \ref{UniversalArrow}. Hence consider any morphism $f \;\colon\; X_1 \to X_2$ with $X_2 \in \mathbf{H}_{conc} \hookrightarrow \mathbf{H}$. Then we need to show that there is a unique diagonal morphism as below, that makes the following \emph{top left triangle} [[commuting diagram|commute]]:

\begin{displaymath}
\itexarray{
    X_1
      &\overset{\phantom{AA} f \phantom{AA}}{\longrightarrow}&
    X_2
    \\
    {}^{\mathllap{epi}}\big\downarrow^{\mathrlap{\eta^{conc}_{X_1}}}
      &{}^{\mathllap{\exists !}}\nearrow&
    \big\downarrow^{\mathrlap{mono}}
    \\
    im(\eta^\sharp_{X_1})
      &\underset{}{\longrightarrow}&
    \sharp X_2
  }
\end{displaymath}
Now, from \eqref{NaturalitySquareForConcretificationUnit}, we have a [[commuting square]] as shown. Here the left morphism is an [[epimorphism]] by construction, while the right morphism is a [[monomorphism]] by assumption on $X_2$. With this, the [[(epi, mono) factorization system|epi/mono-factorization]] in Prop. \ref{SheafToposEpiMonoFactorization} says that there is a diagonal [[lift]] which makes \emph{both} triangles [[commuting diagram|commute]].

It remains to see that the lift is unique with just the property of making the top left triangle commute. But this is equivalently the statement that the left morphism is an epimorphism, by Def. \ref{Monomorphism}.

\end{proof}
The equivalence of the first two follows with (\href{cohesive+topos#Johnstone}{Johnstone, lemma 2.1, corollary 2.2}). The equivalence of the first and the last is due to \href{cohesive+topos#LawvereMenni15}{Lawvere-Menni 15, lemma 4.1, lemma 4.2}.

$\,$

\hypertarget{ElasticToposes}{}\subsubsection*{{Elastic toposes}}\label{ElasticToposes}

\begin{defn}
\label{DifferentialCohesion}\hypertarget{DifferentialCohesion}{}
\textbf{([[elastic topos]])}

Let $\mathbf{H}_{red}$ be a [[cohesive topos]] (Def. \ref{CohesiveTopos}). Then an \emph{[[elastic topos]]} or \emph{[[differentially cohesive topos]]} over $\mathbf{H}_{red}$ is a [[sheaf topos]] $\mathbf{H}$ which is

\begin{enumerate}%
\item a [[cohesive topos]] over [[Set]],


\item equipped with a [[adjoint quadruple|quadruple]] of [[adjoint functors]] (Def. \ref{AdjointFunctorsInTermsOfNaturalBijectionOfHomSets}) to $\mathbf{H}_{red}$ of the form

\begin{displaymath}
\mathbf{H}_{red}
    \itexarray{
      \overset{\phantom{AA} \iota_{inf} \phantom{AA} }{\hookrightarrow}
      \\
      \overset{\phantom{AA} \Pi_{inf} \phantom{AA} }{\longleftarrow}
      \\
      \overset{\phantom{AA} Disc_{inf} \phantom{AA} }{\hookrightarrow}
      \\
      \overset{\phantom{AA} \Gamma_{inf} \phantom{AA} }{\longleftarrow}
    }
  \mathbf{H}
\end{displaymath}


\end{enumerate}
\end{defn}
\begin{lemma}
\label{ProgressionOfSubcategoriesOfElasticTopos}\hypertarget{ProgressionOfSubcategoriesOfElasticTopos}{}
\textbf{(progression of ([[coreflective subcategory|co-]])[[reflective subcategories]] of [[elastic topos]])}

Let $\mathbf{H}$ be an [[elastic topos]] (Def. \ref{DifferentialCohesion}) over a [[cohesive topos]] $\mathbf{H}_{red}$ (Def. \ref{CohesiveTopos}):

\begin{displaymath}
Set
    \itexarray{
      \overset{\phantom{A} \Pi_{red} \phantom{A} }{\longleftarrow}
      \\
      \overset{\phantom{A} Disc_{red} \phantom{A} }{\hookrightarrow}
      \\
      \overset{\phantom{A} \Gamma_{red} \phantom{A} }{\longleftarrow}
      \\
      \overset{\phantom{A} coDisc_{red} \phantom{A} }{\hookrightarrow}
    }
  \mathbf{H}_{red}
    \itexarray{
      \overset{\phantom{AA} \iota_{inf} \phantom{AA} }{\hookrightarrow}
      \\
      \overset{\phantom{AA} \Pi_{inf} \phantom{AA} }{\longleftarrow}
      \\
      \overset{\phantom{AA} Disc_{inf} \phantom{AA} }{\hookrightarrow}
      \\
      \overset{\phantom{AA} \Gamma_{inf} \phantom{AA} }{\longleftarrow}
      \\
      \phantom{A}
      \\
      \phantom{a}
    }
  \mathbf{H}
\end{displaymath}
and write

\begin{displaymath}
Set
    \itexarray{
      \overset{\phantom{AA} \Pi \phantom{AA} }{\longleftarrow}
      \\
      \overset{\phantom{AA} Disc \phantom{AA} }{\hookrightarrow}
      \\
      \overset{\phantom{AA} \Gamma \phantom{AA} }{\longleftarrow}
      \\
      \overset{\phantom{AA} coDisc \phantom{AA} }{\hookrightarrow}
    }
  \mathbf{H}
\end{displaymath}
for the [[adjoint quadruple]] exhibiting the [[cohesion]] of $\mathbf{H}$ itself. Then these adjoint functors arrange and decompose as in the following [[diagram]]

\end{lemma}
\begin{proof}
The identification

\begin{displaymath}
(Disc \dashv \Gamma)
  \;\simeq\;
  ( Disc_{inf} \circ Disc_{red} \,\dashv\, \Gamma_{red} \circ \Gamma_{inf} )
\end{displaymath}
follows from the essential uniqueness of the [[global section]]-[[geometric morphism]] (Example \ref{GlobalSectionsGeometricMorphism}). This implies the identifications $\Pi \simeq \Pi_{red} \circ \Pi_{inf}$ by essential uniqueness of [[adjoints]] (Prop. \ref{UniquenessOfAdjoints}).

\end{proof}
\begin{defn}
\label{DiffCohesiveModalities}\hypertarget{DiffCohesiveModalities}{}
\textbf{([[adjoint modalities]] on [[elastic topos]])}

Given an [[elastic topos]] ([[differentially cohesive topos]]) $\mathbf{H}$ over $\mathbf{H}_{red}$ (Def. \ref{DifferentialCohesion}), [[composition]] of the functors in Lemma \ref{ProgressionOfSubcategoriesOfElasticTopos} yields, via Prop. \ref{ModalOperatorsEquivalentToReflectiveSubcategories}, the following [[adjoint modalities]] (Def. \ref{AdjointModality})

\begin{displaymath}
\Re \dashv \Im \dashv \&
  \;\;\colon\;\;
  \mathbf{H}
    \itexarray{
      \overset{ \Re \;\coloneqq\; \iota_{inf} \circ \Pi_{inf}  }{\longleftarrow}
      \\
      \overset{\Im \;\coloneqq\; Disc_{inf} \circ \Pi_{inf}  }{\longrightarrow}
      \\
      \overset{ \& \;\coloneqq\; Disc_{inf}  \circ \Gamma_{inf} }{\longleftarrow}
    }
  \mathbf{H}
  \,.
\end{displaymath}
Since $\iota_{inf}$ and $Disc_{inf}$ are [[fully faithful functors]] by assumption, these are ([[comodal operator|co-]])[[modal operators]] (Def. \ref{ModalOperator}) on the [[cohesive topos]], by (Prop. \ref{ModalOperatorsEquivalentToReflectiveSubcategories}).

We pronounce these as follows:

\begin{tabular}{l|l|l}
$\phantom{A}$ [[reduction modality]] $\phantom{A}$&$\phantom{A}$ [[infinitesimal shape modality]] $\phantom{A}$&$\phantom{A}$ [[infinitesimal flat modality]] $\phantom{A}$\\
\hline 
$\phantom{A}$ $\Re \;\coloneqq\; \iota_{inf} \circ \Pi_{inf}$ $\phantom{A}$&$\phantom{A}$ $\Im \;\coloneqq\; Disc_{inf} \circ \Pi_{inf}$ $\phantom{A}$&$\phantom{A}$ $\& \;\coloneqq\; Disc_{inf} \circ \Gamma_{inf}$ $\phantom{A}$\\
\end{tabular}

and we refer to the corresponding [[modal objects]] (Def. \ref{ModalObjects}) as follows:

\begin{itemize}%
\item a [[reduction modality|reduction]]-[[comodal object]]

\begin{displaymath}
\Re X
    \underoverset{\simeq}{\epsilon^\Re_X}{\longrightarrow}
  X
\end{displaymath}
is called a \emph{[[reduced object]]};


\item an [[infinitesimal shape modality|infinitesimal shape]]-[[modal object]]

\begin{displaymath}
X \underoverset{\simeq}{\phantom{A}\eta^\Im_X\phantom{A}}{\longrightarrow} \Im X
\end{displaymath}
is called a \emph{[[coreduced object]]}.



\end{itemize}
\end{defn}
\begin{prop}
\label{ProgressionOfModalitiesOnElasticTopos}\hypertarget{ProgressionOfModalitiesOnElasticTopos}{}
\textbf{(progression of [[adjoint modalities]] on [[elastic topos]])}

Let $\mathbf{H}$ be an [[elastic topos]] (Def. \ref{DifferentialCohesion}) and consider the corresponding [[adjoint modalities]] which it inherits

\begin{enumerate}%
\item for being a [[cohesive topos]], from Def. \ref{CohesiveModalities},


\item for being an [[elastic topos]], from Def. \ref{DiffCohesiveModalities}:



\end{enumerate}
\begin{tabular}{l|l|l}
$\phantom{A}$ [[shape modality]] $\phantom{A}$&$\phantom{A}$ [[flat modality]] $\phantom{A}$&$\phantom{A}$ [[sharp modality]] $\phantom{A}$\\
\hline 
$\phantom{A}$ $&#643; \;\coloneqq\; Disc \circ \Pi$ $\phantom{A}$&$\phantom{A}$ $\flat \;\coloneqq\; Disc \circ \Gamma$ $\phantom{A}$&$\phantom{A}$ $\sharp \;\coloneqq\; coDisc \circ \Gamma$ $\phantom{A}$\\
&&\\
$\phantom{A}$ [[reduction modality]] $\phantom{A}$&$\phantom{A}$ [[infinitesimal shape modality]] $\phantom{A}$&$\phantom{A}$ [[infinitesimal flat modality]] $\phantom{A}$\\
$\phantom{A}$ $\Re \;\coloneqq\; \iota_{inf} \circ \Pi_{inf}$ $\phantom{A}$&$\phantom{A}$ $\Im \;\coloneqq\; Disc_{inf} \circ \Pi_{inf}$ $\phantom{A}$&$\phantom{A}$ $\& \;\coloneqq\; Disc_{inf} \circ \Gamma_{inf}$ $\phantom{A}$\\
\end{tabular}

Then these arrange into the following progression, via the [[preorder]] on modalities from Def. \ref{PreorderOnModalities}

\begin{displaymath}
\itexarray{
    \Re &\dashv& \Im &\dashv& \&
    \\
    && \vee && \vee
    \\
    && &#643; &\dashv& \flat &\dashv& \sharp
    \\
    && && \vee && \vee
    \\
    && && \emptyset &\dashv& \ast
  }
\end{displaymath}
where we display also the [[bottom]] [[adjoint modality]] $\emptyset \dashv \ast$ (Example \ref{InitialAndFinalAdjointModality}), for completeness.

\end{prop}
\begin{proof}
We need to show, for all $X \in \mathbf{H}$, that

\begin{enumerate}%
\item $\flat X$ is an $\&$-[[modal object]] (Def. \ref{ModalObjects}), hence that

\begin{displaymath}
\& \flat X  \;\simeq\; X
\end{displaymath}

\item $&#643; X$ is an $\Im$-[[modal object]] (Def. \ref{ModalObjects}), hence that

\begin{displaymath}
\Im &#643; X  \;\simeq\; X
\end{displaymath}


\end{enumerate}
After unwinding the definitions of the modal operators Def. \ref{CohesiveModalities} and Def. \ref{CohesiveModalities}, and using their re-identification from Lemma \ref{ProgressionOfSubcategoriesOfElasticTopos}, this comes down to the fact that

\begin{displaymath}
\Pi_{inf} Disc_{inf} \;\simeq\; id
  \phantom{AAA}
  \text{and}
  \phantom{AAA}
  \Gamma_{inf} Disc_{inf} \;\simeq\; id
  \,,
\end{displaymath}
which holds by Prop. \ref{FullyFaithfulAndInvertibleAdjoints}, since $Disc_{inf}$ is a [[fully faithful functor]] and $\Pi_{inf}$, $Gamma_{inf}$ are ([[coreflective subcategory|co-]])[[reflective subcategory|reflectors]] for it, respectively:

\begin{displaymath}
\begin{aligned}
    \underset{Disc_{inf} \Gamma_{inf}}{\underbrace{\;\;\;\&\;\;\;}}
    \underset{Disc \Gamma }{\underbrace{\;\;\;\flat\;\;\;}}
    &
    =
     Disc_{inf} \Gamma_{inf}
    \underset{ Disc_{inf} Disc_{red} }{\underbrace{\;\;\;\Disc\;\;\;}} \Gamma
    \\
    & =
    \underset{
      \simeq Disc
    }{
    \underbrace{
      Disc_{inf} \underset{\simeq id}{\underbrace{\Gamma_{inf} Disc_{inf}}} Disc_{red}
    }}
    \; \Gamma
    \\
    & \simeq
    \underset{ Disc }{\underbrace{ Disc_{inf} Disc_{red} }} \Gamma \mathbf{X}
    \\
    & =
    Disc \Gamma
    \\
    & = \flat
  \end{aligned}
\end{displaymath}
and

\begin{displaymath}
\itexarray{
    \underset{
      Disc_{inf} \Pi_{inf}
    }{
    \underbrace{
      \;\;\;\Im\;\;\;
    }}
    \underset{
      Disc \Pi
    }{
    \underbrace{
      \;\;\;&#643;\;\;\;
    }
    }
    & =
    Disc_{inf}
    \Pi_{inf}
    \underset{
      Disc_{inf} Disc_{red}
    }{
    \underbrace{
      \;\;\;Disc\;\;\;
   }
   }
   \Pi
   \\
   & =
   \underset{
     \simeq Disc
   }{
   \underbrace{
   Disc_{inf}
   \underset{
     \simeq id
   }{
   \underbrace{
     \Pi_{inf}
     Disc_{inf}
   }
   }
   Disc_{red}
   }
   }
   \Pi
   \\
   & \simeq
   Disc
   \Pi
   \\
   & =
   &#643;
  }
\end{displaymath}
\end{proof}
$\,$

\hypertarget{SolidToposes}{}\subsubsection*{{Solid toposes}}\label{SolidToposes}

\begin{defn}
\label{SuperDifferentialCohesion}\hypertarget{SuperDifferentialCohesion}{}
\textbf{([[solid topos]])}

Let $\mathbf{H}_{bos}$ be an [[elastic topos]] (Def. \ref{DifferentialCohesion}) over a [[cohesive topos]] $\mathbf{H}_{red}$ (Def. \ref{CohesiveTopos}). Then a \emph{[[solid topos]]} or \emph{[[super-differentially cohesive topos]]} over $\mathbf{H}_{bos}$ is a [[sheaf topos]] $\mathbf{H}$, which is

\begin{enumerate}%
\item a [[cohesive topos]] over [[Set]] (Def. \ref{CohesiveTopos}),


\item an [[elastic topos]] over $\mathbf{H}_{red}$,


\item equipped with a [[adjoint quadruple|quadruple]] of [[adjoint functors]] (Def. \ref{AdjointFunctorsInTermsOfNaturalBijectionOfHomSets}) to $\mathbf{H}_{bos}$ of the form

\begin{displaymath}
\mathbf{H}_{bos}
    \itexarray{
      \overset{\phantom{A} even \phantom{A} }{\longleftarrow}
      \\
      \overset{\phantom{AA} \iota_{sup} \phantom{AA} }{\hookrightarrow}
      \\
      \overset{\phantom{AA} \Pi_{sup} \phantom{AA} }{\longleftarrow}
      \\
      \overset{\phantom{AA} Disc_{sup} \phantom{AA} }{\hookrightarrow}
    }
  \mathbf{H}
\end{displaymath}
hence with $\iota_{sup}$ and $Disc_{sup}$ being [[fully faithful functors]] (Def. \ref{FullyFaithfulFunctor}).



\end{enumerate}
\end{defn}
\begin{lemma}
\label{ProgressionOfSubcategoriesOfSolidTopos}\hypertarget{ProgressionOfSubcategoriesOfSolidTopos}{}
\textbf{(progression of ([[coreflective subcategory|co-]])[[reflective subcategories]] of [[solid topos]])}

Let $\mathbf{H}$ be a [[solid topos]] (Def. \ref{SuperDifferentialCohesion}) over an [[elastic topos]] $\mathbf{H}_{red}$ (Def. \ref{DifferentialCohesion}):

\begin{displaymath}
Set
    \itexarray{
      \overset{\phantom{A} \Pi_{red} \phantom{A} }{\longleftarrow}
      \\
      \overset{\phantom{A} Disc_{red} \phantom{A} }{\hookrightarrow}
      \\
      \overset{\phantom{A} \Gamma_{red} \phantom{A} }{\longleftarrow}
      \\
      \overset{\phantom{A} coDisc_{red} \phantom{A} }{\hookrightarrow}
    }
  \mathbf{H}_{red}
    \itexarray{
      \overset{\phantom{AA} \iota_{inf} \phantom{AA} }{\hookrightarrow}
      \\
      \overset{\phantom{AA} \Pi_{inf} \phantom{AA} }{\longleftarrow}
      \\
      \overset{\phantom{AA} Disc_{inf} \phantom{AA} }{\hookrightarrow}
      \\
      \overset{\phantom{AA} \Gamma_{inf} \phantom{AA} }{\longleftarrow}
      \\
      \phantom{A}
      \\
      \phantom{A \atop A}
    }
  \mathbf{H}_{bos}
    \itexarray{
      \overset{\phantom{AA} even \phantom{AA} }{\longleftarrow}
      \\
      \overset{\phantom{AA} \iota_{sup} \phantom{AA} }{\hookrightarrow}
      \\
      \overset{\phantom{AA} \Pi_{sup} \phantom{AA} }{\longleftarrow}
      \\
      \overset{\phantom{AA} Disc_{sup} \phantom{AA} }{\hookrightarrow}
      \\
      \overset{\phantom{AA} \Gamma_{sup} \phantom{AA} }{\longleftarrow}
      \\
      \phantom{A}
      \\
      \phantom{A \atop A}
      \\
      \phantom{A \atop A}
    }
  \mathbf{H}
\end{displaymath}
Then these adjoint functors arrange and decompose as shown in the following [[diagram]]:

Here the composite [[adjoint quadruple]]

\begin{displaymath}
Set
    \itexarray{
      \overset{\Pi \simeq \Pi_{red}\Pi_{inf} \Pi_{sup} }{\longleftarrow}
      \\
      \overset{Disc = Disc_{sup} Disc_{inf} Disc_{red}}{\hookrightarrow}
      \\
      \overset{\Gamma = \Gamma_{sup} \Gamma_{inf} \Gamma_{red} }{\longleftarrow}
      \\
      \overset{\phantom{AA} coDisc \phantom{AA} }{\hookrightarrow}
    }
  \mathbf{H}
\end{displaymath}
exhibits the [[cohesion]] of $\mathbf{H}$ over [[Set]], and the composite adjoint quadruple

\begin{displaymath}
\mathbf{H}_{red}
    \itexarray{
      \overset{\iota_{sup} \iota_{inf}}{\hookrightarrow}
      \\
      \overset{\Pi_{inf} \Pi_{sup} }{\longleftarrow}
      \\
      \overset{Disc_{inf} Disc_{red}}{\hookrightarrow}
      \\
      \overset{ \Gamma_{sup} }{\longleftarrow}
    }
  \mathbf{H}
\end{displaymath}
exhibits the [[elastic topos|elasticity]] of $\mathbf{H}$ over $\mathbf{H}_{red}$.

\end{lemma}
\begin{proof}
As in the proof of Prop. \ref{ProgressionOfSubcategoriesOfElasticTopos}, this is immediate by the essential uniqueness of adjoints (Prop. \ref{UniquenessOfAdjoints}) and of the [[global section]]-[[geometric morphism]] (Example \ref{GlobalSectionsGeometricMorphism}).

\end{proof}
\begin{defn}
\label{SuperDiffCohesiveModalities}\hypertarget{SuperDiffCohesiveModalities}{}
\textbf{([[adjoint modalities]] on [[solid topos]])}

Given a [[solid topos]] $\mathbf{H}$ over $\mathbf{H}_{bos}$ (Def. \ref{SuperDifferentialCohesion}), [[composition]] of the functors in Lemma \ref{ProgressionOfSubcategoriesOfSolidTopos} yields, via Prop. \ref{ModalOperatorsEquivalentToReflectiveSubcategories}, the following [[adjoint modalities]] (Def. \ref{AdjointModality})

\begin{displaymath}
\rightrightarrows
  \;\dashv\;
  \rightsquigarrow
  \;\dashv\;
  Rh
  \;\;\colon\;\;
  \mathbf{H}
    \itexarray{
      \overset{ \rightrightarrows \;\coloneqq\; \iota_{sup} \circ even  }{\longleftarrow}
      \\
      \overset{\rightsquigarrow \;\coloneqq\; \iota_{sup} \circ \Pi_{sup}  }{\longrightarrow}
      \\
      \overset{ Rh \;\coloneqq\; Disc_{sup}  \circ \Pi_{sup} }{\longleftarrow}
    }
  \mathbf{H}
  \,.
\end{displaymath}
Since $\iota_{sup}$ and $Disc_{sup}$ are [[fully faithful functors]] by assumption, these are ([[comodal operator|co-]])[[modal operators]] (Def. \ref{ModalOperator}) on the [[cohesive topos]], by (Prop. \ref{ModalOperatorsEquivalentToReflectiveSubcategories}).

We pronounce these as follows:

\begin{tabular}{l|l|l}
$\phantom{A}$ [[fermionic modality]] $\phantom{A}$&$\phantom{A}$ [[bosonic modality]] $\phantom{A}$&$\phantom{A}$ [[rheonomy modality]] $\phantom{A}$\\
\hline 
$\phantom{A}$ $\rightrightarrows \;\coloneqq\; \iota_{sup} \circ even$ $\phantom{A}$&$\phantom{A}$ $\rightsquigarrow \;\coloneqq\; \iota_{sup} \circ \Pi_{sup}$ $\phantom{A}$&$\phantom{A}$ $Rh \;\coloneqq\; Disc_{sup} \circ \Pi_{sup}$ $\phantom{A}$\\
\end{tabular}

and we refer to the corresponding [[modal objects]] (Def. \ref{ModalObjects}) as follows:

\begin{itemize}%
\item a $\rightsquigarrow$-[[comodal object]]

\begin{displaymath}
\overset{\rightsquigarrow}{X}
    \underoverset{\simeq}{\epsilon^\rightsquigarrow_X}{\longrightarrow}
  X
\end{displaymath}
is called a \emph{[[bosonic object]]};


\item a $Rh$-[[modal object]]

\begin{displaymath}
X
    \underoverset{\simeq}{ \eta^{Rh}_X}{\longrightarrow}
  Rh X
\end{displaymath}
is called a \emph{rheonomic object};



\end{itemize}
\end{defn}
\begin{prop}
\label{ProgressionOfModalitiesOnSolidTopos}\hypertarget{ProgressionOfModalitiesOnSolidTopos}{}
\textbf{(progression of [[adjoint modalities]] on [[solid topos]])}

Let $\mathbf{H}$ be a [[solid topos]] (Def. \ref{SuperDifferentialCohesion}) and consider the [[adjoint modalities]] which it inherits

\begin{enumerate}%
\item for being a [[cohesive topos]], from Def. \ref{CohesiveModalities},


\item for being an [[elastic topos]], from Def. \ref{DiffCohesiveModalities},


\item for being a [[solid topos]], from Def. \ref{SuperDiffCohesiveModalities}:



\end{enumerate}
\begin{tabular}{l|l|l}
$\phantom{A}$ [[shape modality]] $\phantom{A}$&$\phantom{A}$ [[flat modality]] $\phantom{A}$&$\phantom{A}$ [[sharp modality]] $\phantom{A}$\\
\hline 
$\phantom{A}$ $&#643; \;\coloneqq\; Disc \Pi$ $\phantom{A}$&$\phantom{A}$ $\flat \;\coloneqq\; Disc \circ \Gamma$ $\phantom{A}$&$\phantom{A}$ $\sharp \;\coloneqq\; coDisc \circ \Gamma$ $\phantom{A}$\\
&&\\
$\phantom{A}$ \textbf{[[reduction modality]]} $\phantom{A}$&$\phantom{A}$ \textbf{[[infinitesimal shape modality]]} $\phantom{A}$&$\phantom{A}$ \textbf{[[infinitesimal flat modality]]} $\phantom{A}$\\
$\phantom{A}$ $\Re \;\coloneqq\; \iota_{sup} \iota_{inf} \circ \Pi_{inf}\Pi_{sup}$ $\phantom{A}$&$\phantom{A}$ $\Im \;\coloneqq\; Disc_{sup} Disc_{inf} \circ \Pi_{inf} \Pi_{sup}$ $\phantom{A}$&$\phantom{A}$ $\& \;\coloneqq\; Disc_{sup} Disc_{inf} \circ \Gamma_{inf}\Gamma_{sup}$ $\phantom{A}$\\
&&\\
$\phantom{A}$ \textbf{[[fermionic modality]]} $\phantom{A}$&$\phantom{A}$ \textbf{[[bosonic modality]]} $\phantom{A}$&$\phantom{A}$ \textbf{[[rheonomy modality]]} $\phantom{A}$\\
$\phantom{A}$ $\rightrightarrows \;\coloneqq\; \iota_{sup} \circ even$ $\phantom{A}$&$\phantom{A}$ $\rightsquigarrow \;\coloneqq\; \iota_{sup} \circ \Pi_{sup}$ $\phantom{A}$&$\phantom{A}$ $Rh \;\coloneqq\; Disc_{sup} \circ \Pi_{sup}$ $\phantom{A}$\\
\end{tabular}

Then these arrange into the following progression, via the [[preorder]] on modalities from Def. \ref{PreorderOnModalities}:

\begin{displaymath}
\itexarray{    
    id &\dashv& id
    \\
    \vee && \vee
    \\
    \rightrightarrows &\dashv& \rightsquigarrow &\dashv& Rh
    \\
    && \vee && \vee
    \\
    && \Re &\dashv& \Im &\dashv& \&
    \\
    && && \vee && \vee
    \\
    && && &#643; &\dashv& \flat &\dashv& \sharp
    \\
    && && && \vee && \vee
    \\
    && && && \emptyset &\dashv& \ast
  }
\end{displaymath}
where we are displaying, for completeness, also the [[adjoint modalities]] at the [[bottom]] $\emptyset \dashv \ast$ and the [[top]] $id \dashv id$ (Example \ref{InitialAndFinalAdjointModality}).

\end{prop}
\begin{proof}
By Prop. \ref{ProgressionOfModalitiesOnElasticTopos}, it just remains to show that for all [[objects]] $X \in \mathbf{H}$

\begin{enumerate}%
\item $\Im X$ is an $Rh$-[[modal object]], hence $Rh \Im X \simeq X$,


\item $\Re X$ is a [[bosonic object]], hence $\overset{\rightsquigarrow}{\Re X} \simeq \Re X$.



\end{enumerate}
The proof is directly analogous to that of Prop. \ref{ProgressionOfModalitiesOnElasticTopos}, now using the decompositions from Lemma \ref{ProgressionOfSubcategoriesOfSolidTopos}:

\begin{displaymath}
\begin{aligned}
    Rh \Im 
    & =
    Disc_{sup} 
    \underset{
      \simeq id
    }{
    \underbrace{
      \Pi_{sup} \;\; Disc_{sup}
    } 
    }
    Disc_{inf} \Pi_{inf} \Pi_{sup}
    \\
    & \simeq 
    Disc_{sup} Disc_{inf} \Pi_{inf} \Pi_{sup}
    \\
    & = \Im
  \end{aligned}
\end{displaymath}
and

\begin{displaymath}
\begin{aligned}
    \rightsquigarrow \Re
    & =
    \iota_{sup} 
    \underset{\simeq id}{\underbrace{
    \Pi_{sup} \;\; \iota_{sup}}}
    \iota_{inf} \Pi_{inf}\Pi_{sub}
    \\
    & \simeq
    \iota_{sup} \iota_{inf} \Pi_{inf} \Pi_{sub}    
    \\
    & \simeq \Re
  \end{aligned}
\end{displaymath}
\end{proof}
(\ldots{})



\end{document}