nLab sufficiently cohesive topos

Idea

A sufficiently cohesive topos is a cohesive topos that has enough connected objects in the sense that every object embeds into a connected object.

This can be viewed as a strong form of cohesiveness in the context of Lawvere's axiomatic approach to gros toposes. In fact, in Lawvere (1986) a big topos of spaces was defined as (one equivalent to) a sufficiently cohesive topos.

Terminology

Sufficient cohesion is a relative concept and requires minimally the presence of an essential geometric morphism $p:\mathcal{E}\to\mathcal{S}$. Here we state it for an adjoint quadruple between toposes

$$p_!\dashv p^* \dashv p_* \dashv p^!\;\colon\;\mathcal{S}\to\mathcal{E}$$

such that $p^!$ (and hence $p^\ast$) is fully faithful and $p_!$ preserves finite products.

This (and $\mathcal{E}$ in particular) is called a ‘cohesive topos’ (over $\mathcal{S}$) at cohesive topos, and will be referred to as a ‘weakly cohesive topos’ in the present entry - a sufficiently cohesive topos in this context corresponds to the three axioms (0-2) for a ‘gros topos’ in Lawvere (1986) where the concept of sufficient cohesion was considered for the first time.

A weakly cohesive topos is called pre-cohesive if $p$ furthermore satisfies the Nullstellensatz i.e. the canonical map $\theta:p_\ast\to p_!$ is an epimorphism. This is the situation explored in Menni (2014a, 2014b).

A pre-cohesive topos that moreover satisfies the continuity principle that $p_!(X^{p^\ast(Y)})\simeq p_!(X)^{Y}$ natural in $X\in\mathcal{E}$, $Y\in\mathcal{S}$, is called ‘cohesive’ in Lawvere (2007) where the term ‘sufficently cohesive’ occurs for the first time although the notion is defined in a more restricted environment than the earlier papers (cf. Lawvere 1986, 1992, 1999).

Definitions

Definition

An object $X$ in a weakly cohesive topos $p:\mathcal{E}\to\mathcal{S}$ is called contractible if for every object $Y\in\mathcal{E}$: $p_!(X^Y)=1$.

Remark

In particular, a contractible object is connected: $p_!(X)=p_!(X^1)=1$. Since exponentiation $(-)^Y$ preserves $1$ in any Cartesian closed category, the terminal object is contractible in any weakly cohesive topos.

Definition

A weakly cohesive topos $p:\mathcal{E}\to\mathcal{S}$ is called sufficiently cohesive if the subobject classifier $\Omega\in\mathcal{E}$ is contractible i.e. $p_!(\Omega^X)=1$ for every object $X\in\mathcal{E}$ or, in other words, if all power objects are connected.

Remark

Since in general, every object $X$ embeds into its power object via the singleton map $\{\}:X\rightarrowtail\Omega^X$ it follows that in a sufficiently cohesive topos $\mathcal{E}$ every object embeds into a connected object i.e. $\mathcal{E}$ has enough connected objects.

Furthermore, since in a Cartesian closed category

$$(X^Y)^Z\simeq X^{(Y\times Z)}\simeq X^{(Z\times Y)}\simeq (X^Z)^Y$$

one sees that in a sufficiently cohesive topos power objects $\Omega^X$ are not only connected but even contractible:

$$p_!((\Omega^X)^Z)=p_!(\Omega^{X\times Z})=1$$

and hence it follows that in a sufficiently cohesive topos every object embeds into a contractible object.

Conversely, if every power object $\Omega^X$ embeds into a connected object then the power objects $\Omega^X$ will be connected themselves by proposition below since power objects are injective in general. Whence a (weakly) cohesive topos is sufficiently cohesive iff every object embeds into a connected object iff every object embeds into a contractible object. The last formulation is taken as the definition of sufficient cohesion in Lawvere (2007).

Remark

The definition of sufficient cohesion by ‘having enough contractible objects’ (Lawvere 2007) has of course the advantage that it even works in the wider context of Cartesian closed extensive categories that lack a subobject classifier. The definition by ‘having enough connected objects’ would be feasible for merely distributive categories that are not necessarily Cartesian closed (cf. Lawvere 1991, 1992) but Lawvere (1991, p.4) suggests that in this case the definition should be strenghtened to demand that every object is the equaliser of a pair of maps between two connected objects.

Properties

Let us first record some easy but useful facts concerning the interplay between connectedness and constancy.

