Seven Sketches in Compositionality: An Invitation to Applied Category Theory

Purpose and audience

• The book offers a self-contained taste of advanced category-theoretic topics through concrete examples, rather than a comprehensive treatment.It aims to give readers a sense of working with these structures and how they might appear in practice.Source: Purpose and audience · p. 3
• Many applied category theory topics build on monoidal categories, so the book aims to provide an unconventional reference for them.The authors note that introductory material on monoidal categories was scarce in 2018, with user-friendly exceptions in [CK17, Chapter 3] and [CP10].Source: Purpose and audience · p. 4
• The book is intended to be approachable with minimal prerequisites, while leaving the complete story to further reading and future exploration.The authors hope readers will use it to orient themselves in a growing literature and discover applications.Source: Purpose and audience · p. 4

How to read this book

• Chapters pair a real-world motivation, such as circuits or control theory, with a category-theoretic purpose.The book asks readers to watch for structures and coherence as concepts are layered throughout its chapters.Source: How to read this book · p. 5
• Chapter difficulty increases within each chapter, but later chapters begin fairly easily, allowing readers to move on and return to difficult material later.The authors include about 240 exercises, with solutions in Appendix A, and encourage active work through them.Source: How to read this book · pp. 5–6

Personal note

• The authors ground their application of category theory beyond mathematics in the hope that it can help bring humanity together around big problems.They caution that, like any tool, category theory can be used for purposes they do not align with.Source: Personal note · p. 6
• Suggested actions include inviting under-represented people into study groups and designing software that helps people relate and align.The authors frame these as examples of using the book's material for social good.Source: Personal note · p. 6
• The authors hope readers use category theory to connect people, create common ground, and represent life, society, and environment across perspectives.They ask readers to share such efforts with the authors and community.Source: Personal note · pp. 6–7

5 Signal flow graphs: Props, presentations, & proofs

• The chapter introduces props and presentations, including port graphs and free constructions.Its contents also include universal properties and the free prop on a signature.Source: §5 · p. 10
• The chapter develops simplified signal flow graphs and relates them to matrices over a rig.Listed topics include turning signal flow graphs into matrices and functorial semantics.Source: §5 · p. 10
• The chapter's graphical linear algebra material includes a presentation of Mat(R) and signal flow graphs with feedback.It also includes an aside on monoid objects in a monoidal category.Source: §5 · p. 10

6 Circuits: hypergraph categories and operads

• The chapter introduces colimits and connection, covering initial objects, coproducts, pushouts, finite colimits, and cospans.Source: §6 · pp. 10–11
• The chapter develops hypergraph categories through Frobenius monoids, wiring diagrams, and their definition.Source: §6 · p. 11
• The chapter presents decorated cospans and applies them to electric circuits.It also covers symmetric monoidal functors.Source: §6 · p. 11
• The chapter treats operads as a way to design wiring diagrams and includes operads from symmetric monoidal categories.It also lists the operad for hypergraph props.Source: §6 · p. 11

7.1 How can we prove our machine is safe?

• The chapter opens with the question of how to prove a machine is safe.Source: §7 · p. 11

7.2 The category Set as an exemplar topos

• It introduces Set as an exemplar topos, covering topos-like properties, the subobject classifier, and logic in Set.Source: §7 · p. 11

7.3 Sheaves

• The sheaves section proceeds from presheaves and topological spaces to sheaves on topological spaces.Source: §7 · p. 11

7.4 Toposes

• The toposes section covers a sheaf topos’s subobject classifier and logic, predicates, quantification, modalities, and type theories and semantics.Source: §7 · p. 11

7.5 A topos of behavior types

• The chapter then treats a topos of behavior types through the interval domain, sheaves on IR, and safety proofs in temporal logic.Source: §7 · p. 11

A Exercise solutions

• Solutions for Chapters 1 and 2 are listed in Appendix sections A.1 and A.2.Source: A Exercise solutions · p. 11
• Appendix sections A.3 through A.5 list solutions for Chapters 3 through 5.Source: A Exercise solutions · p. 12
• Appendix sections A.6 and A.7 list solutions for Chapters 6 and 7.Source: A Exercise solutions · p. 12

1.1 More than the sum of their parts

• Because observation is lossy, combining systems can yield results that differ from combining their observations, a phenomenon the section calls a generative effect.The section notes that this can matter when local authorities combine information about possible contagion.Source: §1.1 · pp. 13, 14, 17

1.1.1 A first look at generative effects

• Alice’s observation returns false for each of two systems but true for their join, showing that it does not preserve join.The observation tracks only whether • and ∗ are connected; the joined system connects them through ◦, so a more detailed observation is needed to predict the result.Source: §1.1 · p. 16

1.1.2 Ordering systems

• Systems are ordered by inclusion of their connections, their join is the least system above both, and Alice’s observation preserves order but not join.For the example, Φ(A) ∨ Φ(B) can be false while Φ(A ∨ B) is true.Source: §1.1.2 · pp. 17–18

1.2.1 Review of sets, relations, and functions

• A partition of a set determines an equivalence relation, and each equivalence relation determines a partition whose parts are its nonempty closed, connected subsets.The constructions are mutually inverse; the quotient is the set of parts in the corresponding partition.Source: §1.2.1 · p. 22
• A surjective function from A to P determines a partition of A through the preimages of the elements of P.Each preimage is one part of the partition.Source: §1.2.1 · p. 24

1.2.2 Preorders

• A preorder is a reflexive, transitive relation; unlike a partial order, it may treat distinct elements as equivalent when each is related to the other.Identifying such equivalent elements converts a preorder into a partial order.Source: §1.2.2 · p. 25
• A graph presents a preorder by declaring v ≤ w exactly when a path runs from v to w, with reflexivity and transitivity arising from paths.Paths of length zero give reflexivity, and concatenation gives transitivity.Source: §1.2.2 · pp. 26–27
• Preorders can encode different structures, including total orders on natural numbers, divisibility on natural numbers, and subset inclusion on power sets.The natural-number size ordering is total, whereas the power set is ordered by inclusion.Source: §1.2.2 · pp. 27–28
• In a preorder, partitions can be ordered by fineness, upper sets by inclusion, product orders coordinatewise, and the opposite preorder reverses the order.Source: §1.2.2 · pp. 29–30

1.2.3 Monotone maps

• Monotone maps preserve preorder relations; maps P→B correspond bijectively to upper sets, and p↦↑p represents each element by its relationships with other elements up to equivalence.Source: §1.2.3 · pp. 30, 32, 34

1.3 Meets and joins

• Meets and joins are greatest lower bounds and least upper bounds, respectively, and exemplify universal properties that have categorical counterparts in limits and colimits.Source: §1.3 · p. 35, §1.3.1 · p. 35

1.3.1 Definition and basic examples

• A meet is a greatest element among the lower bounds of a subset, while a join is a least element among its upper bounds; either may fail to exist, and multiple meets are equivalent.Source: §1.3.1 · pp. 35–36

1.3. MEETS AND JOINS

• In a power set ordered by inclusion, the meet of two subsets is their intersection and their join is their union.Source: §1.3 · p. 37
• If one set of elements is contained in another, its meet is at least as large and its join is at most as large, whenever those meets and joins exist.For sets, the text identifies meet with intersection and join with union; in a total order, they are infimum and supremum.Source: §1.3 · p. 37

1.3.2 Back to observations and generative effects

• A monotone map has a generative effect when joining inputs reveals more than joining their separate observations; Adam’s approach restricts to maps that preserve meets [Ada17].Meet preservation makes the map behave well on subsystems even when joining systems produces surprises.Source: §1.3.2 · p. 38

1.4 Galois connections

• Galois connections relate two preorders through monotone maps in opposite directions and are a special case of adjunctions.They generalize preorder isomorphisms: every preorder isomorphism is a Galois connection, but not every Galois connection is an isomorphism.Source: §1.4 · p. 38, §1.4.1 · p. 39

1.4.1 Definition and examples of Galois connections

• A Galois connection consists of monotone maps in opposite directions, one a left adjoint and the other a right adjoint; for total orders, the text visualizes the condition using noncrossing arrows.The example of multiplication by 3 from integers to reals uses the ceiling of division by 3 as a left adjoint.Source: §1.4.1 · pp. 39–40

1.4.2 Back to partitions

• Any function between sets induces a Galois connection on their partition preorders: the left adjoint pushes partitions forward and takes transitive closure, while the right adjoint pulls them back.The push-forward first relates target elements whose preimages were related, then adds relations needed for transitivity.Source: §1.4.2 · pp. 40–41

