A Report on Subobject Classifiers and Monads

TL;DR

This paper provides two separate essays discussing subobject classifiers and monads, exploring their theoretical aspects within category theory.

Contribution

It offers a detailed analysis of subobject classifiers and monads, contributing to the understanding of their roles in category theory.

Findings

Clarifies the concept of subobject classifiers

Explores properties of monads in categorical contexts

Provides insights into their theoretical significance

Abstract

A two-part report, containing (unrelated) essays on subobject classifiers and on monads.

Equations

$$a$$

$$x\in -f\text{ iff }x\notin f$$

$$x\in f\cup g\text{ and }x\in f\text{ or }x\in g,$$

$$\mathcal{E}$$

$$f\subseteq g\text{ iff whenever }x:1\to d\text{ and }x\in f\text{, we have }x\in g.$$

$$\alpha$$

$$\mathcal{E}\models \alpha \text{ iff }\mathcal{E}(1,\Omega )\models \alpha \text{ iff }Sub(1)\models \alpha .$$

$$S_a=\{b:b\subseteq a\}.$$

$$\Omega (a)=\{S:S\text{ is an }a\text{-crible}\}$$

$$\Omega (b\subseteq a)=(\Omega (a)\to \Omega (b),S\mapsto \{c\in S:c\subseteq b\}).$$

$$Se{t}^{P^{op}}(H_{\{1,2,3\}},\Omega )\cong$$

$$\varnothing ,$$

$$\{\varnothing \},$$

$$\{\varnothing ,\{1\}\},\{\varnothing ,\{2\}\},\{\varnothing ,\{3\}\},$$

$$\{\varnothing ,\{1\},\{2\}\},\{\varnothing ,\{2\},\{3\}\},\{\varnothing ,\{1\},\{3\}\},$$

$$\{\varnothing ,\{1\},\{2\},\{3\}\},$$

$$\{\varnothing ,\{1\},\{2\},\{1,2\}\},\{\varnothing ,\{1\},\{2\},\{3\},\{1,2\}\}$$

$$\{\varnothing ,\{2\},\{3\},\{2,3\}\},\{\varnothing ,\{1\},\{2\},\{3\},\{2,3\}\}$$

$$\{\varnothing ,\{1\},\{3\},\{1,3\}\},\{\varnothing ,\{1\},\{2\},\{3\},\{1,3\}\}$$

$$\{\varnothing ,\{1\},\{2\},\{3\},\{1,2\},\{1,3\}\},\{\varnothing ,\{1\},\{2\},\{3\},\{1,2\},\{2,3\}\},\{\varnothing ,\{1\},\{2\},\{3\},\{2,3\},\{1,3\}\},$$

$$\{\varnothing ,\{1\},\{2\},\{3\},\{1,2\}\{2,3\},\{1,3\}\},$$

$$\{\varnothing ,\{1\},\{2\},\{3\},\{1,2\}\{2,3\},\{1,3\},\{1,2,3\}\}.$$

$$⟨p=q⟩\cdot p=⟨p=q⟩\cdot q$$

$$\alpha \le ⟨\alpha \cdot p=p⟩.$$

$$⟨p=q⟩\le ⟨q=p⟩$$

$$⟨p=q⟩\wedge ⟨q=r⟩\le ⟨p=r⟩;$$

$$p=⟨p=q⟩\cdot p=⟨p=q⟩\cdot q.$$

$$p=$$

$$=$$

$$\alpha \cdot p=(\alpha \wedge \beta )\cdot p=\alpha \cdot (\beta \cdot p),$$

$$\alpha \cdot p=\alpha \cdot (\beta \cdot q)=(\alpha \wedge \beta )\cdot q\le \alpha \cdot q,$$

$$p\wedge q:=⟨p=q⟩\cdot p=⟨p=q⟩\cdot q.$$

$$r=$$

$$=$$

Full text

1. 1 The subobject classifier and its logical applications
2. 2 The subobject classifier on a presheaf topos
3. 3 Actions of the subobject classifier
4. 4 Monad morphisms
5. 5 Modelling non-determinism with monads
6. A Appendix: Propositional Logic, Intuitionistic Logic, Classical Logic

1 The subobject classifier and its logical applications

Essay* (1(a)).*

In a given category $\mathcal{C}$, let us declare that a monic $f:a\rightarrowtail d$ is contained in a monic $g:b\rightarrowtail d$, if there is a map $h:a\rightarrowtail b$ such that $gh=f$. We declare two monics $f,g$ into $d$ two be equivalent, written $f\simeq g$, if each is contained in the other. A subobject of $d$ is an equivalence class of monics into $d$, and the relation of containment gives us a poset $(Sub(d),\subseteq)$ on the subobjects of $d$.

Let $\mathcal{C}$ be a category with a terminal object $1$. A subobject classifier of $\mathcal{C}$ is a $\mathcal{C}$-object $\Omega$ together with a $\mathcal{C}$-arrow $1\xrightarrow{\textit{true}}\Omega$ that satisfies the following axiom:

($\Omega$-axiom): For each monic $f:a\rightarrowtail d$ there is a unique $\mathcal{C}$-arrow $\chi_{f}:d\rightarrow\Omega$ making

[TABLE]

We say $\chi_{f}$ is the character of the subobject $f$, and often write $\top$ for $true$ and $true_{a}$ for $a\xrightarrow{!}1\xrightarrow{true}\Omega$.

When they exist, subobject classifiers are unique up to (unique) isomorphism, and it is also easy to see that the assignment of $\chi_{f}$ to $f$ yields a 1-1 correspondence between subobjects of $d$ and arrow $d\rightarrow\Omega$ — we have $Sub(d)\cong\mathcal{C}(d,\Omega)$ (at least, so long as we can take arbitrary pullbacks).

An (elementary) topos $\mathcal{E}$ is a Cartesian closed category with a subobject classifier.

For instance, $Set$ is a topos with subobject classifier $\top:1\xrightarrow{1}2$. In Set, a monic is just a subset $a\subseteq d$, and we are familiar with the characteristic function $\chi_{a}:d\rightarrow\{0,1\}$ that sends an element of $d$ to $1$ if it belongs to $a$, and [math] otherwise. We have $\mathcal{P}(d)=Sub(d)\cong Set(d,2)$, and furthermore there are operations of (set-theoretic) union $\cup$, intersection $\cap$ and complement $\lnot$ on $Sub(d)$.

These operations turn $Sub(d)$ into a Boolean algebra: a complemented distributive lattice. In particular, we can use $Set(1,\Omega)=\{0,1\}$ and its operations of $\cup$, $\cap$ and $\lnot$ to model classical logic.

That is the story in $Set$; subobject classifiers are important because they generalise this concept — once we define on $\mathcal{E}(1,\Omega)$ categorical notions of union, intersection and negation that generalise their counterparts in the case of $Set$, we can model different flavours of logics on different topoi! Some of these logics will not even be classical — that is, they will differ from the logic of $Set$, and $Sub(d)$ need not be a Boolean algebra. The algebra of subobjects in such a topos will only be a Heyting algebra.

