1: Generative Effects - Orders and Adjunctions
( \newcommand{\kernel}{\mathrm{null}\,}\)
- 1.1: What is Order?
- Above we informally spoke of two different ordered sets: the order on system connectivity and the order on booleans false ≤ true. Then we related these two ordered sets by means of Alice’s observation Φ. Before continuing, we need to make such ideas more precise. We begin with a review of sets and relations and give the definition of a preorder—short for preordered set—and a good number of examples.
- 1.2: Meets and Joins
- As we have said, a preorder is a set P endowed with an order ≤ relating the elements. With respect to this order, certain elements of P may have distinctive characterizations, either absolutely or in relation to other elements. We have discussed joins before, but we discuss them again now that we have built up some formalism.
- 1.3: Galois Connections
- The preservation of meets and joins, and in particular issues concerning generative effects, is tightly related to the theory of Galois connections, which is a special case of a more general theory we will discuss later, namely that of adjunctions. We will use some adjunction terminology when describing Galois connections.