1.4.3 Basic theory of Galois connections

• When the relevant preorders have all meets or joins, a monotone map preserves meets exactly when it is a right adjoint, and preserves joins exactly when it is a left adjoint.More generally, right adjoints preserve meets and left adjoints preserve joins. For a function between sets, the preimage map has both adjoints: direct image is its left adjoint, and the right adjoint is also described in the text.Source: §1.4.3 · pp. 43–45
• Adjoints induced by a function yield three meaningful operations on subsets of apples and buckets, with interpretations based on containment and whether buckets contain chosen apples.The text notes that empty buckets count among those whose apples are all in the chosen subset, vacuously.Source: §1.4.3 · p. 45

1.4.4 Closure operators

• Composing adjoints gives a closure operator: a monotone, inflationary, idempotent map that can model valid, repeat-stable expression reduction.In logic, propositions ordered by implication admit modal closure operators; “assuming Bob is in San Diego” is given as an example.Source: §1.4.4 · pp. 45–47
• Conversely, any closure operator yields an adjunction from the preorder to its sub-preorder of fixed points, with the inclusion as right adjoint.The left adjoint sends each element to its closure; the adjunction follows from the fixed-point property and inflationarity.Source: §1.4.4 · p. 46

1.4.5 Level shifting

• For a set S, reflexive-transitive closure sends binary relations to preorders and is left adjoint to the inclusion of preorders among relations.This is a level shift: preorders on S themselves form a preorder under inclusion.Source: §1.4.5 · p. 47

1.5 Summary and further reading

• The chapter frames generative effects as observations of a whole that cannot be deduced by combining observations of its parts, and relates adjoints to preservation of joins or meets.Later chapters add monoidal structure to preorders and morphisms to orders, bringing these generalizations together in monoidal categories; preorders offer a simpler setting for intuition.Source: §1.5 · p. 48

2.1 Getting from a to b

• Monoidal preorders and wiring diagrams formalize recipes for transforming resources and combining existing methods; V-categories let a preorder structure questions about possibility or cost between points.In a more general monoidal-category setting, Set-categories can describe sets of methods between points.Source: §2.1 · pp. 51–53

2.2 Symmetric monoidal preorders

• A symmetric monoidal preorder adds a monotone binary product and unit to a preorder, with the product associative and symmetric.The product combines elements while preserving their order; the unit acts neutrally.Source: §2.2.1 · pp. 53–54

2.2.1 Definition and first examples

• The real numbers with ≤, 0, and addition form a symmetric monoidal preorder, while the proposed poker-hand product fails because it is not monotone.The poker example gives better individual hands whose proposed combined hand loses to the combination of weaker hands.Source: §2.2.1 · pp. 54–55

2.2.2 Introducing wiring diagrams

• Wiring diagrams represent elements as wires and relationships as boxes, combining them in series and parallel to depict graphical proofs.For the lemon meringue pie example, the diagram proves the overall recipe if each interior method is valid.Source: §2.2.2 · pp. 56, 59
• The exercises ask readers to derive Eq. (2.17) from Eq. (2.16) using the preorder rules and identify when the wiring diagram needs no symmetry axiom.They specifically call for explicit use of reflexivity and transitivity.Source: §2.2.2 · p. 60

2.2.3 Applied examples

• Applied resource theories model static conversions: chemistry uses reactions, manufacturing permits discarding resources, and classical information permits copying them.Chemistry is formalized by materials ordered by possible reactions, with combination as the monoidal product; manufacturing adds an axiom allowing any resource to be discarded. For information, copying is added alongside discarding.Source: §2.2.3 · pp. 61, 63, 64

2.2.4 Abstract examples

• Abstract examples include Bool with AND as its monoidal product, as well as structures on natural numbers under addition and on divisibility under multiplication.Bool uses true as its unit, and the text notes that another monoidal structure on the Boolean preorder uses OR, though the AND structure seems more useful in practice.Source: §2.2.4 · pp. 64–65
• Cost uses nonnegative extended reals ordered by ≥, with 0 as unit and addition as product; reversing any symmetric monoidal preorder preserves its structure.In Cost, enrichment interprets getting from a to b as a cost question, with the cost from a to c at most the sum of the costs from a to b and b to c.Source: §2.2.4 · pp. 66–67

2.2.5 Monoidal monotone maps

• A monoidal monotone is a monotone map that sends the source unit above the target unit and preserves products up to the target preorder.For f from P to Q, the conditions are IQ ≤Q f(IP) and f(p1) ⊗Q f(p2) ≤Q f(p1 ⊗P p2).Source: §2.2.5 · p. 67
• Monoidal monotones preserve preorder structure and satisfy unit and tensor inequalities; stronger variants are called strong or strict, while the floor map is not strong.The floor map from nonnegative reals to naturals satisfies f(x) + f(y) ≤ f(x + y), but fails the strong condition at x = y = 0.5.Source: §2.2.5 · pp. 67–68

2.3 Enrichment

• V-categories use a symmetric monoidal preorder as their base; Bool-categories are preorders, and Cost-categories generalize metric spaces.Source: §2.3 · p. 69

2.3.1 V-categories

• A V-category has objects and V-valued hom-objects, with the monoidal unit bounded by each self-hom and hom composition satisfying X(x, y) ⊗ X(y, z) ≤ X(x, z).V is a symmetric monoidal preorder; symmetry is needed for products of V-categories to exist.Source: §2.3.1 · p. 69

2.3.2 Preorders as Bool-categories

• There is a one-to-one correspondence between preorders and Bool-categories.A Bool-category defines x ≤ y when its hom-object X(x, y) is true; its axioms give reflexivity and transitivity.Source: §2.3.2 · pp. 70–71

2.3.3 Lawvere metric spaces

• A Lawvere metric space is a Cost-category, retaining zero self-distance and the triangle inequality while allowing infinite, asymmetric distances.Its Cost-valued hom-objects serve as distances, with composition expressed by d(x, y) + d(y, z) ≥ d(x, z).Source: §2.3.3 · pp. 72–73

2.3.4 V-variations on preorders and metric spaces

• Other monoidal preorders can serve as enrichment bases, and an M-category can represent the modes of transportation available between each pair of objects.For the transportation interpretation, hom-objects are subsets of modes; the exercise constructs them by intersecting edge labels along paths and taking the union across paths.Source: §2.3.4 · p. 75

2.4.1 Changing the base of enrichment

• A monoidal monotone V→W changes a V-category into a W-category by retaining its objects and applying the map to each hom-object.The example map from Cost to Bool converts Lawvere metric spaces into preorders.Source: §2.4.1 · p. 76, §2.4 · p. 77

2.4.2 Enriched functors

• V-functors generalize structure-preserving maps: Bool-functors correspond to monotone maps of preorders, while Cost-functors are 1-Lipschitz maps.A Cost-functor does not increase distances between any pair of points.Source: §2.4.2 · p. 78

2.4.3 Product V-categories

• The V-product has pairs of objects and assigns each pair-to-pair hom-object by tensoring the corresponding hom-objects in its factors.For Cost-categories this gives product objects with distances equal to the sum of the factor distances; for Bool-categories it gives componentwise preorder relations.Source: §2.4 · p. 79

2.5 Computing presented V-categories with matrix multiplication

• Generalized matrix multiplication constructs matrix representations of categories presented by weighted graphs when the enriching preorder is a unital commutative quantale.Such a quantale has all joins and is symmetric monoidal closed.Source: §2.5 · pp. 80–81, §2.5.2 · p. 83

2.5.1 Monoidal closed preorders

• In a closed monoidal preorder, −⊗v has right adjoint v⊸−, and the hom-elements v⊸w make the preorder enriched in itself.In resource terms, a⊗c can yield d exactly when a can yield the single-use converter c⊸d; the chemical-material preorder Mat is not closed.Source: §2.5.1 · pp. 81–83

2.5.2 Quantales

• Cost is a quantale, and a symmetric monoidal preorder with all joins is closed exactly when its monoidal product distributes over joins.In a preorder, having all joins is equivalent to having all meets, so quantales have both despite being defined using joins.Source: §2.5.2 · pp. 84–85

2.5.3 Matrix multiplication in a quantale