Let us see how the whole idea of ‘modelling logic with topoi’ works, starting with classical logic.

Recall that in defining the formal language PL (propositional logic), we have the set $\Phi_{0}:=\{\pi_{0},\pi_{1},\pi_{2},\ldots\}$ of variables, and the set $\Phi:=\{\alpha:\alpha\text{ is a {PL}-sentence}\}$ of sentences. (See the Appendix for a review of the formal language PL, along with the axiom systems CL (classical logic) and IL (intuitionistic logic).)

Recall also that every Boolean algebra $\mathbb{B}=(B,\sqsubseteq,\sqcap,\sqcup,^{\prime},0,1)$ has, by definition, operations of meet ($\sqcap$), join ($\sqcup$), and complement (′). We may additionally define an implication operation as $x\Rightarrow y:=x^{\prime}\sqcup y$.

We now describe the semantics of PL in $\mathbb{B}$:

A $\mathbb{B}$-valuation is a function $V:\Phi_{0}\rightarrow B$. By the following rules, any valuation lifts uniquely to a function $V:\Phi\rightarrow B$:

• (a)

$V(\sim\alpha)=V(\alpha)^{\prime}$;

• (b)

$V(\alpha\land\beta)=V(\alpha)\sqcap V(\beta)$;

• (c)

$V(\alpha\lor\beta)=V(\alpha)\sqcup V(\beta)$;

• (d)

$V(\alpha\supset\beta)=V(\alpha)\Rightarrow V(\beta)$.

We say a sentence $\alpha$ is $\mathbb{B}$-valid, and write $\mathbb{B}\models\alpha$, if for every $\mathcal{B}$-valuation $V$ we have $V(\alpha)=1$.

Note that in any $\mathbb{B}$, [math] and $1$ provide a copy of the Boolean algebra 2, so already we see that $\mathbb{B}\models\alpha$ only if $\alpha$ is a tautology, i.e., 2 $\models\alpha$.

We have the following Soundness Theorem for $\mathbb{B}$-validity: If $\vdash_{CL}\alpha$ then $\mathbb{B}\models\alpha$.

The converse also holds! That is, we have the following Completeness Theorem: If $\mathbb{B}\models\alpha$ then $\vdash_{CL}\alpha$.

In particular, if a sentence is valid in some Boolean algebra, then it is a CL-theorem, so it is valid in every Boolean algebra!

This is a powerful result, and indeed, completeness is the harder direction of the two to prove.

Next, let us fulfill the promise of defining truth-arrows in a topos — categorical notions of $\cap$, $\cup$ etc. on the subobject classifier. Let $\mathcal{E}$ be a topos with classifier $\top:1\rightarrow\Omega$. Make the following definitions:

$\lnot:\Omega\rightarrow\Omega$ is the character of $\bot:1\rightarrow\Omega$, where $\bot$ is the character of $!:0\rightarrow 1$. 2. 2.

$\cap:\Omega\times\Omega\rightarrow\Omega$ is the character of the product arrow $\langle\top,\top\rangle:1\rightarrow\Omega\times\Omega$. 3. 3.

$\cup:\Omega\times\Omega\rightarrow\Omega$ is the character of the image of the arrow $[\langle\top_{\Omega},1_{\Omega}\rangle,\langle 1_{\Omega},\top_{\Omega}\rangle]:\Omega+\Omega\rightarrow\Omega\times\Omega$.

(The image of a map $f:a\rightarrow b$ in a topos is the smallest subobject of $b$ through which $f$ factors.) 4. 4.