Recall that in a category with a terminal object a morphism $c:X\to Y$ is called constant if $c$ factors through the terminal object $1$:

$$X\overset{c}{\to} Y=X\overset{!_X}{\to}1\overset{c_\ast}{\to} Y\quad .$$

Observation

An object $X$ is a terminal object iff $id_X$ is constant.

Proof. “$\Leftarrow$”: By assumption $id_X=(id_X)_\ast\circ !_X$. Since $X$ has a point $(id_X)_\ast$ there exists for every object $Z$ at least one map $Z\to X$. Suppose then that $f$ is some map $Z\to X$:

$$f=id_X\circ f=(id_X)_\ast\circ !_X\circ f=(id_X)_\ast\circ !_Z\quad .$$

But the righthand side does not depend on $f$ hence it is the only map $Z\to X$. $\qed$

Observation

Let $X$ be an object in a weakly cohesive topos and $c:X\to X$ be a constant endomap such that $p_!(c)=p_!(id_X)$. Then $X$ is connected i.e. $p_!(X)=1$.

Proof. Since by assumption $p_!(1)=1$, $p_!(c)$ and, accordingly, $p_!(id_X)=id_{p_!(X)}$ are constants. $\qed$

Observation

In a weakly cohesive topos, retracts of connected objects are connected themselves.

Proof. Let $X$ be a retract of $Y$ with $p_!(Y)=1$. Then $id_X$ factors as $X\rightarrowtail Y\to X$ and applying $p_!$ shows that $id_{p_!(X)}$ factors through the terminal object $p_!(Y)$. $\qed$

Since in general, injective objects $I$ are retracts of the objects $X$ that they embed into because such inclusions $I\rightarrowtail X$ factor through $id_I$ by injectivity, it follows that in a weakly cohesive topos injective objects that embed into a connected object are connected themselves.

In particular, all injective objects are connected in a sufficiently cohesive topos. Since power objects are injective in general one gets the converse as well:

Proposition

A weakly cohesive topos is sufficiently cohesive iff all injective objects are connected. $\qed$

We can replace ‘connected’ with ‘contractible’ in this proposition as the following propositions show.

Proposition

Let $\mathcal{E}$ be a topos. Then all injective objects are connected iff all injective objects are contractible.

Proof. “$\Rightarrow$”: by the following lemma. $\qed$

Lemma

Let $I$ be an injective object in a topos $\mathcal{E}$. Then $I^X$ is injective for any object $X$ , or in other words, exponentials $(_-)^X$ preserve injective objects.

Proof. (cf. at injective object) We have to show that for every mono $m:S\rightarrowtail B$ the induced function $m^\ast:Hom(B,I^X)\to Hom(S,I^X)$ is onto. From the exponential adjunction one has the following commutative diagram

$$\array{ Hom(B,I^X) &\overset{m^\ast}{\rightarrow} & Hom(S,I^X) \\ \simeq \parallel& &\parallel \simeq \\ Hom(X\times B,I) &\underset{(m\times id_X)^\ast}{\rightarrow} &Hom(X\times S,I) }$$

whence it suffices to show that $m\times id_X:S\times X\to B\times X$ is a mono since $I$ is injective. But this is easy to see:

$$\begin{aligned} (m\times id_X)\circ \langle f_1,f_2\rangle &= (m\times id_X)\circ\langle g_1,g_2\rangle \\ \langle m\circ f_1, f_2\rangle &=\langle m\circ g_1,g_2\rangle \end{aligned}$$

which is equivalent to $\m\circ f_1=m\circ g_1$ and $f_2=g_2$. $\qed$

Summing up we get:

Proposition

A weakly cohesive topos $\mathcal{E}$ is sufficiently cohesive iff all injective objects are contractible. $\qed$

Cohesively connected truth

In a sufficiently cohesive topos the subobject classifier is obviously connected since $\Omega=\Omega^1$. It is the aim of this section to prove that in a weakly cohesive topos the converse holds as well: $\Omega$ is connected iff $\Omega$ is contractible.

Before embarking on a proof let us consider two non-examples that display varied behaviors in respect to the connectedness of the subobject classifier and the exactness properties of the components functor $p_!$:

Example

The Sierpinski topos $Set^\to$ is weakly cohesive over $Set$ since there exists a string of adjoint functors $L\dashv\Pi\dashv\Delta\dashv\Gamma\dashv B: Set\to Set^\to$ with