• For a finite weighted graph, powers of its quantale-valued matrix stabilize at the distance matrix, yielding an algorithm to compute the presented V-category.Each power records shortest-path lengths using at most that many edges; in the infinite case, taking the infimum of all powers still defines a Lawvere metric space.Source: §2.5.3 · p. 87, §2.6 · p. 87

2.6 Summary and further reading

• Resource-based preorders lead to monoidal preorders and enrichment over Bool; replacing Bool with Cost gives Lawvere metric spaces, where hom-objects describe resource-conversion costs.The chapter also presents base change, functors, and products, and shows how labelled graphs and matrix multiplication compute V-category hom-objects.Source: §2.6 · p. 87
• Noncommutative quantales include power sets of monoids and binary relations under composition, with applications to concurrency, process semantics, and automata.The section points to further work on resource theories, enrichment, Lawvere metric spaces, and quantales.Source: §2.6 · pp. 87–88

3.1. WHAT IS A DATABASE?

• Category-theoretic data migration translates data between different organizational forms and can guarantee that migrated data fits the target schema and satisfies its constraints.The chapter formalizes migration using adjoint functors.Source: §3.1 · pp. 92–93

3.1 What is a database?

• A database schema represents tables and their cross-references; instances are set-valued functors from schema categories, and schema mappings are functors.Unique ID columns let entries in one table reference rows in another.Source: §3.1 · pp. 90, 93

3.2 Categories

• A category consists of objects, morphisms, identities, and composition, subject to unitality and associativity.Morphisms have domains and codomains, and composition combines compatible morphisms.Source: §3.2 · p. 93

3.2.1 Free categories

• The free category on a graph has its vertices as objects and paths as morphisms, with trivial paths as identities and path concatenation as composition.A one-object category corresponds to a monoid.Source: §3.2.1 · pp. 94–95

3.2.2 Presenting categories via path equations

• A finite graph with equations between parallel paths presents a finitely presented category; identifying paths can reduce the morphisms and imply further equations.Database schemas are finite presentations of categories.Source: §3.2.2 · pp. 96–97

3.2.3 Preorders and free categories: two ends of a spectrum

• A preorder can be viewed as a category in which every pair of parallel arrows is equal, and any category can be “crushed down” into a preorder.This frames preorders and categories as two ends of a spectrum.Source: §3.2.3 · p. 97
• Preorders and free categories are opposite extremes of graph presentations: all parallel paths are identified in preorders, while each path remains distinct in free categories.Presentations with some path equations lie between these extremes.Source: §3.2.3 · p. 98

3.2.4 Important categories in mathematics

• Set has sets as objects and functions as morphisms, and categories in the ordinary sense are exactly Set-categories.Other examples include categories of topological spaces, graphs, and groups; reversing all morphisms produces the opposite category.Source: §3.2.4 · pp. 99–100

3.2.5 Isomorphisms in a category

• An isomorphism is a morphism with a two-sided inverse, formalizing when objects are interchangeable; in FinSet, cardinality is characterized by isomorphism to a natural number.In Set, isomorphisms are bijections.Source: §3.2.5 · p. 100

3.3.3 Database instances as Set-valued functors

• Database instances map each schema category to sets and functions, so they are functors into Set.A database schema presents a category, and an instance is a set-valued functor on it.Source: §3.3.1 · p. 102, §3.3.3 · p. 105

3.3.1 Sets and functions as databases

• Database schemas become categories, while sets are one-column tables and functions require tables for both their domain and codomain.An instance assigns a set to each schema vertex and a function to each arrow.Source: §3.3.1 · pp. 101–102

3.3.2 Functors

• A functor preserves identities and composition; between preorders, functors are exactly monotone maps.The section also shows that a commutative-square category cannot map to a free-square category while preserving the named objects, because that would impose an equation absent from the free category.Source: §3.3.2 · pp. 103–104

3.3.3 Database instances as Set-valued functors

• A database schema is a category, its instances are set-valued functors, and functorial composition enforces the schema’s constraints or business rules.The section defines a schema as a finitely presented category and an instance as a functor to Set.Source: §3.3.3 · pp. 105–106

3.3.4 Natural transformations

• A natural transformation assigns each object a morphism between functor values, with naturality requiring compatibility with every morphism; these transformations are morphisms in a functor category.When the source category has one object, a natural transformation between Set-valued functors is just a function between the corresponding sets.Source: §3.3.4 · pp. 107–108
• For functors N → N, natural transformations exist exactly when the corresponding sequences are pointwise ordered, so the functor category is the preorder of monotone maps N → N.Any two such natural transformations are the same.Source: §3.3.4 · pp. 108–109

3.3.5 The category of instances on a schema

• Every graph can be represented as an instance on the graph schema Gr, and every Gr-instance is a graph; the instance homomorphisms are graph homomorphisms respecting sources and targets.Naturality ensures the vertex and arrow maps commute with the source and target maps.Source: §3.3.5 · p. 110

3.4 Adjunctions and data migration

• Composing functors gives a simple form of data migration between schemas, while more complex migrations use adjoints.The section introduces migration by composing a schema functor with a set-valued instance functor.Source: §3.4 · p. 111

3.4.1 Pulling back data along a functor

• Precomposing a set-valued instance with a schema functor pulls the data back to the source schema; the example maps a discrete dynamical system instance to a graph.In the example, both Gr objects map to State, while source maps to the identity and target maps to next.Source: §3.4.1 · pp. 112–114

3.4.2 Adjunctions

• The data-migration functor ∆ has both a left adjoint, Σ, and a right adjoint, Π.The text states that these adjoints exist for the migration functor from Definition 3.68.Source: §3.4.2 · p. 114
• An adjunction is a natural isomorphism between hom-sets for a pair of functors, relating morphisms into the right adjoint to morphisms out of the left adjoint.Galois connections between preorders are exactly adjunctions between their corresponding categories.Source: §3.4.2 · pp. 114–115

3.4.3 Left and right pushforward functors, Σ and Π

• Schema functors induce Δ, Σ, and Π migrations that together provide a framework for specifying and reasoning about complex database migrations.The example illustrates Δ copying rows, Σ taking a union, and Π selecting matching pairs; the passage notes that essentially all useful migrations can be built from these induced functors.Source: §3.4.3 · pp. 117–118

3.4.4 Single set summaries of databases

• For a schema C, Σ! and Π! turn an instance into a one-column set summary: Σ! groups connected entries, while Π! selects entries satisfying a criterion.The email example describes Σ! as listing connected components and Π! as selecting self-to-self emails; generally, Σ-operations are built from colimits in Set and Π-operations from limits.Source: §3.4.4 · pp. 118–119

3.5 Bonus: An introduction to limits and colimits

• Limits turn a diagram functor into an object, while colimits encompass constructions such as products and Π! summaries, and disjoint unions and Σ! summaries, respectively.The section identifies meets in a preorder with limits and joins with colimits.Source: §3.5 · p. 119

3.5.1 Terminal objects and products

• A terminal object receives exactly one morphism from every object, and a product is an object with projections that receives a unique map from any object mapping to both factors.In Set, a singleton is terminal and the usual Cartesian product satisfies the product property; all terminal objects in a category are isomorphic.Source: §3.5.1 · pp. 120–121

3.5.2 Limits

• A limit of a diagram is a terminal object in its category of cones, unifying familiar constructions such as terminal objects and products under one definition.A cone consists of an object with compatible morphisms to each object in the diagram.Source: §3.5.2 · pp. 122–123
• A limit of a diagram is its terminal cone, whose object is the limit object and whose maps are the projection maps.Source: §3.5.2 · p. 123

3.5.3 Finite limits in Set

• Finite limits in Set select tuples satisfying each diagram-arrow constraint, allowing limits to express database queries.For the empty diagram, the limit is the singleton set containing the empty tuple.Source: §3.5.3 · p. 124

3.5.4 A brief note on colimits

• A colimit is defined dually as the colimit cocone obtained by taking the limit of the opposite diagram in the opposite category.The text postpones a fuller treatment of colimits until Chapter 6, where it discusses electric circuits.Source: §3.5.4 · pp. 125–126

3.6 Summary and further reading

• A database schema can be modeled by a category, and filling it with data corresponds to a functor from that category to Set.The chapter describes this as a database perspective on categories.Source: §3.6 · p. 126
• The chapter identifies coherence conditions as requirements that structures fit together and presents universal constructions as seeking a best solution via a limit or colimit.It notes that data migration also fits this form through Kan extensions.Source: §3.6 · pp. 126–127

4.1 Can we build it?