$\Rightarrow:\Omega\times\Omega\rightarrow\Omega$ is the character of e:\leavevmode\hbox to12.75pt{\vbox to12.75pt{\pgfpicture\makeatletter\hbox{\hskip 6.37334pt\lower-6.37334pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{6.17334pt}{0.0pt}\pgfsys@curveto{6.17334pt}{3.40948pt}{3.40948pt}{6.17334pt}{0.0pt}{6.17334pt}\pgfsys@curveto{-3.40948pt}{6.17334pt}{-6.17334pt}{3.40948pt}{-6.17334pt}{0.0pt}\pgfsys@curveto{-6.17334pt}{-3.40948pt}{-3.40948pt}{-6.17334pt}{0.0pt}{-6.17334pt}\pgfsys@curveto{3.40948pt}{-6.17334pt}{6.17334pt}{-3.40948pt}{6.17334pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.8889pt}{-2.5pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\phantom{\leq}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-2.54428pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\makebox[0.0pt][c]{\rightarrowtail}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\Omega\times\Omega, where $e$ is the equaliser of $\Omega\times\Omega\overset{\cap\ }{\underset{\pi_{1}}{\rightrightarrows}}\Omega$.

In $Set$, unpacking the definitions gives us the classical truth functions.

For instance, $\Rightarrow:2\times 2\rightarrow 2$ sends $(1,0)$ to [math] and all other tuples to $1$.

Now we can describe the semantics of interpreting propositional logic in any topos $\mathcal{E}$!

A truth value in $\mathcal{E}$ is an arrow $1\rightarrow\Omega$.

An $\mathcal{E}$-valuation is a function $V:\Phi_{0}\rightarrow\mathcal{E}(1,\Omega)$. Similarly to valuations on a Boolean algebra, any such function extends to all of $\Phi$ by the following rules:

• (a)

$V(\sim\alpha)=\lnot\circ V(\alpha)$.

• (b)

$V(\alpha\land\beta)=\cap\circ\langle V(\alpha),V(\beta)\rangle$.

• (c)

$V(\alpha\lor\beta)=\cup\circ\langle V(\alpha),V(\beta)\rangle$.

• (d)

$V(\alpha\subset\beta)=\Rightarrow\circ\ \langle V(\alpha),V(\beta)\rangle$.

We say $\alpha$ is $\mathcal{E}$-valid, and write $\mathcal{E}\models\alpha$, if for every $\mathcal{E}$-valuation $V$ we have $V(\alpha)=\top:1\rightarrow\Omega$.

Several questions immediately arise.

For one, we might wonder if the notions of $\mathbb{B}$-valuations and $\mathcal{E}$-valuations are related. We shall give a better result at the end of this section, once we generalise the notion of a Boolean algebra $\mathbb{B}$ to that of Heyting algebra $\mathbb{H}$, and define $\mathbb{H}$-valuations entirely analogously to $\mathbb{B}$-valuations. It will then be noted that $Sub(d)$ is always a Heyting algebra, and that an $\mathcal{E}$-valuation is precisely a $Sub(1)$-valuation, where $1\in\mathcal{E}$ is the terminal object.

Another question one might ask is how ‘compatible’ our topos interpretation is with the system CL: namely, we ask if CL is sound and complete for $\mathcal{E}$-validity. (This was the case for $\mathbb{B}$-validity, i.e., when we interpreted propositional logic in a Boolean algebra.)

It turns out that CL is complete but not sound for $\mathcal{E}$-validity: in any topos $\mathcal{E}$, every $\mathcal{E}$-valid sentence is derivable as a theorem in CL, but there exist topoi $\mathcal{E}$ in which some CL-theorems are not $\mathcal{E}$-valid.

More precisely, the first eleven axioms of CL (see Appendix) are always $\mathcal{E}$-valid, so we are saying that in some topoi the twelth axiom $\alpha\lor\sim\alpha$ is not valid.

The ‘correct’ axiom system which captures $\mathcal{E}$-validity is the system IL (intuitionistic logic), obtained simply by removing the twelfth axiom of CL, keeping all other axioms, and the single inference rule. In IL, tautologies such as $\alpha\lor\sim\alpha$ and $\sim\sim\alpha\supset\alpha$ are not derivable, so this is genuinely a different system than CL.

A topos is degenerate if there is an arrow $1\rightarrow 0$, or equivalently, if all its objects are isomorphic. A topos is bivalent if $\top$ and $\bot$ are its only truth values. A topos is classical if $[\top,\bot]:1+1\rightarrow\Omega$ is an isomorphism.

These are just various measures of how much a topos ‘looks like’ $Set$, which is a non-degenerate bivalent classical topos. We remark that for a bivalent topos $\mathcal{E}$, we do have CL-soundness for $\mathcal{E}$-validity.

As examples, the category $Set^{2}$ of pairs of sets is a classical, non-bivalent topos. If M is a monoid, then the category M-Set of its actions is a topos, and this topos is classical iff M is a group.

In particular M2-Set is not classical, where M2 is the monoid $(\{0,1\},\cdot)$ where $\cdot$ is usual integer multiplication. It is, however, bivalent, so by the above paragraph M2-Set models all the CL-theorems.

Let us next discuss how to turn $Sub(d)$ into a lattice, which we alluded to earlier.

Let $\mathcal{E}$ be a topos, and $d\in\mathcal{E}$. Using the operations we have defined on we define some operations on $Sub(d)$:

The complement of $f:a\rightarrowtail d$ (relative to $d$) is the subobject $-f:-a\rightarrowtail d$ whose character is $\lnot\circ\chi_{f}$. 2. 2.

The intersection of $f:a\rightarrowtail d$ and $g:b\rightarrowtail d$ is the subobject $f\cap g:a\cap b\rightarrowtail d$ whose character is $\chi_{f}\cap\chi_{g}:=\cap\circ\langle\chi_{f},\chi_{g}\rangle$. 3. 3.

The union of $f:a\rightarrowtail d$ and $g:b\rightarrowtail d$ is the subobject $f\cup g:a\cup b\rightarrowtail d$ whose character is $\chi_{f}\cup\chi_{g}:=\cup\circ\langle\chi_{f},\chi_{g}\rangle$. 4. 4.

The subobject $f\Rrightarrow g:a\Rrightarrow b\rightarrowtail d$, for subobjects $f:a\rightarrowtail d$ and $g:b\rightarrowtail d$, is that whose character is $\chi_{f}\Rightarrow\chi_{g}:=\Rightarrow\circ\ \langle\chi_{f},\chi_{g}\rangle$.

Then $(Sub(d),\subseteq)$ is a bounded distributive lattice, with $\cap$ and $\cup$ above providing the meet and join operations. ($1_{d}$ and $0_{d}$ provide the unit and zero.) If this is complemented, then it is a Boolean algebra by definition. This is not always the case: while $f\cap-f\simeq 0_{d}$ always holds, $f\cup-f\simeq 1_{d}$ need not. Let us say a topos is Boolean if for every $d\in\mathcal{E}$, $(Sub(d),\subseteq)$ is a Boolean algebra. The following are equivalent:

$\mathcal{E}$ is Boolean; 2. 2.

$Sub(\Omega)$ is a Boolean algebra; 3. 3.

$\mathcal{E}$ is classical; 4. 4.

$\bot=-\top$ in $Sub(\Omega)$; 5. 5.

$\lnot\circ\lnot=1_{\Omega}$; 6. 6.

in $Sub(\Omega)$, $f\Rrightarrow g\simeq-f\cup g$; 7. 7.

in each $Sub(d)$, $f\Rrightarrow g\simeq-f\cup g$.

In particular, in a non-Boolean topos $\Rrightarrow$ behaves differently from a Boolean implication operator.

The following equivalent conditions are weaker than the above:

$\mathcal{E}\models\alpha$ iff $\vdash_{CL}\alpha$ for every $\alpha$; 2. 2.

$\mathcal{E}\models\alpha\lor\sim\alpha$ for any $\alpha$; 3. 3.

$Sub(1)$ is a Boolean algebra.

These really are weaker conditions. For instance we have remarked that M2-Set models every CL-theorem but is not classical.

The slogan is topoi generalise sets, so let us go further and define, where $f:a\rightarrowtail d$ is a subobject of $d$ in topos $\mathcal{E}$, $x:1\rightarrow d$ to be an element of $f$ if $x$ factors through $f$. Write this as $x\in f$. We always have, in $Sub(d)$, $x\in f\cap g$ iff $x\in f$ and $x\in g$. However, the property

[TABLE]

holds in every $Sub(d)$, iff $\mathcal{E}$ is bivalent. As for the property

[TABLE]

if this holds in every $Sub(d)$ we say $\mathcal{E}$ is disjunctive.

We have the following characterisation:

[TABLE]

A topos is extensional if in $Sub(d)$ we always have

[TABLE]

That is, extensional topoi are those in which subobjects are determined by their elements. $Set$ is extensional.

Let us say a bit more about non-Boolean topoi in general. A topos fails to be Boolean precisely when some $(Sub(d),\subseteq)$ fails to be Boolean. In a lattice $\mathbb{L}=(L,\sqsubseteq)$, we say $c\in L$ is the pseudo-complement of $a\in L$ relative to $b\in L$, written $c=a\Rightarrow b$, if $c$ is the greatest element of $\{x\in L:a\sqcap x\sqsubset b\}$.

If $a\Rightarrow b$ exists for all $a,b\in L$, we say $\mathbb{L}$ is a relatively pseudo-complemented (r.p.c.) lattice.

Finally, a Heyting algebra is an r.p.c. lattice with zero.

If $\mathbb{H}=(H,\sqsubseteq,\Rightarrow,0)$ is a Heyting algebra, we may define the pseudo-complement $\lnot:H\rightarrow H$ as $\lnot a=a\Rightarrow 0$.

We define an $\mathbb{H}$-valuation as a function $V:\Phi_{0}\rightarrow H$. Once again, such a function extends to a function on sentences, using $\sqcap,\sqcup,\Rightarrow,\lnot$ to respectively interpret $\land,\lor,\supset,\sim$ in exactly the same way as with $\mathbb{B}$-valuations.

A sentence $\alpha$ is $\mathbb{H}$-valid if for all $\mathbb{H}$-valuations $V$, $V(\alpha)=1$. $\alpha$ is HA-valid if it is valid in every Heyting algebra.

We have Soundness and Completeness!

[TABLE]

The point is, although $(Sub(d),\subseteq)$ need not be a Boolean algebra, it is always a Heyting algebra. It can be verified that the r.p.c. is given by $\Rrightarrow$.

Since the $\Omega$-axiom gave us $Sub(d)\cong\mathcal{E}(d,\Omega)$ (as sets), we may also consider the latter as a Heyting algebra.

To our relief, the following holds:

[TABLE]

This is because the unit of the Heyting algebra $\mathcal{E}(1,\Omega)$ is $\top:1\rightarrow\Omega$.

Soundness of IL for $\mathcal{E}$-validity now follows immediately for its soundness for HA-validity:

If $\vdash_{IL}\alpha$ then $\alpha$ is HA-valid, so $\mathcal{E}(1,\Omega)\models\alpha$, so $\mathcal{E}\models\alpha$.

In fact IL-Completeness for $\mathcal{E}$-validity also holds: \text{If \alpha is valid on every topos, then }\vdash_{IL}\alpha.

The latter is proven using some additional theory on Kripke-style semantics, in Goldblatt (2006).

As a final remark, we note that higher-order logics can also be interpreted in topoi – these are logics with quantifiers $\forall$, $\exists$. All this again exploits the Heyting algebra structure on $Sub(d)$, which we recall hinges on the existence of the wonderful subobject classifier.

2 The subobject classifier on a presheaf topos

Example** (1(b)(i)).**

*The subobject classifier $\Omega$ of the presheaf topos given by $Set^{P^{op}}$,

where $P$ is the powerset of $\{1,2,3\}$ seen as a poset under inclusion, is described as follows.*

For a given object $a$ in $P$, let $S_{a}$ be the collection of all elements in $P$ contained in $a$,

[TABLE]

A crible on $a$, or $a$-crible, is a downwards-closed subset $S$ of $S_{a}$, meaning whenever $b\in S$ and $c\subseteq b$, then $c\in S$.

Then the subobject classifier is the functor $\Omega:P^{op}\rightarrow Set$ defined on objects by by

[TABLE]

and on maps by

[TABLE]

[TABLE]

(More generally, the subobject category on a functor category $[\mathfrak{C},Set]$ is described similarly using the dual notion of cribles, called $sieves$. This is explained in Goldblatt (2006).)

In our example, there are twenty generalised truth values (arrows from the terminal object to $\Omega$).

To see this, note that the terminal object in $Set^{P^{op}}$ is the functor that sends every element of $P^{op}$ to the terminal object of $Set$, which is just a singleton $1$. The (co)representable functor $H_{\{1,2,3\}}=P(-,\{1,2,3\})$ does this, since for any $a\subseteq\{1,2,3\}$ the set $P(a,\{1,2,3\})$ has precisely one element, given by $a\subseteq\{1,2,3\}$.

Next, observe that

[TABLE]

This means that the generalized truth values are just elements of $\Omega(\{1,2,3\})$, i.e., $\{1,2,3\}$-cribles. There are twenty of these:

[TABLE]

We have systemically listed these twenty $\{1,2,3\}$-cribles in ascending order of the size of a largest set contained in the crible: first we listed the empty crible, then we listed the singleton crible, then the cribles whose largest size of an element is one, then those whose largest size of an element is two, then the crible equal to the entire powerset $\mathbb{P}(\{1,2,3\})$ of $\{1,2,3\}$.

Henceforth we will often write $\Omega$ to mean $\Omega(\{1,2,3\})\cong\text{Sub}(H_{\{1,2,3\}})$.

Proposition** (1(b)(ii)).**

Regarding the truth values of the subobject classifier as a Heyting algebra, $\Omega$ has a monoid stucture with multiplication given by the lattice meet operation $\land$.

Proof.

The meet operation on $\Omega$ is given by set-theoretic intersection. We need to show that this is an associative binary operation on the set of $\{1,2,3\}$-cribles, and that the powerset $\mathbb{P}(\{1,2,3\})$ is the unit of this operation.

To show that $\land$ is a binary operation, we must check that if $S_{1}$ and $S_{2}$ are $\{1,2,3\}$-cribles, then so is $S_{1}\land S_{2}$:

• •

$S_{1}\land S_{2}\subseteq S_{\{1,2,3\}}$, because $S_{1}\land S_{2}\subseteq S_{1}\subseteq S_{\{1,2,3\}}$.

• •

Suppose $c\in S_{1}\land S_{2}$, and $b\subseteq c$.

Then $b\in S_{1}$ since $S_{1}$ is downwards-closed; similarly $b\in S_{2}$ since $S_{2}$ is downwards-closed. Therefore $b\in S_{1}\cap S_{2}=S_{1}\land S_{2}$.

This shows that $S_{1}\land S_{2}$ is really downwards-closed, i.e., a crible.

This binary operation is associative because taking set-theoretic intersections is associative:

for any sets $x,y,z$, we have $(x\cap y)\cap z=x\cap(y\cap z)$.

Finally, the operation has unit $\mathbb{P}(\{1,2,3\})$ because its intersection with any $\{1,2,3\}$-crible $S$ is just $S$.

(After all, we have $S\subseteq S_{\{1,2,3\}}=\mathbb{P}(\{1,2,3\})$.) ∎

3 Actions of the subobject classifier

As a monoid, $\Omega$ can act on a set $X$. This action is well-defined if

[TABLE]

for all $p,q\in X$, where $\langle p=q\rangle$ is the truth value of the assertion $p=q$.

All of the below concerns well-defined actions as above. We define a partial order on $\Omega$ by $\alpha\leq\beta$ iff $\alpha\land\beta=\alpha$. We may assume that

[TABLE]

We also note that the truth assignment satisfies

[TABLE]

and

[TABLE]

Goldblatt (2006) provides these as axioms under the section Heyting-valued sets.

Lemma** (1(c)(i)).**

For all $p,q$ the following three statements are equivalent:

$p=\langle p=q\rangle\cdot p$; 2. 2.

$p=\langle p=q\rangle\cdot q$; 3. 3.

$p=\alpha\cdot q$* for some $\alpha$.*

Proof.

We show that the first statement implies the second, the second implies the third, and the third implies the first.

• •

The first statement implies the second, by assumption of the action being well-defined:

[TABLE]

• •

The second statement implies the third; just take $\alpha=\langle p=q\rangle$.

• •

The third statement implies the first.

Write $p=\alpha\cdot q$ for some $\alpha$. Since $\alpha\leq\langle\alpha\cdot q=q\rangle=\langle p=q\rangle$, we have $\alpha\land\langle p=q\rangle=\alpha$.

Therefore,

[TABLE]

∎

Write $p\leq q$ if the above equivalent conditions hold.

Lemma** (1(c)(ii)).**

The relation $\leq$ just defined is a partial order on $X$.

Proof.

We check reflexivity, transitivity and antisymmetry.

Let $p,q,r\in X$.

• •

$p\leq p$.

Use the third equivalent statement above, and the unit axiom for monoid actions. (This says $p=1\cdot p$, where $1$ is the unit of the monoid.)

• •

if $p\leq q$ and $\ q\leq r$, then $p\leq r$.

Use again the third characterisation of $p\leq q$.

Writing $p=\alpha\cdot q$ and $q=\beta\cdot r$, we see that $p=\alpha\cdot(\beta\cdot r)=(\alpha\land\beta)\cdot r$.

• •

if $p\leq q$ and $\ q\leq p$, then $p=q$.

Using the first characterisation of $p\leq q$, write $p=\langle p=q\rangle\cdot p$.

Using the second characterisation of $q\leq p$, write $q=\langle q=p\rangle\cdot p=\langle p=q\rangle\cdot p$.

Then we see that $p=\langle p=q\rangle\cdot p=q$.

∎

Proposition** (1(c)(iii)).**

The action of $\Omega$ on $X$ seen as a map $\Omega\times X\rightarrow X$ is order-preserving in each variable respectively.

Proof.

• We simply check this in each variable.
• •

Suppose we have $\alpha,\beta\in\Omega$ with $\alpha\leq\beta$. We show that $\alpha\cdot p\leq\beta\cdot p$ for each $p\in X$.

Well, $\alpha=\alpha\land\beta$, so

[TABLE]

and we are done by the third characterisation of $\alpha\cdot p\leq\beta\cdot p$.

• •

Suppose we have $p,q\in X$ with $p\leq q$. We show that $\alpha\cdot p\leq\alpha\cdot q$ for each $\alpha\in\Omega$.

Well, using the third characterisation of $p\leq q$, there is some $\beta\in\Omega$ such that $p=\beta\cdot q$. Then,

[TABLE]

where the last step follows from the fact that the action is order-preserving in the first variable, and the fact that $\alpha\land\beta\leq\alpha$.

∎

Proposition** (1(c)(iv)).**

The partial order on $X$ has a greatest lower bound operation given by

[TABLE]

Proof.

This operation is at least well-defined, since we are working with well-defined actions.

We need to show that $p\land q\leq p$ and $p\land q\leq q$, and that $p\land q$ is universal with respect to these properties, meaning that whenever $r\leq p$ and $r\leq q$, we have $r\leq p\land q$.

• •

$p\land q\leq p$.

$p\land q=\langle p=q\rangle\cdot p$, so w are done by the third characterisation of $p\land q\leq p$. (Just take $\alpha=\langle p\land q\rangle$.)

• •

$p\land q\leq q$.

Similarly, $p\land q=\langle p=q\rangle\cdot q$, so w are done by the third characterisation of $p\land q\leq q$. (Just take $\alpha=\langle p\land q\rangle$.)

• •

whenever $r\leq p$ and $r\leq q$, we have $r\leq p\land q$.

We have

[TABLE]

∎

Proposition** (1(c)(v)).**

For all $p\in X$ we have an adjunction given by the pair of functors $F_{p}:\Omega\rightarrow X$ and $G_{p}:X\rightarrow\Omega$, where

[TABLE]

Proof.

Fix $p\in X$.

It is enough for us to give the unit $\eta:id_{\Omega}\rightarrow G_{p}F_{p}$ and counit $\epsilon:F_{p}G_{p}\rightarrow id_{X}$ of the adjunction.

Let us first show that $\alpha\leq G_{p}F_{p}(\alpha)$ for each $\alpha\in\Omega$, and $F_{p}G_{p}(q)\leq q$ for each $q\in X$.

• •

$\alpha\leq G_{p}F_{p}(\alpha)$ for each $\alpha\in\Omega$.

We have

[TABLE]

• •

$F_{p}G_{p}(q)\leq q$ for each $q\in X$

We have

[TABLE]

This means we have a collection of maps $\eta_{\alpha}:\alpha\rightarrow G_{p}F_{p}(\alpha)$ in $\Omega$, and a collection of maps $\epsilon_{q}:F_{p}G_{p}(q)\rightarrow q$ in $X$. These respectively give us our unit $\eta$ and counit $\epsilon$ of the adjunction. Indeed, since all diagrams commute in a poset, we immediately have naturality of $\eta$ and of $\epsilon$, and also that they satisfy the triangle identities

[TABLE]

∎

Write $\langle p\in Y\rangle=\cup_{z\in Y}\langle z=p\rangle$, where $\cup$ is the lattice join operation on $\Omega$, which is just set-theoretic union. (The union of downwards-closed sets is again downwards-closed.)

Proposition** (1(c)(vi)).**

Any bounded subset $Y$ of $X$ satisfies

[TABLE]

for any upper bound $p$ of $Y$.

Proof.

We want to show that for each $y\in Y$, we have $y\leq\langle p\in Y\rangle\cdot p$, and furthermore, any upper bound $q$ of $Y$ satisfies $\langle p\in Y\rangle\cdot p\leq q$.

• •

for each $y\in Y$, $y\leq\langle p\in Y\rangle\cdot p$.

Observe that $y\leq y$ (by reflexivity of $\leq$) and $y\leq p$ (as $p$ is an upper bound for $Y$), so we have $y\leq y\land p$. Therefore,

[TABLE]

• •

if $y\leq q$ for each $y$, then $(\cup_{z\in Y}\langle z=p\rangle)\cdot p\leq q$.

By the proposition above, we know that $\langle p\leq q\rangle\cdot p=F_{p}G_{p}(q)\leq q$, so it will be enough to show that

[TABLE]

In fact, we only need to show that

[TABLE]

since the action is order-preserving in the first variable.

Let us now show that $\langle y=p\rangle\leq\langle p\leq q\rangle$ for each $y\in Y$.

(Then we would be done, by the universal property of the join.)

First note that $\langle y=y\land q\rangle=1$, since

[TABLE]

Hence, we have

[TABLE]

and so,

[TABLE]

as desired.

∎

4 Monad morphisms

Recall that for a monad $(T,\mu,\eta)$ on a category $\mathfrak{C}$, the objects of its Eilenberg-Moore category $\mathfrak{C}^{T}$ are pairs $(A,\sigma_{A})$ consisting of an object $A$ in $\mathfrak{C}$ and a $\mathfrak{C}$-morphism $\sigma_{A}:TA\rightarrow A$ such that

[TABLE]

As such, the Eilenberg-Moore category of algebras for the monad comes equipped with a forgetful functor $U:\mathfrak{C}^{T}\rightarrow\mathfrak{C}$.

For two categories $\mathfrak{C}_{1}$ and $\mathfrak{C}_{2}$, a monad morphism from $T_{1}$ to $T_{2}$ is a pair $(F,\theta)$ consisting of a functor $F:\mathfrak{C}_{1}\rightarrow\mathfrak{C}_{2}$ and a natural transformation $\theta:T_{2}F\implies FT_{1}$ such that

[TABLE]

Proposition** (2(a)(i)).**

A monad morphism $(F,\theta)$ as above can be used to uniquely define a functor $\hat{F}$ between the corresponding categories of algebras such that the following diagram commutes:

[TABLE]

Proof.

Given such a monad morphism $(F,\theta)$, define a functor $\hat{F}:\mathfrak{C}_{1}^{T_{1}}\rightarrow\mathfrak{C}_{2}^{T_{2}}$ as follows.

Given a $T_{1}$-algebra $(A,\sigma_{A})$, define $\hat{F}(A,\sigma_{A})=(FA,\widetilde{\sigma_{A}})$, where $\widetilde{\sigma_{A}}=F\sigma_{A}\circ\theta_{A}:T_{2}FA\rightarrow FA$.

Indeed, for the desired diagram to commute, the carrier of the algebra $\hat{F}(A,\sigma_{A})$ has to be

[TABLE]

Let us check that our definition really gives us a $T_{2}$-algebra:

• •

[TABLE]

[TABLE]

• •

[TABLE]

[TABLE]

We still have to define $\hat{F}$ on morphisms in $\mathfrak{C_{1}}^{T_{1}}$.

Given a homomorphism of $T_{1}$-algebras $(A,\sigma_{A})\xrightarrow{h}(B,\sigma_{B})$, define $\hat{F}(h):(FA,F\sigma_{A}\circ\theta_{A})\rightarrow(FB,F\sigma_{B}\circ\theta_{B})$ as the homomorphism of $T_{2}$-algebras $FA\xrightarrow{Fh}FB$.

Indeed, for the desired diagram to commute, our choice of $\hat{F}(h)$ is defined uniquely:

[TABLE]

Let us check that $Fh$ is really a homomorphism of $T_{2}$-algebras:

[TABLE]

[TABLE]

Finally, let us check the two functoriality axioms:

• •

for each $T_{1}$-algbera $(A,\sigma_{A})$, we have $\hat{F}(id_{(A,\sigma_{A})})=F(id_{A})=id_{FA}=id_{\hat{F}(A,\sigma_{A})}$;

• •

if $(A,\sigma_{A})\xrightarrow{h}(B,\sigma_{B})$ and $(B,\sigma_{B})\xrightarrow{k}(C,\sigma_{C})$ are maps in $\mathfrak{C_{1}}^{T_{1}}$, then

[TABLE]

∎

Proposition** (2(a)(ii)).**

The converse also holds: each commutative diagram (2) gives rise to a natural transformation $\theta$ making $(F,\theta)$ into a monad morphism.

Proof.

Suppose we have a functor $\hat{F}:\mathfrak{C_{1}}^{T_{1}}\rightarrow\mathfrak{C_{2}}^{T_{2}}$ such that $FU_{1}=U_{2}\hat{F}$. We construct a natural transformation $\theta:T_{2}F\implies FT_{1}$ as follows. Apply $\hat{F}$ to the free $T_{1}$-algebra $(T_{1}A,(\mu_{1})_{A})$ to get a $T_{2}$-algebra $(FT_{1}A,\widetilde{(\mu_{1})_{A}})$. Then, set

[TABLE]

for each $A\in\mathfrak{C_{1}}$.

Note that for each homomorphism of $T_{1}$-algebras $h$, we again know what $\hat{F}(h)$ must be. It is given by

[TABLE]

Now, let us check naturality of $\theta$: for each $A\xrightarrow{f}B$ in $\mathfrak{C_{1}}$,

[TABLE]

[TABLE]

Next, let us verify that $(F,\theta)$ is indeed a monad morphism:

• •

$\theta\circ\mu_{2}F=F\mu_{1}\circ\theta T_{1}\circ T_{2}\theta$:

[TABLE]

• •

$\theta\circ\eta_{2}F=F\eta_{1}$:

[TABLE]

∎

Proposition** (2(a)(iii)).**

If $F$ is faithful so is $\hat{F}$.

Proof.

Let $F$ be faithful, meaning given any two objects $A,B$ of $\mathfrak{C}_{1}$ and a map $FA\xrightarrow{g}FB$ in $\mathfrak{C}_{2}$, there is at most one map $A\xrightarrow{f}B$ in $\mathfrak{C}_{1}$ such that $g=Ff$.

Suppose we are given two $T_{1}$-algebras $(A,\sigma_{A}),(B,\sigma_{B})$, a homomorphism of $T_{2}$-algebras $(FA,\widetilde{\sigma_{A}})\xrightarrow{k}(FB,\widetilde{\sigma_{B}})$, and two homomorphisms of $T_{1}$-algebras $(A,\sigma_{A})\xrightarrow{h_{1},h_{2}}(B,\sigma_{B})$ such that $\hat{F}h_{1}=k=\hat{F}h_{2}$. We must show that $h_{1}=h_{2}$.

Well, $U_{2}k$ is a map $FA\rightarrow FB$ in $\mathfrak{C}_{2}$, so by faithfulness of $F$ there is at most of map $A\xrightarrow{f}B$ in $\mathfrak{C}_{1}$ such that $Ff=U_{2}k$. However, both $f=h_{1}$ and $f=h_{2}$ satisfy this equation:

[TABLE]

Therefore, we must have $h_{1}=h_{2}$ (as maps in $\mathfrak{C}_{1}$, so also as maps in $\mathfrak{C}_{1}^{T_{1}}$). ∎

Proposition** (2(a)(iv)).**

If $F$ is fully faithful and each component of $\theta$ is an epimorphism, then $\hat{F}$ is fully faithful.

Proof.

Now we additionally assume $F$ is full, meaning given any two objects $A,B$ of $\mathfrak{C}_{1}$ and a map $FA\xrightarrow{g}FB$ in $\mathfrak{C}_{2}$, there is some map $A\xrightarrow{f}B$ in $\mathfrak{C}_{1}$ such that $g=Ff$.

Suppose we are given two $T_{1}$-algebras $(A,\sigma_{A}),(B,\sigma_{B})$ and a homomorphism of $T_{2}$-algebras

[TABLE]

By fullness of $F$, there is some map $A\xrightarrow{f}B$ in $\mathfrak{C}_{1}$ such that $U_{2}k=Ff:FA\rightarrow FB$.

Let us show that $f$ is a homomorphism of $T_{1}$-algebras:

[TABLE]

Well, we have

[TABLE]

Since by assumption $\theta_{A}$ is epic, this implies $F(f\circ\sigma_{A})=F(\sigma_{B}\circ T_{1}f)$.

Since we also assumed $F$ to be faithful, we have $f\circ\sigma_{A}=\sigma_{B}\circ T_{1}f$, as desired.

By construction, $\hat{F}f=Ff=k$, so we have completed our proof that $\hat{F}$ is full.

We already know by the result above that $\hat{F}$ is faithful, so we are done.

∎

Theorem** (2(a)(v)).**

If $F$ is fully faithful and $\theta$ is an isomorphism, then $\hat{F}$ is the pullback of $F$ along $U_{2}$.

Proof.

Since $\theta$ is an isomorphism, there is some natural transformation $\beta:FT_{1}\implies T_{2}F$ such that $\theta\circ\beta=id_{FT_{1}}$ and $\beta\circ\theta=id_{T_{2}F}$. In particular, for each $A$ we have

[TABLE]

hence each component $\theta_{A}$ is split epic, hence epic! Therefore we are in the situation of Proposition 2(a)(iv) above, and $\hat{F}$ is fully faithful.

We wish to show that

[TABLE]

is a pullback square.

It certainly commutes, so let us check that it is universal as such.

Suppose we have another commutative square:

[TABLE]

We construct a unique functor $G:\mathfrak{D}\rightarrow\mathfrak{C}_{1}^{T_{1}}$ such that

[TABLE]

• •

Uniqueness of $G$:

Suppose $G$ is a functor satisfying these conditions.

Fix $D\in\mathfrak{D}$. The carrier of the $T_{1}$-algebra $GD$ has to be $G_{1}D$, since $U_{1}GD=G_{1}D$. Hence, write

[TABLE]

We claim that $\sigma_{G_{1}D}$ is also uniquely determined. Apply $\hat{F}$ to this $T_{1}$-algebra, to get the $T_{2}$-algebra

[TABLE]

where $\widetilde{\sigma_{G_{1}D}}=F\sigma_{G_{1}D}\circ\theta_{G_{1}D}$.

Then, $\widetilde{\sigma_{G_{1}D}}\circ\beta_{G_{1}D}=F\sigma_{G_{1}D}\circ\theta_{G_{1}D}\circ\beta_{G_{1}D}=F\sigma_{G_{1}D}$.

This shows that $\sigma_{G_{1}D}$ is unique!

($F$ is fully faithful, so there can only be one map $F^{-1}(\widetilde{\sigma_{G_{1}D}}\circ\beta_{G_{1}D})$ sent by $F$ to $\widetilde{\sigma_{G_{1}D}}\circ\beta_{G_{1}D}$, and we have just shown that $\sigma_{G_{1}D}$ is such a map.)

We have shown that the action of $G$ on objects is uniquely determined. Next, let us show that its action on maps is also uniquely determined.

Let $D\xrightarrow{f}D^{\prime}$ be a map in $\mathfrak{D}$. Then $\hat{F}Gf=G_{2}f$. This shows that $Gf$ is unique.

($\hat{F}$ is fully faithful, so there can only be one map $\hat{F}^{-1}(G_{2}f)$ sent by $\hat{F}$ to $G_{2}f$, and we have just shown that $Gf$ is such a map.)

• •

Existence of $G$:

We know by the above what $G$ has to be, if it exists:

It must be given by $D\mapsto(G_{1}D,\ T_{1}G_{1}D\xrightarrow{\sigma_{G_{1}D}=F^{-1}(\widetilde{\sigma}\circ\beta_{G_{1}D})}G_{1}D)$, $(D\xrightarrow{f}D^{\prime})\mapsto(GD\xrightarrow{\hat{F}^{-1}(G_{2}f)}GD^{\prime})$,

where $\widetilde{\sigma}$ is the map given by $G_{2}D=(U_{2}G_{2}D,\ \widetilde{\sigma})=(FG_{1}D,\widetilde{\sigma})$.

Let us show that this gives us a well-defined functor from $\mathfrak{D}$ to $\mathfrak{C}_{1}^{T_{1}}$.

Note that $Gf=\hat{F}^{-1}(G_{2}f)$ is a homomorphism of $T_{1}$-algebras, by definition. (It is the one that maps under $\hat{F}$ to the homomorphism of $T_{2}$-algebras $G_{2}f$.

Next, we see that $GD$ is really a $T_{1}$-algebra:

• –

$\sigma_{G_{1}D}\circ T_{1}\sigma_{G_{1}D}=\sigma_{G_{1}D}\circ(\mu_{1})_{G_{1}D}$:

Since $F$ is faithful, it is enough to check equality on $F$ applied to these maps.

We have

[TABLE]

• –

$\sigma_{G_{1}D}\circ(\eta_{1})_{G_{1}D}=id_{G_{1}D}$:

Again it is enough to check equality on $F$ applied to these maps. We have

[TABLE]

Next, let us check functoriality of $G$:

• –

$G(id_{D})=\hat{F}^{-1}(G_{2}id_{D})=\hat{F}^{-1}(id_{G_{2}D})=id_{GD}$,

where in the last step we are using that $\hat{F}$ is fully faithful, and that $\hat{F}id_{GD}=id_{\hat{F}GD}=id_{G_{2}D}$.

• –

Let $D\xrightarrow{f}D^{\prime}$, $D^{\prime}\xrightarrow{g}D^{\prime\prime}$ be maps in $\mathfrak{D}$.

Then $G(g\circ f)=\hat{F}^{-1}(G_{2}(g\circ f))=Gg\circ Gf$,

where in the last step we are using that $\hat{F}$ is fully faithful, and that

[TABLE]

Finally, we must check the universal property for pullbacks:

• –

$\hat{F}G=G_{2}$:

[TABLE]

so we have equality on objects.

On maps,

[TABLE]

• –

$U_{1}G=G_{1}$:

[TABLE]

so we have equality on objects.

On maps,

[TABLE]

where the last equality follows from the equality of $F$ applied to these maps:

[TABLE]

∎

5 Modelling non-determinism with monads

Essay* (2(b)).*

Monad are commonly used to model non-deterministic procedures. This can be implemented effectively in Haskell (or indeed other functional programming languages).

Non-determinism of an algorithm just means that at each stage there are several possible outputs that can be taken as input of the next stage. For instance, non-deterministic finite state automata have transition functions of the form $\delta:Q\times\Sigma\cup\epsilon\rightarrow\mathcal{P}(Q)$, where $Q$ is the set of states, and $\Sigma$ is the alphabet. At each stage the machine may transition to several (or no) states.

We give three brief instances of how monads model non-determinism. Since we would like to account for each possible branch of the computation, we use the list monad to form a collection of the outcomes. (The Powerset monad works fine, too — see our closing remark.)

Our first example demonstrates the extent to which monads are inbuilt into Haskell.

Suppose we have a list of functions $[f_{1},\cdots,f_{n}]$ on the same domain, and a list of elements $[x_{1},\cdots,x_{m}]$ in the domain. We would like to evaluate each function on each element. We may execute these calculations ‘in parallel’ with the command

⬇

    ghci> (app) <$> [f1, ..., fn] <*> [x1, ..., xm]

where app takes a function and an element and applies the former to the latter.

The monad does not even appear explicitly, but we are actually using the list monad as an applicative.

To make the monad structure more clear, we note that this is nothing more than the list comprehension

[TABLE]

In general, a comprehension has the form [t|q], where t is a term, and q a qualifier. A qualifier has one of the following forms:

• •

the empty qualifier $\Lambda$;

• •

a generator x $\leftarrow$ u, for some variable x and list-valued term u;

• •

a composition (p,q) of shorter qualifiers.

The point is that monads $(T,\eta,\mu)$ can be derived from comprehensions, and vice versa. We have:

• •

[t|$\Lambda$] = $\eta_{t}$;

• •

[t|x $\leftarrow$ u] = $T(\lambda x.t)u$;

• •

[t|(p,q)] = $\mu($[[t|q]|p]$)$.

See Wadler (1992) for further details.

A second example is the composition of multi-valued functions. If we take the $m^{th}$ root of a complex number, and then take the $n^{th}$ root of the result, we want this to be equal to the result of taking the $mn^{th}$ root. Hence we would like to return $mn$ possibilities in a list.

Once again the list monad achieves this. We simply define:

⬇

    bind :: (**Complex** **Double** -> [**Complex** **Double**]) -> ([**Complex** **Double**] -> [**Complex** **Double**])

    bind f x = **concat** (**map** f x)

    unit :: **Complex** **Double** -> [**Complex** **Double**]

    unit x = [x]

Here we have given the monad in Kleisli form, where the Kleisli extension is given by bind, and the unit by unit, of course.

We end with another application of the list monad, to the modelling of a conditional probability problem (Taylor, 2013). Suppose we are given two boxes $A$ and $B$, each containing three marbles. The first has one white and two black marbles; the second has all three marbles white. We blindly select a box at random, and then from the box randomly extract a marble. If this is white, what is the probability that we selected the first box?

Using Bayes’ Theorem we may calculate this probabillity to be $\frac{(1/3)(1/2)}{4/6}=1/4$, but using the list monad we may model the scenario explicitly; such methods are valuable in applied statistics.

⬇

        **data** Box = BoxA | BoxB **deriving** (**Show**)

        **data** Marble = Black | White **deriving** (**Eq**,**Show**)

        extract BoxA   = [White, Black, Black]

        extract BoxB = [White, White, White]

        pick = [BoxA, BoxB]

        trial = **do**

          box   <- pick         *-- Simulate picking a box at random*

          result <- toss coin    *-- Extract a marble and observe the result*

          **guard** (result == White) *-- We only proceed if the marble is white*

          **return** box            *-- Return which box this marble came from*

        >> trial

    \\    [BoxA, BoxB, BoxB, BoxB]

Let us briefly explain the code. First, we defined two data types that store the values of the boxes and the marbles. Then, we modelled the outcomes using a list. We next defined a function pick that modelled the random selection of either box.

Where the monad comes in is the do block.

In Haskell,

⬇

    **do** { x1 <- action1

       ; x2 <- action2

       ; mk_action3 x1 x2 }

is short for

⬇

    action1 >>= (\ x1 ->

      action2 >>= (\ x2 ->

        mk_action3 x1 x2 ))

where >>= is the bind combinator, i.e., Kleisli extension:

[TABLE]

Since the program outputs three instances of BoxB and one of BoxA, we conclude that the probability that we had chosen Box $A$, given that we have extracted a white marble, is $1/4$ as expected.

It is worth noting that the algorithm is not really randomly selecting boxes and extracting marbles; we are merely simulating the non-determinism of the process by listing all the outcomes — that is the point, after all.

As a closing remark, we note that the powerset monad also models non-determinism effectively, albeit with less structure than the list monad — now we no longer keep track of duplicate entries, and elements of a list are returned having no order. Depending on the scenario it is useful to use one monad or the other. For instance, the powerset monad would not model our last example, since there we needed to keep track of duplicates. However, the powerset monad might better suit our first example if we wished to return values in no particular order and without repetitions.

Appendix A Appendix: Propositional Logic, Intuitionistic Logic, Classical Logic

The formal language PL (propositional logic) is described by its alphabet and formation rules:

• •

the alphabet for PL consists of:

a collection $\{\pi_{i}:i\in\mathbb{N}\}$ of symbols, called the propositional variables; 2. 2.

the symbols $\sim,\land,\lor,\supset$; 3. 3.

the bracket symbols $)$, $($.

• •

we have the following formation rules for PL-sentences:

each propositional variable $\pi_{i}$ is a PL-sentence, or formula; 2. 2.

if $\alpha$ is a sentence, so is $(\sim\alpha)$; 3. 3.

if $\alpha$ and $\beta$ are sentences, so are $(\alpha\land\beta),(\alpha\lor\beta),(\alpha\supset\beta)$.

Define $\Phi_{0}:=\{\pi_{0},\pi_{1},\pi_{2},\ldots\}$ and $\Phi:=\{\alpha:\alpha\text{ is a {PL}-sentence}\}$.

An axiom system is described by a collection of sentences (its axioms), and a collection of inference rules, which prescribe operations on sentences in order to derive new ones. A proof sequence is a finite sequence of sentences, each of which is either an axiom or derivable from earlier members of the sequence using an inference rule.

The axiom system CL (classical logic) has axioms which are sentences of one of the form:

$\alpha\supset(\alpha\land\alpha)$; 2. 2.

$(\alpha\land\beta)\supset(\beta\land\alpha)$; 3. 3.

$(\alpha\supset\beta)\supset((\alpha\land\gamma)\supset(\beta\land\gamma))$; 4. 4.

$((\alpha\supset\beta)\land(\beta\supset\gamma))\supset(\alpha\supset\gamma))$; 5. 5.

$\beta\supset(\alpha\supset\beta)$; 6. 6.

$(\alpha\land(\alpha\supset\beta))\supset\beta$; 7. 7.

$\alpha\subset(\alpha\lor\beta)$; 8. 8.

$(\alpha\lor\beta)\supset(\beta\lor\alpha)$; 9. 9.

$((\alpha\supset\gamma)\land(\beta\supset\gamma))\supset((\alpha\lor\beta)\supset\gamma)$; 10. 10.

$(\sim\alpha)\supset(\alpha\supset\beta)$; 11. 11.

$((\alpha\supset\beta)\land(\alpha\supset\sim\beta))\supset(\sim\alpha)$; 12. 12.

$\alpha\lor(\sim\alpha)$.

The system CL has one inference rule:

Modus Ponens. From $\alpha$ and $\alpha\supset\beta$ we may derive $\beta$.

We say $\alpha$ is a CL-theorem, and write $\vdash_{CL}\alpha$, if $\alpha$ is the last member of some proof sequence in CL.

That last axiom $\alpha\lor(\sim\alpha)$ in CL is called the law of excluded middle; if we remove this axiom, keeping all the other axioms and the Modus Ponens inference rule, then we obtain the axiom system IL (intuitionistic logic).

We say $\alpha$ is an IL-theorem, and write $\vdash_{IL}\alpha$, if $\alpha$ is the last member of some proof sequence in IL.