• $L(Z)=\emptyset \to Z$

• $\Pi(X\to Y) = Y$

• $\Delta(Z)=Z\overset{id}{\to} Z$

• $\Gamma (X\to Y) = X$

• $B(Z)=Z\to 1$.

The Nullstellensatz fails as does the continuity principle. As a right adjoint $\Pi$ preserves all limits and the terminal object in particular whence $1$ is connected in $Set^\to$. Since the underlying category $\to$ satisfies the Ore condition trivially, it follows then from a general result¹ of Lawvere that $\Omega$ is not connected and, accordingly, that the Sierpinski topos is not sufficiently cohesive!

Example

On the other hand, consider the topos of directed graphs $Set^\rightrightarrows$: it lacks the right adjoint $p^!$ to the section functor $p_*$ but has a connected components functor $p_!$ and the subobject classifier for directed graphs $\Omega$ is connected.

Although $p_!$ does not preserve finite products in general, it nevertheless preserves finite products with the subobject classifier $\Omega$ since $\Omega$ has arcs between all nodes in both directions. This implies that the proof of proposition below still goes through and since this is the only argument that hinges on exactness properties of $p_!$ and nothing hinges on (the existence of) the right adjoint $p^!$ at all, the conclusions from hold as well: the subobject classifier of $Set^\rightrightarrows$ is not only connected but contractible! In other words, despite not being sufficiently cohesive $Set^\rightrightarrows$ nevertheless has enough contractible objects.

Recall that in any topos, the subobject classifier $\Omega$ has two points $\mathsf{true},\mathsf{false}$ fitting into the following pullback diagram (which is an equaliser diagram as well) due to the classifying property of $\Omega$ for the monomorphism $0\to 1$:

$$\array{ 0 &\to & 1 \\ \downarrow & &\downarrow\mathsf{true} \\ 1 &\underset{\mathsf{false}}{\to} &\Omega }$$

In a sufficiently cohesive topos $\Omega$ is furthermore connected whence together with its Heyting algebra structure we can view it as a generalized (non linear) “interval” object:

Definition

An object $T$ in a weakly cohesive topos is called a (cohesive) connector if $p_!(T)=1$ and $T$ has two points $t_0,t_1:1\to T$ with empty equaliser: $0\overset{e}{\to} 1\overset{t_0}{\underset{t_1}{\rightrightarrows}} T$.

In a topos with a connected subobject classifier $\Omega$ itself is a connector. Conversely the existence of a connector implies the connectedness of $\Omega$:

Proposition

Let $\mathcal{E}$ be weakly cohesive topos. $\mathcal{E}$ has a connector $T$ iff $p_!(\Omega)=1$.

Proof. “$\Rightarrow$”: Let $1\overset{t_0}{\underset{t_1}{\rightrightarrows}} T$ be a connector. Then $t_1:1\to T$ is a subobject with characteristic map $\chi_1:T\to\Omega$. Consider the two composites $\chi_1\circ t_i$ , $i=0,1$:

For $i=1$ this simply yields $\mathsf{true}$ by the definition of $\chi_1$.

For $i=0$ we claim that $\chi_1\circ t_0=\mathsf{false}$ since we have the following diagram:

$$\array{ 0 &\to & 1 &\to & 1 \\ \downarrow & &t_1\downarrow& & \downarrow \mathsf{true} \\ 1&\underset{t_0}{\to} &T&\underset{\chi_1}{\to}&\Omega }$$

Here the left square is a pullback since $t_o,t_1$ have empty equaliser by assumption. The right square is a pullback since it classifies $t_1$ whence the outer square is a pullback too. Therefore $\chi_1\circ t_0$ classifies $0\to 1$ which is exactly the definition of $\mathsf{false}$.

Since $p_!(T)$ is terminal $p_!(t_0)=p_!(t_1)$. Whence

$$p_!(\mathsf{true})=p_!(\chi_1\circ t_1)=p_!(\chi_1)\circ p_!(t_1)=p_!(\chi_1)\circ p_!(t_0)=p_!(\chi_1\circ t_0)=p_!(\mathsf{false})\quad$$

This says that $\mathsf{true}$ and $\mathsf{false}$ are in the same connected component but a lattice whose top and bottom elements are in the same component is necessarily connected. $\qed$

One can use connectors to define a (generalized) homotopy relation between maps that behaves well under taking connected components.