• Co-design diagrams factor hierarchical projects into interdependent subproblems whose feasibility relations can be composed to assess the whole design.Teams may plan independently, but resource dependencies and design-change notices can ripple through a project and cause failure.Source: §4.1 · pp. 129–131

4.2 Enriched profunctors

• The chapter develops abstract machinery for treating co-design problems as a category and replacing preorder design spaces with other enriched categories.Source: §4.2 · p. 131

4.2.1 Feasibility relationships as Bool-profunctors

• Feasibility relations are Bool-profunctors, and the quantale structure underlying Bool also lets other quantales, such as Cost, interpret co-design diagrams.A feasibility relation is monotone: feasible production remains feasible for less output or with more resources.Source: §4.2.1 · pp. 132–133

4.2.2 V-profunctors

• A V-profunctor is defined for V-categories over a unital commutative quantale, generalizing the Bool case to enriched settings.For Bool, profunctors can be pictured as bridges connecting points in two preorders.Source: §4.2.2 · pp. 133–134

4.2.3 Back to co-design diagrams

• In co-design diagrams, each box relates the product preorder of its produced resources to the product preorder of its required resources.The section illustrates this interpretation with a movie-design feasibility relation between tone and entertainment value on one side and cost on the other.Source: §4.2.3 · p. 136

4.3 Categories of profunctors

• Feas has preorders as objects and feasibility relations as morphisms, with composition and identities required to satisfy associativity and unitality.Source: §4.3 · p. 137

4.3.1 Composing profunctors

• The composition discussion sets up composing two feasibility relations in series, illustrated by relations between three preorders represented as matrices.Source: §4.3.1 · pp. 137–138
• Profunctor composition aggregates the possible ways through intermediate objects, generalizing the Boolean feasibility example to arbitrary unital commutative quantales.In the Boolean case, this is a big OR over possible way-points; composing feasibility relations with a unit leaves them unchanged.Source: §4.3.1 · p. 138, §4.3.2 · p. 140

4.3.2 The categories V-Prof and Feas

• For any skeletal quantale V, V-categories and V-profunctors form a category ProfV under profunctor composition, with unit profunctors and associative composition.For non-skeletal quantales, one can use isomorphism classes of profunctors or relax the category laws to hold up to isomorphism.Source: §4.3.2 · pp. 139, 140, 142

4.3.3 Fun profunctor facts: companions, conjoints, collages

• A V-functor yields a companion and a conjoint, while a profunctor’s collage forms a V-category containing its source and target objects with inclusions from both.The companion and conjoint use the target category’s hom-values; the collage takes the disjoint union of the objects and incorporates the profunctor.Source: §4.3.3 · pp. 142–143

4.4 Categorification

• The chapter aims to define compact closed categories and feedback-style wiring diagrams, then show that V-profunctors form a compact closed category interpreting the co-design diagrams.This continues the story of co-design and extends to V-profunctors in general.Source: §4.4 · pp. 144–145

4.4.1 The basic idea of categorification

• The section introduces categorification as adding structure so former properties become structures, while recovering the original concept by forgetting that structure.There is no prescribed categorification; its success is often empirical, depending on whether the added structure yields insight into the subject being modeled.Source: §4.4.1 · pp. 145–146

4.4.2 A reflection on wiring diagrams

• Categorified preorder wiring diagrams label boxes with morphisms, and category associativity and unitality make composition and wire lengthening or shortening unambiguous.Associativity makes alternative bracketings agree, while identity morphisms can be inserted or discarded.Source: §4.4.2 · pp. 146–147
• Symmetric monoidal categories model labelled boxes with typed inputs and outputs, whose composition and monoidal product combine them into diagrams interpreted unambiguously by coherence laws.Source: §4.4.2 · pp. 147–148

4.4.3 Monoidal categories

• Symmetric monoidal categories equip a category with a product, unit, and natural isomorphisms for unit, associativity, and swapping, constrained by coherence laws.For Set, associativity is an isomorphism rather than equality, requiring bookkeeping; Mac Lane’s coherence theorem allows diagrams to be treated as strict when useful.Source: §4.4.3 · pp. 148–149

4.4.4 Categories enriched in a symmetric monoidal category

• A V-category specifies objects, V-valued hom-objects, identity and composition morphisms, subject to associative and unital laws.This categorifies the earlier V-category notion: when V is a symmetric monoidal preorder, properties such as identity existence become choices of structure.Source: §4.4.4 · pp. 150–151

4.5 Profunctors form a compact closed category

• Compact closed categories extend symmetric monoidal categories with feedback, formally interpreting wiring diagrams used in co-design and appearing in fields such as quantum mechanics and dynamical systems.Caps and cups allow wires to reverse direction, with arrows recording their orientation.Source: §4.5 · p. 152

4.5.1 Compact closed categories

• Compact closed categories add dual objects, units, and counits to symmetric monoidal categories, enabling wires to bend between inputs and outputs.For every object c, a dual c* has unit I → c* ⊗ c and counit c ⊗ c* → I satisfying the snake equations; Corel is an example in which every finite set is its own dual.Source: §4.5.1 · pp. 153, 155

4.5.2 Feas as a compact closed category

• For any skeletal quantale V, ProfV is compact closed, with the product of V-categories as its monoidal product.Feas is the ProfBool instance; its compact closed structure gives mathematical semantics to co-design wiring diagrams.Source: §4.5.2 · pp. 155–156
• In ProfV, each V-category X has dual Xop, with unit and counit profunctors both defined by X(x, x′).The unit is ηX : 1 → Xop × X, and the counit is ϵX : X × Xop → 1.Source: §4.5.2 · p. 157

4.6 Summary and further reading

• V-profunctors extend beyond preorders: they can be defined for any symmetric monoidal category V, with related concepts discussed in [Shu08] [Shu10].The exposition also covers equipments, companions and conjoints, and symmetric monoidal bicategories.Source: §4.6 · p. 157
• Symmetric monoidal bicategories are a categorification of symmetric monoidal categories, with categorification discussed in and examples in [CY96].The passage characterizes symmetric monoidal bicategories as a sort of categorification.Source: §4.6 · p. 157
• Wiring diagrams are central to applied category theory, and their formalization for monoidal categories is presented in.A quick introduction to monoidal categories is available in.Source: §4.6 · p. 157
• Compact closed categories are one kind of structured monoidal category; [Sel10] introduces other flavors through their styles of wiring diagram.Source: §4.6 · p. 158

5.1 Comparing systems as interacting signal processors

• Signal-flow graphs support evaluating and comparing composite input-output behavior, and recast matrix operations graphically with functorial semantics as matrices.The diagrams model signal processing, with signal-flow graphs described as having functorial semantics as matrices.Source: §5.1 · pp. 160–161

5.2 Props and presentations

• Props use natural numbers as objects generated by one object, making unlabeled wires suitable for diagrams with a single wire type.A prop is a symmetric strict monoidal category whose objects are natural numbers and whose monoidal product on objects is addition.Source: §5.1 · pp. 160–161, §5.2 · p. 161

5.2.1 Props: definition and first examples

• A prop is a symmetric strict monoidal category with objects N, unit 0, and object-level monoidal product given by addition.Each natural-number object is the corresponding number of tensor copies of the generating object 1.Source: §5.2.1 · p. 161

5.2.2 The prop of port graphs

• Port graphs connect external inputs and outputs through vertex ports by a bijection, require acyclic internal flow, and compose and tensor to form the prop PG.Composition joins graphs across shared interfaces, while the monoidal product takes disjoint unions.Source: §5.2.2 · pp. 163–165

5.2.3 Free constructions and universal properties

• Free structures add only constraints forced by the specified structure, with freeness characterized by maps out; the free category on a graph has its paths as morphisms.For a free preorder, any function respecting the generating relation extends to a monotone map from the resulting preorder.Source: §5.2.3 · pp. 165–166

5.2.4 The free prop on a signature

• A prop signature specifies generators and their input and output arities; Free(G) has G-labeled port graphs as morphisms, with composition and monoidal structure inherited from port graphs.A labeling is valid when each vertex’s arities match those of its assigned generator.Source: §5.2.4 · pp. 167–168
• Free props represent morphisms through port graphs or expressions built from generators, identities, symmetries, composition, and monoidal product, with only prop axioms identifying expressions.The free prop is also characterized by a universal property: prop functors out correspond to generator assignments with matching arities.Source: §5.2.4 · pp. 168–170

5.2.5 Props via presentations

