- Pos

Awodey:

Another kind of example one often sees in mathematics is categories of

structured sets, that is, sets with some further “structure” and functions that “preserve it,” where these notions are determined in some independent way.

A partially ordered set or

posetis a setAequipped with a binary relationa ≤such that the following conditions hold for all_{A}ba, b, c ∈ A:

- reflexivity: a ≤
_{A}a- transitivity: if a ≤
_{A}b and b ≤_{A}c, then a ≤_{A}c- antisymmetry: if a ≤
_{A}b and b ≤_{A}a, then a = bAn arrow from a poset

Ato a posetBis a function m: A => B that ismonotone, in the sense that, for all a, a’ ∈ A,

- a ≤
_{A}a’ implies m(a) ≤_{A}m(a’).

As long as the functions are *monotone*, the objects will continue to be in the category, so the “structure” is preserved. The category of posets and monotone functions is denoted as **Pos**. Awodey likes posets, so it’s important we understand it.

An example of poset is the `Int`

type where the binary operation of `≤`

is integer `<=`

just as it is defined with `PartialOrder`

typeclass.
Another example could be `case class LString(value: String)`

where `≤`

is defined by comparing the length of `value`

.

```
scala> :paste
// Entering paste mode (ctrl-D to finish)
case class LString(value: String)
val f: Int => LString = (x: Int) => LString(if (x < 0) "" else x.toString)
// Exiting paste mode, now interpreting.
defined class LString
f: Int => LString = <function1>
scala> f(0)
res0: LString = LString(0)
scala> f(10)
res1: LString = LString(10)
```

`f`

in the above is monotone since `f(0) ≤ f(10)`

, and any other pairs of `Int`

s that are `a <= a'`

.

herding cats — Pos