\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*{De Morgan topos} \hypertarget{context}{}\subsubsection*{{Context}}\label{context} \hypertarget{category_theory}{}\paragraph*{{Category theory}}\label{category_theory} [[!include category theory - contents]] \hypertarget{topos_theory}{}\paragraph*{{Topos Theory}}\label{topos_theory} [[!include topos theory - contents]] \hypertarget{contents}{}\section*{{Contents}}\label{contents} \noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak \noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak \noindent\hyperlink{examples}{Examples}\dotfill \pageref*{examples} \linebreak \noindent\hyperlink{some_equivalent_formulations}{Some equivalent formulations}\dotfill \pageref*{some_equivalent_formulations} \linebreak \noindent\hyperlink{properties}{Properties}\dotfill \pageref*{properties} \linebreak \noindent\hyperlink{de_morganization}{De Morganization}\dotfill \pageref*{de_morganization} \linebreak \noindent\hyperlink{the_gleason_cover}{The Gleason cover}\dotfill \pageref*{the_gleason_cover} \linebreak \noindent\hyperlink{relation_to_cohesion}{Relation to cohesion}\dotfill \pageref*{relation_to_cohesion} \linebreak \noindent\hyperlink{relation_to_model_theory}{Relation to model theory}\dotfill \pageref*{relation_to_model_theory} \linebreak \noindent\hyperlink{related_entries}{Related entries}\dotfill \pageref*{related_entries} \linebreak \noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak \hypertarget{idea}{}\subsection*{{Idea}}\label{idea} A \textbf{De Morgan topos} $\mathcal{E}$ is a middle thing between a [[Boolean topos]] with a [[classical logic|classical internal logic]] and a general [[topos]] with an [[intuitionistic logic|intuitionistic internal logic]], in that the lattices of [[subobjects]] in $\mathcal{E}$ obey a weak form of the [[law of excluded middle]] which defines a [[De Morgan Heyting algebra]]. The de Morgan property has many equivalent formulations and many facets making the class of de Morgan toposes an important one in [[topos theory]]. From the perspective on toposes as generalized spaces they correspond to \emph{extremally disconnected spaces} in [[topology]]. \hypertarget{definition}{}\subsection*{{Definition}}\label{definition} A topos $\mathcal{E}$ is called a \textbf{De Morgan topos} if its [[subobject classifier]] $\Omega$ is an internal [[De Morgan Heyting algebra]]. \hypertarget{examples}{}\subsection*{{Examples}}\label{examples} \begin{itemize}% \item Every [[Boolean topos]] is a De Morgan topos. \item A simple example of a topos that is De Morgan but not Boolean is the [[Sierpinski topos]] $Set^{\to}$ the [[arrow category]] of $Set$: the diagram category $\to$ is easily seen to satify the [[Ore condition]] (cf. \hyperlink{presheaf-deMorgan}{below}). \item The topos $Sh(X)$ of sheaves on a topological space $X$ is De Morgan precisely iff $X$ is [[extremally disconnected topological space|extremally disconnected]], i.e. the closure of every open subset is open. (Since $Set^{\to}$ is equivalently the topos of sheaves on [[Sierpinski space]] it instantiates this case as well.) \item [[injective topos|Injective Grothendieck toposes]] are De Morgan (cf. \hyperlink{Johnstone}{Johnstone 2002, p.739}). \end{itemize} \hypertarget{some_equivalent_formulations}{}\subsection*{{Some equivalent formulations}}\label{some_equivalent_formulations} The importance of the concept of a De Morgan topos stems partly from the fact that for many statements whose classical (Boolean) validity is lost in intuitionistic logic the De Morgan property delineates precisely the range of toposes where the statement is valid. An illustration of this is e.g. the implication that maximal ideals are prime in commutative rings. Though such statements are in fact equivalent to the De Morgan property they are better viewed as higher-order properties of De Morgan toposes. In contrast, there exists also a long list, mostly due to \hyperlink{Johnstone79}{Johnstone (1979)}, of statements equivalent to the De Morgan property, that are logically of the same complexity and are often more convenient to work with than the original definition. Some of the most important of these appear in the following: \begin{prop} \label{deMorgan_equivalents}\hypertarget{deMorgan_equivalents}{} Let $\mathcal{E}$ be a topos. The following are equivalent: \begin{itemize}% \item $\mathcal{E}$ is a De Morgan topos. \item For all formulae $\varphi,\psi$ : $\mathcal{E}\models \neg (\varphi\wedge\psi)\Leftrightarrow(\neg\varphi\vee\neg\psi)$ . \item For every formula $\varphi$ : $\mathcal{E}\models \neg\varphi\vee\neg\neg\varphi$. \item For every subobject $X\rightarrowtail Y$: $\neg X\vee\neg\neg X=Y$. \item $Sub(X)$ is a De Morgan Heyting algebra for every $X\in\mathcal{E}$. \item The canonical monomorphism $(\top,\bot):1\coprod 1\rightarrowtail\Omega_{\neg\neg}$ to the subobject classifier of $Sh_{\neg\neg}(\mathcal{E})$ is an isomorphism. \item $\Omega_{\neg\neg}$ is [[decidable object|decidable]]. \item $1\coprod 1$ is a retract of $\Omega_{\neg\neg}$. \item $1\coprod 1$ is [[injective object|injective]]. \item Every $\neg\neg$-sheaf is decidable. \item $\bot:1\to\Omega$ has a [[complement]]. \end{itemize} \end{prop} The first few equivalences are based mainly on the validity of the ``law of excluded middle'' for elements of the form $\neg a$ in any [[De Morgan Heyting algebra]]. For the rest see e.g. \hyperlink{Johnstone}{Johnstone (2002, pp.999-1000)}. \hypertarget{properties}{}\subsection*{{Properties}}\label{properties} The following shows that `being De Morgan' is a \emph{local property} i.e. stable under slicing. This is immediate from the fact that the functor $\mathcal{E}\to\mathcal{E}/A$ sending $X$ to the projection $p_A: X\times A\to A$ is [[logical functor|logical]] hence preserves the various equivalent formulations of De Morgan's law. \begin{prop} \label{local_property}\hypertarget{local_property}{} Let $A$ be an object of the De Morgan topos $\mathcal{E}$. Then the [[slice topos]] $\mathcal{E}/A$ is De Morgan as well. \end{prop} \begin{prop} \label{presheaf-deMorgan}\hypertarget{presheaf-deMorgan}{} Let $\mathcal{C}$ be a small category. The [[presheaf topos]] $Set^{\mathcal{C}^{op}}$ is De Morgan precisely if $\mathcal{C}$ satifies the [[Ore condition]]. \end{prop} This result due to [[Peter Johnstone]] appears e.g. in \hyperlink{Johnstone79}{Johnstone (1979)}. Compare also the generalizations in \hyperlink{KR94}{Kock-Reyes (1994)} and \hyperlink{Caramello12}{Caramello (2012)}. Since the [[dense topology]] coincides with the [[atomic site|atomic topology]] on $\mathcal{C}$ satisfying the Ore condition the preceding proposition implies that the [[double negation|double negation subtopos]] of a De Morgan presheaf topos $Set^{\mathcal{C}^{op}}$ is always [[atomic topos|atomic]]. \hypertarget{de_morganization}{}\subsubsection*{{De Morganization}}\label{de_morganization} It was discovered by [[Olivia Caramello]] that every topos $\mathcal{E}$ can be associated with a De Morgan topos $Sh_m(\mathcal{E})$, its [[De Morganization]], in a universal way: \begin{prop} \label{largest_deMorgan}\hypertarget{largest_deMorgan}{} Given a topos $\mathcal{E}$. There exists a unique largest [[dense subtopos]] $Sh_m(\mathcal{E})$ of $\mathcal{E}$ that is a De Morgan topos. \end{prop} For a proof see \hyperlink{Caramello09}{Caramello (2009)}. The $m$ that occurs here, refers to the \emph{De Morgan topology} , cf. [[De Morganization]]. As $Sh_{\neg\neg}(\mathcal{E})$, the sheaf subtopos for the [[double negation|double negation topology]] $\neg\neg$ , is the \emph{smallest} dense De Morgan subtopos, we see that all dense De Morgan subtoposes lie in the interval between $Sh_{\neg\neg}(\mathcal{E})$ and $Sh_{m}(\mathcal{E})$. In analogy with [[skeletal geometric morphism|skeletal geometric morphisms]] that preserve $\neg\neg$-sheaves, geometric morphisms $\mathcal{F}\to\mathcal{E}$ that map $m$-sheaves in $\mathcal{F}$ to $m$-sheaves in $\mathcal{E}$ are called $m$\emph{-skeletal}. They occur in the following characterization of De Morgan toposes (cf. [[De Morganization]]): \begin{prop} \label{deMorgan_m-skeletal}\hypertarget{deMorgan_m-skeletal}{} A topos $\mathcal{E}$ is De Morgan iff every geometric morphism $\mathcal{F}\to\mathcal{E}$ is $m$-skeletal. $\qed$ \end{prop} \hypertarget{the_gleason_cover}{}\subsubsection*{{The Gleason cover}}\label{the_gleason_cover} Another way to associate a De Morgan topos to an arbitrary topos $\mathcal{E}$ was proposed by [[Peter Johnstone]] in the late 70s (Johnstone \hyperlink{Johnstone79b}{1979b}, \hyperlink{J80}{1980}). The so called \emph{Gleason cover} $\gamma\mathcal{E}$ of $\mathcal{E}$ generalizes a construction in [[topology]] that covers an arbitrary [[space]] by an extremally disconnected topological space. \ldots{}\ldots{} \hypertarget{relation_to_cohesion}{}\subsubsection*{{Relation to cohesion}}\label{relation_to_cohesion} Given that the \hyperlink{deMorgan_equivalents}{above conditions} concern $1\coprod 1$ and the contractability of $\Omega_{\neg\neg}$ it comes as no surprise that the De Morgan property interacts interestingly with [[Lawvere|Lawvere's]] axiomatic approach to [[cohesion]] and, in particular, with the part of it that concerns the connectedness of the subobject classifier in a cohesive topos of spaces. A first indication of this is the following: \begin{prop} \label{omega_connected}\hypertarget{omega_connected}{} Let $Set^{\mathcal{C}^{op}}$ be a [[presheaf topos]]. Then its [[subobject classifier]] is connected iff $1\in Set^{\mathcal{C}^{op}}$ is a [[connected]] object and $Set^{\mathcal{C}^{op}}$ is not de Morgan iff there exists a connected object $X\in Set^{\mathcal{C}^{op}}$ such that $1\coprod 1\rightarrowtail X$ . \end{prop} This result appears in \hyperlink{RZZZ04}{La Palme-Reyes-Reyes-Zolfaghari (2004, p.220)} where it is attributed to [[Lawvere]]. The following result due to \hyperlink{Mielke84}{Mielke (1984)} shows that the De Morgan property coincides with the (local) absence of a non-trivial [[interval object|interval objects]] in a topos. Here by an interval object we mean an internal linearly ordered object $I$ with disjoint least and greatest elements $m:1\to I$ and $M:1\to I$, respectively, i.e. roughly the sort of thing that is classified by [[sSet]]. An interval object is \emph{trivial} if $I\simeq I_1\coprod I_2$ and $m,M$ factor through $I_1,I_2$, respectively. A topos $\mathcal{E}$ is said to be \textbf{homotopically trivial} if every interval object in $\mathcal{E}$ is trivial, $\mathcal{E}$ is said to \emph{locally homotopically trivial} if the [[slice topos]] $\mathcal{E}/X$ is homotopically trivial for all $X\in\mathcal{E}$. \begin{prop} \label{deMorgan_interval}\hypertarget{deMorgan_interval}{} A topos $\mathcal{E}$ is locally homotopically trivial iff $\mathcal{E}$ is a De Morgan topos. If subobjects of $1$ generate, then $\mathcal{E}$ is homotopically trivial iff $\mathcal{E}$ is a De Morgan topos. \end{prop} For situations where subobjects of $1$ generate see e.g. \hyperlink{Johnstone77}{Johnstone (1977, sec.5.3 pp.145ff)}. For a [[Grothendieck topos]] $\mathcal{E}$, this happens precisely when $\mathcal{E}$ is equivalent to $Sh(L)$ for some [[locale]] $L$. From e.g. \hyperlink{Borceux94}{Borceux (1994, p.443)} it follows then that $Sh(L)$ \emph{is homotopically trivial} precisely when $L$ is a \emph{De Morgan locale}. \hypertarget{relation_to_model_theory}{}\subsubsection*{{Relation to model theory}}\label{relation_to_model_theory} \ldots{}. \begin{prop} \label{model_companion}\hypertarget{model_companion}{} Let $\mathcal{T}$ be a coherent theory. Then $\mathcal{T}$ admits a [[model companion]] and $Mod(\mathcal{T})$ has the [[amalgamation property]] iff for each $B\in\mathcal{T}$ , the lattice of subobjects of $B$ admits a negation satisfying $\neg A\vee\neg\neg A = B$. \end{prop} This result appears without proof in \hyperlink{Harun96}{Harun (1976, p.73)} where it is attributed to a preprint of [[André Joyal]] and [[Gonzalo E. Reyes]]. \hypertarget{related_entries}{}\subsection*{{Related entries}}\label{related_entries} \begin{itemize}% \item [[De Morganization]] \item [[De Morgan Heyting algebra]] \item [[Ore condition]] \item [[double negation]] \item [[Boolean topos]] \item [[law of excluded middle]] \item [[skeletal geometric morphism]] \end{itemize} \hypertarget{references}{}\subsection*{{References}}\label{references} \begin{itemize}% \item A. Bagchi, \emph{De Morgan's law and related identities in classifying topoi} , Proc. CT91 pp.1-32, American Mathematical Society 1992. \item A. Bagchi, \emph{Lee Identities in Topoi I} , JPAA \textbf{120} (1997) pp.143-159. \item [[Francis Borceux]], \emph{Handbook of Categorical Algebra vol.3} , Cambridge UP 1994. (sections 1.2, 7.3) \item [[Olivia Caramello]], \emph{De Morgan classifying toposes} , Adv. in Math. \textbf{222} (2009) pp.2117-2144. (\href{http://arxiv.org/abs/0808.1519}{arXiv:0808.1519}) \item [[Olivia Caramello]], \emph{Topologies for intermediate logics} , arXiv:1205.2547 (2012). (\href{http://arxiv.org/abs/1205.2547}{arXiv:1205.2547}) \item [[Olivia Caramello]], [[Peter Johnstone]], \emph{De Morgan's law and the Theory of Fields} , Adv. in Math. \textbf{222} (2009) pp.2145-2152. (\href{http://arxiv.org/abs/0808.1572}{arXiv:0808.1572}) \item R. Harun, \emph{Applications of De Morgan toposes and the Gleason cover} , PhD Montr\'e{}al 1996. (\href{http://www.collectionscanada.gc.ca/obj/s4/f2/dsk2/ftp04/mq29711.pdf}{pdf 4.6MB}) \item [[Peter Johnstone]], \emph{Topos Theory} , Academic Press New York 1977. (Dover reprint New York 2014, exercise 5.5.3 p.162) \item [[Peter Johnstone]], \emph{Conditions Related to De Morgan's Law} , pp.479-491 in LNM \textbf{753} Springer Heidelberg 1979. \item [[Peter Johnstone]], \emph{Another Condition Equivalent to De Morgan's Law} , Comm. Alg. \textbf{7} (1979) pp.1309-1312. \item [[Peter Johnstone]], \emph{The Gleason Cover of a Topos I} , JPAA \textbf{19} (1980) pp.171-192. \item [[Peter Johnstone]], \emph{The Gleason Cover of a Topos II} , JPAA \textbf{22} (1981) pp.229-247. \item [[Peter Johnstone]], \emph{[[Sketches of an Elephant]] vol. II}, Oxford UP 2002. (section D4.6, pp.998ff) \item [[Peter Johnstone]], \emph{The Gleason Cover of a Realizability Topos} , TAC \textbf{28} no.32 (2013) pp.1139-1152. (\href{http://www.tac.mta.ca/tac/volumes/28/32/28-32abs.html}{abstract}) \item [[Anders Kock]], [[Gonzalo E. Reyes]], \emph{Relatively Boolean and De Morgan Toposes and Locales} , Cah. Top. G\'e{}om. Diff. Cat. \textbf{35} no.3 (1994) pp.249-261. (\href{http://www.numdam.org/numdam-bin/item?id=CTGDC_1994__35_3_249_0}{numdam}) \item [[William Lawvere]], [[Matías Menni]], \emph{Internal choice holds in the discrete part of any cohesive topos satisfying stable connected codiscreteness} , TAC \textbf{30} no.26 (2015) pp.909-932. (\href{http://www.tac.mta.ca/tac/volumes/30/26/30-26abs.html}{abstract}) \item K. B. Lee, \emph{Equational Classes of Distributed Pseudo-Complemented Lattices} , Can. J. Math. \textbf{22} (1970) pp.881-891. (\href{http://cms.math.ca/openaccess/cjm/v22/cjm1970v22.0881-0891.pdf}{pdf}) \item B. Loiseau, M.-M. Mawanda, \emph{On Natural Number Objects, Finiteness and Kripke-Platek Models in Toposes} , JPAA \textbf{61} (1989) pp.257-266. \item M.-M. Mawanda, \emph{Well-ordering and Choice in Toposes} , JPAA \textbf{50} (1988) pp.171-184. \item M. V. Mielke, \emph{Homotopically Trivial Toposes} , Pacific J. Math. \textbf{110} no.1 (1984) pp.171-182. (\href{https://projecteuclid.org/euclid.pjm/1102711108}{euclid}) \item M. V. Mielke, \emph{Topos based homology theory} , Comment. Math. Univ. Carolinae \textbf{34} (1993) pp.549-565. (\href{http://www.kurims.kyoto-u.ac.jp/EMIS/journals/CMUC/pdf/cmuc9303/mielke.pdf}{pdf}) \item [[Chris Mulvey]], \emph{The Maximality of Filters} , JPAA \textbf{68} (1990) pp.253-258. \item M. La Palme Reyes, [[Gonzalo E. Reyes|G. E. Reyes]], H. Zolfaghari, \emph{Generic Figures and their Glueings} , Polimetrica Milano 2004. \item M. E. Szabo, \emph{Categorical De Morgan laws} , Alg. Universalis \textbf{12} (1981) pp.93-102. \end{itemize} [[!redirects De Morgan topos]] [[!redirects de Morgan topos]] [[!redirects De Morgan topoi]] [[!redirects de Morgan topoi]] [[!redirects De Morgan toposes]] [[!redirects de Morgan toposes]] [[!redirects DeMorgan topos]] [[!redirects demorgan topos]] [[!redirects De Morgan Topos]] [[!redirects De Morganization]] [[!redirects De Morganisation]] [[!redirects De Morganizations]] [[!redirects De Morganisations]] \end{document}