• Prop presentations impose equations between same-arity expressions, quotienting by those equations and the symmetric strict monoidal category axioms.Maps from the presented prop correspond to generator assignments that preserve arities and satisfy the imposed equations.Source: §5.2.5 · pp. 170–171

5.3.1 Rigs

• A rig models signal amplification and addition using a commutative additive monoid, a multiplicative monoid, distributivity, and zero absorption.Signals can be added before amplification or amplified separately and then added, with the same result.Source: §5.3.1 · p. 171

5.3.2 The iconography of signal flow graphs

• 15x and 3x + 21y are the outputs for inputs x and y in the illustrated graph, and summing path amplifications explains each input’s contribution.Graphs depict amplification, copying, discarding, addition, and the zero signal; prop equations can identify distinct graphs with the same behavior.Source: §5.3.2 · pp. 173–175

5.3 Simplified signal flow graphs

• Simplified signal flow graphs are morphisms in the free prop generated by the graph icons, while the usual form with feedback is deferred to Section 5.4.3.Their semantics arise by adding equations that identify graphs with the same behavior on signals.Source: §5.3.2 · p. 175

5.3.3 The prop of matrices over a rig

• Matrices over a rig can be assembled into a prop, where composing an (m × n)-matrix with an (n × p)-matrix yields an (m × p)-matrix.Each matrix is a function from its row-column index set to rig values.Source: §5.3.3 · p. 176
• For a rig R, Mat(R) has morphisms that are R-valued matrices, composed by matrix multiplication and combined in parallel by block-matrix direct sum.The text calls combinations of multiplication and direct sum interconnections of matrices.Source: §5.3.3 · p. 176

5.3.4 Turning signal flow graphs into matrices

• Theorem 5.53 gives a prop functor from signal flow graphs to matrices, and each matrix entry records how much an input contributes to an output.The functor’s interpretation agrees with path-based amplification, with composition corresponding to matrix multiplication and parallel composition to direct sum.Source: §5.3.4 · pp. 178–179

5.3.5 The idea of functorial semantics

• Functorial semantics computes a large graph’s matrix by composing the matrices of its parts, which can be faster than tracing paths.The process splits the graph into pieces, interprets each piece, then combines them by matrix multiplication and direct sum.Source: §5.3.5 · p. 180

5.4 Graphical linear algebra

• Graphical linear algebra extends these methods and can graphically prove control-theory conjectures that required elaborate matrix-algebra arguments [FSR16].Source: §5.4 · p. 180

5.4.1 A presentation of Mat(R)

• Theorem 5.60 presents Mat(R) using the signal-flow generators and equations, so two graphs represent the same matrix exactly when the equations and prop axioms transform one into the other.Every matrix can be represented by a signal flow graph; the construction arranges copy/discard, scalar, swap/identity, and addition/zero layers.Source: §5.4.1 · pp. 181–182

5.4.2 Aside: monoid objects in a monoidal category

• The equations for Mat(R) include the axioms of a commutative monoid, making the generating triple a commutative monoid object in Mat(R).The broader equation set also contains structures such as (co)monoids, Frobenius algebras, and Hopf algebras.Source: §5.4.2 · p. 184

5.4.3 Signal flow graphs: feedback and more

• Signal flow graphs represent every matrix and solution sets of linear equations, including kernels and images; conversely, every linear relation can be represented by a signal flow graph.Their behaviors are linear relations, so the graphs provide a uniform, compositional language for linear algebra.Source: §5.4.3 · pp. 188–189
• A sound and complete presentation for linear relations yields a graphical method for linear algebra: an equation between linear subspaces holds exactly when it follows from the presentation’s equations.Its generators extend those for signal flow graphs with their mirrored icons, and its equations include the matrix presentation’s equations plus additional ones.Source: §5.4.3 · p. 189
• The prop RelR is compact closed, with every object n dual to itself.The cup and cap behaviors establish self-duality for 1, and their monoidal products establish it for every object.Source: §5.4.3 · pp. 189–190
• A car-speed control problem is framed as choosing coefficients a and b so a signal-flow system’s behavior approximates the relation {(F, u, v) | u = v}.The system uses the rig R[s, s^-1], with s interpreted as integration and s^-1 as differentiation.Source: §5.4.3 · p. 190

5.5 Summary and further reading

• The chapter presents props as a way to formalize signal flow graphs and gain a new perspective on linear algebra, using universal properties to build suitable free and presented structures.Its central idea is separating syntax from semantics and relating them by a functor, an approach identified as functorial semantics.Source: §5.5 · pp. 190–191

6.1 The ubiquity of network languages

• Network diagrams may be undirected, but categorical constructions can capture their compositionality and allow directedness to be dropped when convenient.Hypergraph categories add spiders that connect wires and fuse when they share a leg; operads can tailor algebraic structures and encode wiring diagram languages.Source: §6.1 · pp. 194–196

6.1. THE UBIQUITY OF NETWORK LANGUAGES

• Universal constructions such as colimits can model interconnection, and cospans package colimits as composition and monoidal product; wiring diagrams are strongly connected to cospans.This provides a common structure for comparing network diagram languages and their mathematical models.Source: §6.1 · pp. 193, 195

6.2 Colimits and connection

• Colimits in FinSet merge sets according to functions that designate which elements should be considered the same.This concrete account supports the chapter’s use of colimits to formalize connection.Source: §6.1 · p. 195, §6.2 · p. 196

6.2.1 Initial objects

• An initial object has a unique morphism to every object; in FinSet, the empty set is initial because there is a unique function from it to any finite set.Source: §6.2.1 · p. 197

6.2.2 Coproducts

• Coproducts generalize joins in preorders and are disjoint unions in FinSet and Set, with a unique map into any object receiving maps from both summands.Source: §6.2.2 · p. 198

6.2.3 Pushouts

• Pushouts combine sets by identifying specified elements across them, generalizing ordinary unions; in FinSet they can be represented by equivalence classes of the disjoint union.Each element of the shared domain connects its images, and the pushout is the set of connected components.Source: §6.2.3 · pp. 200–202
• For the stated floor maps, the pushout is a one-element set.The maps identify every element of both sets with the same element in the pushout.Source: §6.2.3 · pp. 202–203

6.2.4 Finite colimits

• A category has all finite colimits exactly when it has an initial object and all pushouts, or all coequalizers and finite coproducts.Finite colimits in Set can be constructed as quotients of coproducts, identifying elements related by diagram arrows.Source: §6.2.4 · pp. 204–205
• The circuit interconnection coequalizer is a three-element set, with one element for each newly connected pair of terminals.The colimit describes the terminals after interconnection; the circuit components are left out at this stage.Source: §6.2.4 · p. 206

6.2.5 Cospans

• In a category with finite colimits, cospans compose via pushouts and form a symmetric monoidal category with coproduct as product.Cospan morphisms are equivalence classes of cospans; the monoidal unit is the initial object.Source: §6.2.5 · p. 208

6.3 Hypergraph categories

• A hypergraph category is a symmetric monoidal category whose wiring diagrams are networks, and electric circuits can be organized in one.Source: §6.3 · p. 209

6.3.1 Frobenius monoids

• Two morphisms built from Frobenius operations are equal if and only if their string diagrams connect the same ports.A Frobenius structure combines commutative monoid and cocommutative comonoid structures with Frobenius and special laws.Source: §6.3.1 · pp. 210–211
• Connected morphisms built from Frobenius spiders and symmetries are determined by their numbers of inputs and outputs, and the Frobenius axioms present CospanFinSet.These structures capture the grammar of circuit diagrams through splitting, merging, initializing, and terminating wires.Source: §6.3.1 · pp. 211–212

6.3.2 Wiring diagrams for hypergraph categories

• Hypergraph-category wiring diagrams are network diagrams that allow wires to split, join, terminate, and initialize, making them general enough for circuit diagrams.Source: §6.3.2 · p. 213

6.3.3 Definition of hypergraph category

• Hypergraph categories equip each object with a Frobenius structure compatible with tensor, include Corel and linear relations, and are self-dual compact closed.Source: §6.3.3 · pp. 213, 215

6.4 Decorated cospans

• The section uses symmetric monoidal functors and decorated cospans to construct a hypergraph category whose morphisms are electric circuits.This approach connects colimits, cospans, circuits, and hypergraph categories.Source: §6.4 · p. 215

6.4.1 Symmetric monoidal functors

• A symmetric monoidal functor consists of a functor and coherence maps compatible with the monoidal structures; it is strong when those maps are isomorphisms.Source: §6.4.1 · p. 216

