1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
|
\Chapter{Conventions}{Here's a one of a kind\\Convention of the mind}{Red Hot Chili Peppers}\appendixlabel{conventions}
\cats{}Sections indicated with a ``beware cats'' sign assume
deeper, but standard, knowledge of category theory. The assumed
knowledge includes: (co)limits, adjunctions, (co)continuity, and
monads, as covered by Mac Lane~\cite{maclane:working-mathematician},
and symmetric monoidal closed categories, and enrichment, as covered
by Kelly~\cite{kelly:basic-concepts-of-enriched-category-theory}.
\nocats{}The ``cat-free'' parts assume only basic
categorical notions, previously used in the semantics and
functional programming communities. We assume
familiarity with functors, monads, natural transformations, and monad
morphisms. These parts may be
read sequentially, skipping over ``beware
cats'' sections. While the statements are formulated in these
more accessible terms, their proofs may rely on categorically involved
accounts. The scope of these two modifiers extends to the end of the literary
unit they are introduced in, such as Chapter, Section, or Proof.
We revisit definitions, examples, and theorems during the development.
%
\DELTA{Shading} indicates the difference from the original unit.
%
An asterisk, e.g., \definitionref+{generic-model}, indicates the
revisited unit is recast in terms of generic effects.
%
An $\omega$, e.g., \definitionref+{recursion-signature}, indicates the
revisited unit is a domain-theoretic specialisation.
%
A (revisited) mark, e.g., \definitionref+{set-type-assignment},
indicates the revisited unit is a set-theoretic reformulation of a
categorically involved unit.
%
A plus,e.g. \definitionref+{presentation-model}, indicates the
revisited unit is an algebraic reformulation in terms of theories
and/or presentations.
%
These modifiers combine, e.g.,
Definition~\algebraicrevisit{definition}{generic-model}{set-generic-model},
meaning an algebraic reforumaltion of the set-theoretic instance of
the generic effects alternative to \definitionref{categorical-model}.
%
Electronic versions of this document use hyper-references to
ease cross-references.
|