Definition

Let $I$ be a connector. Two parallel maps $f,g:A\to B$ are called I-homotopic, in signs: $f\sim_I g$, if there exists a map $h:A\times I\to B$ with the property that

$$f=h\circ\langle id_A, t_0\circ !_A\rangle\quad and\quad g=h\circ\langle id_A, t_1\circ !_A\rangle\quad.$$

(In this case, $h$ is also called an ($I$-)homotopy between $f$ and $g$.)

The following result brings together two ingredients for the equivalence between contractability and connectedness of $\Omega$, namely, the preservation of finite products by $p_!$ and $p_!(\Omega)=1$.

Proposition

Let $f=h\circ\langle i, k_1\rangle$ and $g=h\circ\langle i, k_2\rangle$ be a pair of parallel maps in a weakly cohesive topos with the property that $p_!(k_1)=p_!(k_2)$. Then $p_!(f)=p_!(g)$. In particular, $f\sim_I g$ implies $p_!(f)=p_!(g)$.

Proof. Since $p_!$ preserves finite products it maps product diagrams to product diagrams whence

$$p_!(h\circ\langle i, k_j\rangle)=p_!(h)\circ p_!(\langle i, k_j\rangle)=p_!(h)\circ \langle p_!( i), p_!(k_j)\rangle\quad,\quad j\in\{1,2\}$$

but these two maps coincide since $p_!(k_1)=p_!(k_2)$ by assumption.

Since for an I-homotopy $k_j=t_j\circ !_A:A\to I$ and, $p_!(I)=1$ by assumption, $p_!(k_j):p_!(A)\to 1$, $j\in\{1,2\}$, and these maps necessarily coincide since $1$ is terminal whence $p_!(t_0\circ !_A)=p_!(t_1\circ !_A)$ whence $p_!(f)=p_!(g)$ as claimed. $\qed$

For the following the monoid structure of $\Omega$ will become important. So let us briefly review the basics:

In a general topos, the Heyting algebra structure endows the subobject classifier with the structure of an internal monoid: The multiplication is given by conjunction

$$\Omega\times\Omega\overset{\wedge}{\to}\Omega\quad , \text{ and the unit by }\quad 1\overset{\mathsf{true}}{\to}\Omega\quad .$$

The conjunction $\wedge$ is defined as the characteristic map of $1\xrightarrow{\langle\mathsf{true},\mathsf{true}\rangle}\Omega\times\Omega$.

Importantly, the other truth value $1\xrightarrow{\mathsf{false}}\Omega$ plays the role of a (multiplicative) zero with respect to this multiplication.

For the following we need

Proposition

Let $\mathcal{E}$ be a weakly cohesive topos whose subobject classifier is a connector i.e. $p_!(\Omega)=1$. Then the conjunction $\wedge :\Omega\times\Omega{\to}\Omega$ is an $\Omega$-homotopy from $id_{\Omega}$ to the constant map $\mathsf{false}\circ !_\Omega$.

Proof. We have to show that $\wedge\circ\langle id_\Omega, \mathsf{true}\circ !_\Omega\rangle=id_\Omega$ and $\wedge\circ\langle id_\Omega, \mathsf{false}\circ !_\Omega\rangle=\mathsf{false}\circ !_\Omega$. This is more or less clear from the propositional structure of $\Omega$ but let us spell out the details diagrammatically:

For the first equation, consider the commutative diagram:

$$\array{ 1 &\to & 1 \\ {}_\mathsf{true}\downarrow & &\downarrow_{\langle\mathsf{true},\mathsf{true}\rangle} \\ \Omega &\xrightarrow{\langle id_\Omega,\mathsf{true}\circ !_\Omega\rangle}&\Omega\times\Omega }$$

This pullback pasted to the classifying pullback diagram for $\langle\mathsf{true},\mathsf{true}\rangle$ displays $\wedge\circ\langle id_\Omega, \mathsf{true}\circ !_\Omega\rangle$ as the characteristic map of $\mathsf{true}$ which of course is none other than $id_\Omega$.

For the second, consider the following pullback:

$$\array{ X &\xrightarrow{!_X} & 1 \\ {}_{\mathsf{true}\circ !_X}\downarrow & &\downarrow_{\langle\mathsf{true},\mathsf{true}\rangle} \\ \Omega &\xrightarrow{\langle id_\Omega,\mathsf{false}\circ !_\Omega\rangle }&\Omega\times\Omega }$$