6.4.2 Decorated cospans

• For a category C with finite colimits and a symmetric monoidal functor F, F-decorated cospans form a hypergraph category whose structures derive from CospanC.An F-decorated cospan pairs a cospan with a decoration from F of its apex.Source: §6.4.2 · pp. 218–219

6.4.3 Electric circuits

• Circuit components label graph edges, while Circ assigns circuits to finite vertex sets and combines them over disjoint unions to provide the decoration functor for a hypergraph category.Source: §6.4.3 · pp. 219–221
• Composing open circuits composes their cospans and combines their decorations, while monoidal products take disjoint unions of cospans and decorations.The decoration for composition is formed by taking the disjoint circuit decoration and mapping it along the copairing of the pushout maps.Source: §6.4.3 · pp. 221–222

6.5 Operads and their algebras

• Operads provide a grammar of composition whose algebras describe applications obeying that grammar.The section introduces operad functors O → Set as a way to build algebraic structures from operads.Source: §6.5 · p. 223

6.5.1 Operads design wiring diagrams

• Operads model composition without assigning boxes left and right ports, avoiding domain-and-codomain distinctions that are not inherent to circuits.An operad specifies types, operations for tuples of types, substitution, and identity operations, subject to generalized identity and associativity laws.Source: §6.5.1 · pp. 224–225

6.5.2 Operads from symmetric monoidal categories

• The Cospan operad represents operations as wiring diagrams, with substitution inserting one diagram into another; every symmetric monoidal category also yields an underlying operad.In the underlying operad, objects are types and morphisms from tensor products to an object are operations.Source: §6.5.2 · pp. 227–228

6.5.3 The operad for hypergraph props

• An operad functor maps types and operations while preserving composition and identities; Set-valued functors from operads are also of interest.For each operation in the source operad, the functor specifies an operation of the corresponding mapped arity in the target.Source: §6.5.3 · p. 229
• An operad algebra assigns each wiring-diagram type a set of fillers and each wiring diagram an operation that composes inputs into an output.For circuits, the operation combines circuits with specified interfaces into a circuit with the resulting boundary.Source: §6.5.3 · pp. 229–230
• Cospan-algebras are equivalent to hypergraph props and, unlike decorated cospans, can produce any hypergraph category.The operad approach also allows the operad itself to vary, yielding different compositional rules.Source: §6.5.3 · p. 230
• Operads can enforce wiring-diagram constraints more specific than category axioms, and operads themselves can be characterized as algebras for an operad [Lei04, Example 2.2.23].They conclude a progression from preorders to categories, monoidal categories, and operads.Source: §6.5.3 · p. 230

6.6 Summary and further reading

• The chapter presents operads as a broader framework for compositional structures and points to applications in logic, databases, and dynamical systems [RS13] [VSL15].It also directs readers to further work on hypergraph categories and their applications, including electrical circuits [BF15] and Markov processes and chemistry [BFP16] [BP17].Source: §6.6 · pp. 230–231

7.1 How can we prove our machine is safe?

• A system’s possible behavior is determined by its components’ behaviors and interactions, allowing whole-system properties to be proved from component properties.The chapter aims to formalize component relationships in a logical language so standard proof techniques can combine subsystem properties.Source: §7.1 · pp. 233, 235

7.1. HOW CAN WE PROVE OUR MACHINE IS SAFE?

• The chapter proposes a behavior-specific formal language: BT is a topos whose objects are behavior types, with sheaves providing semantics for properties proved in its internal language.Behavior types are roughly sets whose elements change through time; in BT, structures such as graphs and groups likewise change through time.Source: §7.1 · p. 235

7.2 The category Set as an exemplar topos

• Set illustrates how predicates correspond to subsets and logical operations to set operations, with limits and colimits providing structures used to define those operations.The chapter uses Set to build intuition for toposes, which retain enough Set-like structure for logic while supporting more complex semantics.Source: §7.2 · pp. 236–237

7.2.1 Set-like properties enjoyed by any topos

• Every topos has all limits and colimits, is cartesian closed, admits epi-mono factorizations, and has a subobject classifier.When a square is a pullback, Proposition 7.3 states that the adjacent square is a pullback exactly when the corresponding rectangle is.Source: §7.2.1 · pp. 237, 239

7.2.2 The subobject classifier

• A subobject classifier translates subobjects of any object Y into maps Y → Ω and back, so subobjects can be understood as predicates on Y.In Set, subsets correspond to Boolean-valued functions that return true exactly for elements in the subset.Source: §7.2.2 · pp. 240–241
• In Set, every subset is classified by a predicate to B, and the characteristic map of {(true, true)} defines AND.The review identifies ∧, ∨, ⇒, and ¬ as maps on truth values in a topos.Source: §7.2.3 · pp. 242–243

7.2.3 Logic in the topos Set

• In Set, the subobject classifier B supports logical connectives as operations on truth values, with AND obtained as the characteristic function of {(true, true)}.For a general topos, the text describes ∧, ∨, and ⇒ as maps Ω× Ω→Ω, and ¬ as a map Ω→Ω.Source: §7.2.3 · pp. 242–243

7.3 Sheaves

• A sheaf is described intuitively as a kind of thing that can happen on a space, with points and regions serving as perspectives on it.The text relates this perspective to databases: a schema acts as the site, and its category of instances is a topos.Source: §7.3 · p. 244

7.3.1 Presheaves

• A presheaf on a small category C is a functor C^op→Set, assigning sections to objects and restriction maps to morphisms.Presheaves on the arrow-shaped category correspond to directed graphs; presheaves and sheaves differ by the covering information sheaves take into account.Source: §7.3.1 · pp. 244–246

7.3.2 Topological spaces

• A topology on X specifies open subsets, closed under binary intersections and arbitrary unions and including X; its opens form a preorder under inclusion.A cover of U is a collection of opens whose union is U.Source: §7.3.2 · pp. 246, 248

7.3.3 Sheaves on topological spaces

• Sheaves on a topological space are presheaves on its preorder of open sets that satisfy a special property called the sheaf condition.The section begins introducing matching families and gluing as stages toward defining that condition and the category of sheaves.Source: §7.3.3 · pp. 248–249
• A sheaf is a presheaf whose matching sections on every open cover glue uniquely; continuous sections of a map give examples, including vector fields as sections of tangent bundles.A vector field over an open set continuously assigns a tangent vector to each point in that set.Source: §7.3.3 · pp. 249, 253

7.4 Toposes

• Every topos has limits and colimits, cartesian closure, epi-mono factorizations, and a subobject classifier, letting logical operations act on sub-sheaves rather than only subsets.Sheaf categories on topological spaces and database-instance categories are examples of toposes.Source: §7.4 · pp. 254–255

7.4.1 The subobject classifier Ωin a sheaf topos

• In Shv(X, Op), Ω assigns each open U the open subsets of U, so truth values are regions where a property holds, not merely yes or no.The property is fully true when its open truth value is X and false when it is empty.Source: §7.4.1 · pp. 255–256

7.4.2 Logic in a sheaf topos

• In sheaf-topos logic, conjunction and disjunction are intersection and union, implication is the largest open R with R ∩ U ⊆ V, and negation is the interior of U’s complement.Negation is defined as U ⇒ false.Source: §7.4.2 · p. 257
• Open sets interpret logical connectives, which can be used to reason about where vector fields have properties such as being gradients or non-zero.Predicates can identify the largest open set where a vector field has the specified property.Source: §7.4.2 · pp. 258–259

7.4.3 Predicates

• A predicate on a sheaf S is a morphism S→Ω assigning each section an open-set truth value; predicates form a Heyting algebra with logical operations computed pointwise.The order on predicates is implication, tested by inclusion of their truth-value open sets.Source: §7.4.3 · pp. 259–260

7.4.4 Quantification

• Universal quantification returns the largest open subset where a predicate holds for every local T-section; existential quantification unions opens with local witnesses, which need not form one global witness.The existential quantifier accounts for a cover of the open set by domains of local sections.Source: §7.4.4 · pp. 261–262

7.4.5 Modalities

• A modality is a sheaf morphism Ω→Ω satisfying the stated modality properties; examples send q to p⇒q, p∨q, or (q⇒p)⇒p.The text identifies modalities with closure operators on the posets of predicates.Source: §7.4.5 · p. 262

7.4.6 Type theories and semantics

• In every topos, the internal-language condition for an epimorphism translates to surjectivity: database rows have matching images, while sheaf sections lift locally over an open cover.For sheaves, each section on an open set must have matching sections on an open cover of that set.Source: §7.4.6 · pp. 263–264

7.5 A topos of behavior types; 7.5.1 The interval domain

• The topos of behavior types is Shv(IR), where IR has finite closed intervals as points and basic opens o[a,b] consist of intervals [d,u] with a<d≤u<b.Open sets are unions of these basic opens.Source: §7.5.1 · p. 264, §7.5 · p. 265

7.5. A TOPOS OF BEHAVIOR TYPES

• The subspace topology on the real numbers R⊆IR agrees with the usual topology on R.Source: §7.5 · p. 265

7.5.2 Sheaves on IR

• A sheaf on IR assigns a set of events to each open set, with restriction maps describing the same event on smaller open subsets.An element over U represents an event taking place throughout U.Source: §7.5.2 · p. 265
• Sheaves on IR, called behavior types, can represent interval-based behaviors, including hybrid systems with continuous motion and discrete jumps.The chapter also describes sheaves for constant values and local continuous functions, and presents hybrid systems as another source of examples.Source: §7.5.2 · pp. 265–266

7.5. A TOPOS OF BEHAVIOR TYPES

• Truth values in the sheaf topos are open time intervals, and IR is needed because a proposition may hold on overlapping intervals without holding throughout their union.Examples include a single watcher remaining at a post and the stock market not falling by more than 10 points.Source: §7.5.2 · p. 266, §7.5 · p. 267

7.5.3 Safety proofs in temporal logic

• Behavior contracts are predicates on behavior-type variables; the logic records where they hold, and can derive safe separation if the pilot, airplane, and at least one radar uphold their contracts.One example contract requires engaging the thrusters within one second of the dials indicating a bad position; the safety reasoning is developed in [SS18].Source: §7.5.3 · pp. 267–268

7.6 Summary and further reading

• Temporal sheaves fit into a topos with higher-order logic for reasoning about how they work together in larger systems, building on topos theory and domain theory.A more detailed version of this account appeared in [SS18].Source: §7.6 · p. 268

Function properties

• Translations preserve order and metric, while scaling by 2 fails to preserve the metric and adding 1 fails to preserve addition; scaling by 3 preserves addition.The examples test each property directly using its defining inequality or equation.Source: §A.1 · p. 271

Partitions

• For partitions, the join of (12)(3)(4) and (13)(2)(4) is (123)(4), and the partitions of a set correspond to surjections from that set.The join is above both input partitions and is below each common upper bound; the coarsest and finest partitions correspond to the unique map to {1} and the identity map, respectively.Source: §A.1 · pp. 272, 274, 275

Functions and sets

• A function to the empty set exists only when its domain is empty; examples distinguish injective, surjective, and bijective functions from relations that are not functions.The solutions also enumerate subsets and Cartesian-product elements in basic set exercises.Source: §A.1 · pp. 272–273

Upper sets

• Upper sets are closed upward, and the map sending an element to its principal upper set reverses order; inverse image along a function corresponds to composing the upper-set classifier with that function.For a discrete preorder, every subset is an upper set, so its upper-set collection is the power set.Source: §A.1 · pp. 275–277

Preorders and monotone maps

• In preorders, identity maps and composites of monotone maps are monotone, every map from a discrete preorder is monotone, and a skeletal dagger preorder is discrete.The solutions also describe a preorder obtained from reachability by paths in a directed graph.Source: §A.1 · pp. 276–277

Bounds and meets

• The solutions establish 0 as the greatest lower bound of {1/(n+1) | n ∈ N}, and show that a singleton’s meet and join are its sole element.They also prove uniqueness of meets in a partial order and state the corresponding join facts by reversing the order.Source: §A.1 · p. 277

A.1 Solutions for Chapter 1.

• In the natural-number divisibility order, meet and join are gcd and lcm; multiplication by 3 has floor division by 3 as right adjoint, while ceiling division by 3 has no left adjoint.The no-left-adjoint argument derives a contradiction from the adjunction condition at z = 1 and positive r approaching zero.Source: §A.1 · pp. 277–278
• The finite-order checks confirm one pair is adjoint in all nine cases, while a different pair fails because f(2) ≰ 1 but 2 ≤ 1(1).A second worked table verifies the adjunction condition for the rounding map across twelve pairs.Source: §A.1 · pp. 278, 280
• Worked partition examples compute pushforwards and pullbacks, with the chosen partition c satisfying c ≤ 1*(d) but not c ≤ 1*(e).The examples distinguish a partition coarser than the pushforward of c from one that is not.Source: §A.1 · p. 279
• Adjunctions can be characterized by the unit and counit inequalities; right adjoints are unique, and left adjoints preserve joins.The solutions also show that the composite of a left and right adjoint has the stated unit inequality and idempotent behavior.Source: §A.1 · pp. 279–281
• For a projection map, the solutions calculate inverse images, direct images, and universal-image examples for selected subsets.The listed cases include f*(B1) = {a1}, f*(B2) = {c1, c2}, and f!(A2) = {a, c}.Source: §A.1 · pp. 280–281
• The preorder examples compute the upward closure and closures of two relations, showing one closure is contained in the preorder and the other is not.The solutions also enumerate example relations on pairs drawn from {1, 2}.Source: §A.1 · p. 281

• The proposed operation fails monotonicity: the inputs satisfy the order conditions, but the resulting product inequality does not hold.The counterexample uses x1 = −1, x2 = 0, y1 = −1, and y2 = 1.Source: §A.2 · p. 282

Exercise 2.33

• The divisibility proposal is not monotonic: 1|1 and 1|2, but (1 + 1) ∤ (1 + 2).Source: §A.2 · p. 282

Exercise 2.43

• The map 1 is a strict monoidal monotone because its conditions (a) and (b) hold as equalities.The solution also establishes that 1 is monotonic.Source: §A.2 · p. 283

Exercise 2.63

• A W-category’s hom-object can represent the maximum cargo weight allowed on a route, computed as the maximum over paths of each path’s minimum edge limit.The diagonal hom-objects are infinite, and the limit from x to z is at least the minimum of the limits along x to y and y to z.Source: §A.2 · p. 285

Exercise 2.94

• The powerset monoidal preorder (P(S), ⊆, S, ∩) is a quantale, with hom-object B ⊸ C given by the complement of B union C and joins given by union.Source: §A.2 · p. 287

A.2 Solutions for Chapter 2.

• The solution to Exercise 2.104 uses Proposition 2.87(2), symmetry, and associativity, then follows Eq. (2.101).The displayed steps include results involving v ⊗ a and (M ∗ (N ∗ P))(w, z).Source: §A.2 · pp. 287–288
• Applying Eq. (2.101), the displayed zero-tensor expression reduces to M(x, y).The supplied passage shows the result as M(x, y) ∨ 0 = M(x, y).Source: §A.2 · p. 288
• The section then begins the solution to Exercise 2.105, but supplies no solution details here.Source: §A.2 · p. 288

A.3. SOLUTIONS FOR CHAPTER 3

• The free category on the chain graph has 1 + 2 + · · · + n morphisms, since it has n − i paths of length i for 0 ≤ i ≤ n.Path concatenation adds lengths, and identities are exactly the paths of length 0.Source: §A.3 · pp. 289–291
• The first graph has ten paths, with A # f # h parallel to A # 1 # i, while A is parallel to none of the other nine.In the second diagram, A # f # h = j = A # 1 # i.Source: §A.3 · p. 290
• Between two sets of n elements there are n! isomorphisms; the example monoid generated by s is not a group, whereas the category with s inverse to itself is a group.The inverse of the displayed function sends 1 to b, 2 to a, and 3 to c.Source: §A.3 · p. 291
• A functor from the nine-morphism category sends both f′ # h′ and 1′ # i′ to f # h, while identity and composition are preserved by identity and composite functors.The solutions verify composite-functor preservation by applying the component functors successively to identities and composable morphisms.Source: §A.3 · pp. 291–292
• A set-valued schema with an endomorphism squaring to the identity describes an involution, while a secret-Santa schema models people, gifts, giver and receiver maps, and self-gifters.The solutions also construct a natural transformation by composing its components and check naturality via the resulting commuting outer rectangle.Source: §A.3 · pp. 292–293
• For functors into a preorder, any two natural transformations with the same source and target are equal, because each component lies in a hom-set with at most one morphism.The converse is false: the solution gives distinct transformations from a category with two objects into the one-object preorder.Source: §A.3 · p. 293
• The canonical actions of −×B and (−)^B on functions are functorial, and currying addition gives the function n ↦ n + 3.The product action sends (x, b) to (f(x), b); the exponential action composes a function B → X with f.Source: §A.3 · p. 295
• In a preorder, a terminal object is a top element; the one-object category is terminal in Cat, while a discrete two-object category has none.The preorder criterion follows because there is at most one morphism between any two objects.Source: §A.3 · pp. 295–296
• Products in preorders are meets, and products of categories compose and act componentwise; products more generally are terminal objects in their cone categories.For two sets, the limit formula for a diagram with two objects and no arrows reduces to the usual Cartesian product.Source: §A.3 · pp. 296–297