Chasing the arrows around in the second component yields the equation

$$\mathsf{true}\circ !_X=\mathsf{false}\circ !_\Omega\circ\mathsf{true}\circ !_X=\mathsf{false}\circ !_X$$

but this implies $X=0$ since it corresponds to the pullback of $\mathsf{true}$ and $\mathsf{false}$. Hence the pasted

$$\array{ 0 &\xrightarrow{!_0} & 1 &\to & 1 \\ \downarrow & &\downarrow_{\langle\mathsf{true},\mathsf{true}\rangle}& &\downarrow _\mathsf{true} \\ \Omega &\xrightarrow{\langle id_\Omega,\mathsf{false}\circ !_\Omega\rangle }&\Omega\times\Omega&\xrightarrow{\wedge}&\Omega }$$

is the classifying pullback of $0\rightarrowtail\Omega$. Since it is easily seen that $\mathsf{false}\circ !_\Omega$ is also the characteristic map of $0\rightarrowtail\Omega$ the claim follows. $\qed$

In order to show that the connectedness of $\Omega$ implies its contractibility we will now lift this $\Omega$-homotopy between $id_\Omega$ and a constant map $\Omega\to\Omega$ to a $\Omega$-homotopy between $id_{\Omega^X}$ and a constant map $\Omega^X\to\Omega^X$.

Proposition

Let $\mathcal{E}$ be a weakly cohesive topos with connector $1\overset{t_0}{\underset{t_1}{\rightrightarrows}} T$. Suppose that $m:X\times T\to X$ is a $T$-homotopy between $id_X$ and a constant map $c:X\to X\,$.Then there exists for every object $Y$ a $T$-homotopy $\mu:X^Y\times T\to X^Y$ from $id_{X^Y}$ to a constant endomap $X^Y\to X^Y$.

Proof. We get $\mu$ from $X\times T \overset{m}{\to} X$ as follows

$$\begin{aligned} X& \to X^{T}\quad\text{by transposal} \\ X^Y&\to (X^{T})^{Y}\quad\text{by application of the endofunctor (-)}^Y \\ X^Y &\to (X^Y)^{T}\quad\text{by using rules for powers} \\ X^Y\times T&\overset{\mu}{\to}X^Y\quad \text{by reversing transposal .} \end{aligned}$$

The corresponding terms in the internal language are

$$\array{ m=\lambda (x,t).m(x,t) \\ \lambda x\lambda t.m(x,t) \\ \lambda f\lambda y\lambda t. m(f(y),t) \\ \lambda f\lambda t \lambda y. m(f(y),t) \\ \mu =\lambda (f,t)\lambda y. m(f(y),t) }$$

respectively. The last term evaluates to $\lambda f\lambda y.f(y)$ i.e. to $id_{X^Y}$ at $t_0$ and at $t_1$ evaluates to $\lambda f\lambda y.c$ , i.e. the function mapping f to $c^Y$ , the function constantly $c$ on $Y$, whence $\mu$ is a $T$-homotopy from $id_{X^Y}$ to the constantly $c^Y$ map. $\qed$

By prop. and the preceding the next is immediate:

Corollary

Let $\mathcal{E}$ be a weakly cohesive topos whose subobject classifier is a connector. The $\Omega$-homotopy $\wedge :\Omega\times\Omega{\to}\Omega$ lifts to a $\Omega$-homotopy between $id_{\Omega^X}$ and a constant map $\Omega^X\to\Omega^X$. $\qed$

Remark

In classical topology, a space $X$ with the property that $id_X$ is homotopic to a constant map is called a contractible space. Hence proposition can be viewed as a synthetic internal avatar of the classical fact, that any two parallel maps into a contractible space $X$ are homotopic.

Pursuing this analogy, the preceding result shows that in a weakly cohesive topos with connected subobject classifier, the power object $\Omega^X$ of an object $X$ is akin to the cone $\mathbf{C}X$ of a topological space $X$ in providing a contractible object to embed into. In this perspective, one can think of a sufficiently cohesive topos as being equipped with a generalized cone construction.

Theorem

Let $\mathcal{E}$ be a weakly cohesive topos. Then the subobject classifier $\Omega$ is connected iff $\Omega$ is contractible. In other words, $\mathcal{E}$ is sufficiently cohesive iff $p_!(\Omega)=1$.

Proof. “$\Rightarrow$”: The propositions and imply that for all $X$ $p_!(id_{\Omega^X})=id_{p_!(\Omega^X)}$ is a constant map. By observation it then follows that $p_!(\Omega^X)=1$ for all $X$ which is just the definition of $\Omega$ being contractible. $\qed$

For convenience and summary let us collect all the equivalent formulations of sufficient cohesion in one place:

Theorem (Lawvere)

A weakly cohesive topos $\mathcal{E}$ is sufficiently cohesive iff $\mathcal{E}$ satisfies the following equivalent conditions:

• The subobject classifier $\Omega\in\mathcal{E}$ is contractible i.e. $p_!(\Omega^X)=1$ for every object $X\in\mathcal{E}$. ‘power objects are connected’ or ‘truth is contractible’

• The subobject classifier $\Omega\in\mathcal{E}$ is connected i.e. $p_!(\Omega)=1$. ‘truth is connected’

• The subobject classifier $\Omega\in\mathcal{E}$ is a connector. ‘truth is a connector’

• $\mathcal{E}$ has a connector.

• Every object $X\in\mathcal{E}$ embeds into a contractible object. ‘$\mathcal{E}$ has enough contractible objects’

• Every object $X\in\mathcal{E}$ embeds into a connected object. ‘$\mathcal{E}$ has enough connected objects’

• All injective objects are connected.

• All injective objects are contractible. $\qed$

Related entries

• cohesive topos

• Nullstellensatz

• quality type

• Lawvere interval

• connected object

• injective object

References

• P. Johnstone, Remarks on Quintessential and Persistent Localizations , TAC 2 no.8 (1996) pp.90-99. (pdf)

• P. Johnstone, Sketches of an Elephant vol. 1 , Cambridge UP 2002.

• P. Johnstone, Remarks on Punctual Local Connectedness , TAC 25 no.3 (2011) pp.51-63. (pdf)

• M. La Palme Reyes, G. E. Reyes, H. Zolfaghari, Generic Figures and their Glueings , Polimetrica Milano 2004.

• F. W. Lawvere, Categories of Spaces may not be Generalized Spaces as Exemplified by Directed Graphs, Revista Colombiana de Matemáticas XX (1986) pp.179-186. Reprinted with commentary as TAC Reprint 9 (2005) pp.1-7. (pdf)

• F. W. Lawvere, Some Thoughts on the Future of Category Theory , pp.1-13 in Springer LNM 1488 (1991).

• F. W. Lawvere, Categories of Space and Quantity, pp.14-30 in: J. Echeverria et al. (eds.), The Space of Mathematics , de Gruyter Berlin 1992.

• F. W. Lawvere, Kinship and Mathematical Categories , pp.411-425 in: R. Jackendoff, P. Bloom, K. Wynn (eds.), Language, Logic, and Concepts - Essays in Memory of John Macnamara, MIT Press 1999.

• F. W. Lawvere, Axiomatic cohesion , TAC 19 no.3 (2007) pp.41–49. (pdf)

• F. W. Lawvere, M. Menni, Internal choice holds in the discrete part of any cohesive topos satisfying stable connected codiscreteness, TAC 30 no. 26 (2015) pp.909-932. (abstract)

• F. W. Lawvere, R. Rosebrugh, Sets for Mathematics , Cambridge UP 2003.

• F. Marmolejo, M. Menni, On the relation between continuous and combinatorial , arXiv:1602.02826 (2016). (abstract)

• M. Menni, Sufficient Cohesion over Atomic Toposes , Cah. Top. Géom. Diff. Cat. LV (2014). (preprint)

• M. Menni, Continuous Cohesion over Sets , TAC 29 no.20 (2014) pp.542-568. (pdf)

• M. Menni, Every sufficiently cohesive topos is infinitesimally generated , ms. 2017. (to appear in Cah. Top. Géom. Diff. Cat.; preprint)

• Mike Shulman, Brouwer’s fixed-point theorem in real-cohesive homotopy type theory, Mathematical Structures in Computer Science Vol 28 (6) (2018): 856-941 (arXiv:1509.07584, doi:10.1017/S0960129517000147)

---

1. (Theorem 12.2.3 in La Palme Reyes et al. (2004, p.221)). Of course, this can also easily be proved directly or read off the concrete objects and properties worked out in La Palme Reyes et al. (2004) where the Sierpinski topos is called the category of bouquets. ↩