A.4 Solutions for Chapter 4.

• A Bool-profunctor is a feasibility relation, while a profunctor can encode which tasks are possible given available knowledge.The knowledge example is an upper set: if a task is possible, any easier task is also possible.Source: §A.4 · p. 298
• For the cost example, shortest paths through the bridges D to y and y to r give (Φ # Ψ)(−, −) = X(−, D) + 9 + Z(r, −).The solutions also present matrix multiplication as an alternative way to compute the composite.Source: §A.4 · pp. 299–300
• For skeletal V-categories, F and G are adjoints exactly when their associated profunctors bF and qG are equal; the identity functor is adjoint to itself.The solutions also relate monoidal preorder definitions to enriched-category definitions by identifying the tensor operation's monotonicity with functoriality.Source: §A.4 · pp. 301–302
• Set-categories reproduce ordinary categories, with identity elements and composition functions satisfying unitality and associativity.In Cost-categories, the identity condition implies that each object's distance to itself is zero.Source: §A.4 · p. 302
• Products of resource preorders pair resources componentwise, and products of profunctors express conjunction: both outputs must be obtainable from their respective inputs.Source: §A.4 · p. 303
• The composite profunctor is the identity, establishing the first snake equation; the proof says the other equation is analogous.The calculation repeatedly uses that composing with the unit profunctor is the identity.Source: §A.4 · p. 304

A.5. SOLUTIONS FOR CHAPTER 5

• A function between preorders is monotone exactly when it preserves the generating relation; a monotone function need not preserve that relation pointwise in the reverse-direction example.For the counterexample, the source has one element and the generating relation on the target is empty.Source: §A.5 · p. 307
• The free-category construction and graph extraction are mutually inverse, yielding the adjunction Free : Grph ⇆ Cat : U with Free left adjoint to U.A functor from the free category is determined by its object assignment and the images of graph arrows; arbitrary paths map to composites.Source: §A.5 · pp. 307–308
• The free prop on generators is naturally isomorphic to the prop presented by the same generators with no relations.The only noted distinction is representing a set by singleton subsets in its quotient by the trivial equivalence relation.Source: §A.5 · p. 309
• Matrix multiplication over N is noncommutative in the given 2×2 example, and the described flow graph sends (x, y) to (16x + 4y, x + 4y).The example gives (A ∗ B)(1, 1) = 1 and (B ∗ A)(1, 1) = 0.Source: §A.5 · p. 309
• The four-layer signal-flow construction represents a matrix M, with copying, scalar multiplication, wire rearrangement, and summation implementing its entries.The solution states that the constructed diagram 1 satisfies S(1) = M.Source: §A.5 · pp. 310–311
• The diagrams with and without a left-to-right path cannot represent the same morphism, because the path-breaking equation requires a 0 scalar on that path.The passage notes that no such scalar occurs in the diagram, since sums and products of nonzero natural numbers remain nonzero.Source: §A.5 · p. 312
• Under U, a monoid object in Mat(R) gives R^m coordinatewise addition with the zero vector as unit; for m = 1 this is the additive monoid on R.The functor sends n to R^n and morphisms to matrix-vector multiplication.Source: §A.5 · pp. 312–313
• The reversed addition icon relates x to y and z when x = y + z, while the reversed copy icon relates a triple when its entries are equal.The relational compositions in the exercises reduce to equality of the corresponding function outputs, or to pairs of outputs from a common input.Source: §A.5 · p. 313
• The inverse of 0-reverse gives the kernel of a linear map, and the inverse of discard gives its image; linear relations remain linear under composition.The solutions show closure under scalar multiplication and addition for the composite of two linear relations.Source: §A.5 · pp. 313–314

A.6. SOLUTIONS FOR CHAPTER 6

• The examples characterize initial objects via unique maps: free categories have one when a vertex has a unique path to every object, and Rig has the natural numbers rig as initial object.The solutions also give preorder examples with none, one, or two initial objects, and state that a discrete category has an initial object exactly when its object set has one element.Source: §A.6 · pp. 315, 317
• In a preorder, coproducts are exactly joins: the least elements above both inputs.The universal property requires a coproduct to lie below every common upper bound.Source: §A.6 · p. 316
• Coproducts and an initial object provide the data for a symmetric monoidal category, constructed using their universal properties.The solutions define coproduct as a functor and construct its unit, associativity, and symmetry maps.Source: §A.6 · p. 317
• A pushout of sets can be described as equivalence classes generated by identifying elements that share an image; one example yields four classes.The example’s classes are {1, 1′, 3}, {2}, {4}, and {5, 2′, 3′}.Source: §A.6 · pp. 318–319
• The special cospan law holds because its square is a pushout, and the depicted morphisms are equal in the groups identified by the solutions.Morphisms 1, 4, and 6 are equal; morphisms 3 and 5 are equal; morphism 3 differs from the others.Source: §A.6 · pp. 319–320
• Every category of cospans in C is isomorphic to one formed using the constant singleton-valued functor, since each cospan then has a unique decoration.Composition in both categories is by pushout.Source: §A.6 · p. 321

A.7 Solutions for Chapter 7.

• When adjacent squares are pullbacks, the outer rectangle is a pullback, and the converse holds when the other square is also a pullback.The solutions establish both directions using the universal properties of the pullbacks.Source: §A.7 · pp. 324–325
• For a function between sets, being injective is equivalent to being a monomorphism.The proof uses maps from a one-element set to test injectivity, then applies injectivity pointwise to arbitrary maps.Source: §A.7 · p. 325
• In a preorder, a quantale with the stated properties is cartesian closed, but cartesian closed preorders need not have all joins.The solutions give Nop × Nop as an example with a top element, binary meets, and no bottom element, while the required hom-objects exist.Source: §A.7 · pp. 326–327
• For f, fibers over a, c, and d are {a1,a2}, {c1}, and ∅; section sets have six elements over {a,b,c}, none over {a,b,c,d}, and 12 over {a,b,d,e}.Source: §A.7 · p. 329
• Sections 11 and 12 disagree on the overlap of U1 and U2, so no section over U1 ∪ U2 restricts to both.Source: §A.7 · p. 330
• A unique graph homomorphism classifies G′, marking D, i, 1, and h missing and A, B, C, and f present.Source: §A.7 · p. 331
• For U = R − {0}, ¬U = ∅ and ¬¬U = R, so U ⊆ ¬¬U but ¬¬U ⊆ U is false.Source: §A.7 · p. 331
• For p(n,z) iff n ≤ |z|, ∀z holds on {0} ⊆ N, ∃z on N, ∀n on ∅ ⊆ Z, and ∃n on Z.Source: §A.7 · p. 332
• In the sheaf example, ∃(t:T).p(s,t) holds over the union of intervals where some news item worries s; the item may vary, and coverings shape this meaning.Source: §A.7 · p. 332
• The interval example places [2, 6] in o[0, 8] but in neither o[0, 5] nor o[4, 8].The solution says the membership formula holds for the first interval and fails for each of the latter two.Source: §A.7 · p. 333
• The topology on R induced by the interval domain is the usual topology on R.The solution proves each direction: subspace-open sets are usual-open, and usual-open sets are open in the subspace topology.Source: §A.7 · p. 333
• For any topological space X, H_X(U), the continuous functions U ∩ R → X, forms a presheaf by restriction and a sheaf by gluing functions that agree on overlaps.The solution defines H_X(U) as the set of continuous functions from U ∩ R to X.Source: §A.7 · p. 333

Index

• The supplied material lists index references for preorders and relations, but gives no Chapter 3 solution steps.The entries include preorder relations, partial orders, and relations (pp. 8–16), and presheaves (pp. 232–234).Source: Index · pp. 349–351