Skip to content

Notes Chapter 2 Part 2

Piotr Paradziński edited this page Apr 7, 2020 · 4 revisions

Symmetric monoidal preorder

A poset is a preorder that obeys:

  • if x ≤ y and y ≤ x then x = y (antisymmetry condition)

Fact: Every preorder is equivalent to a poset.

If we have preorder that is not a poset so exists A -> B and B -> A then, it is equivalent to poset where A and B are "collapsed" into a single object.

A monoidal preorder (P, ≤, e, ⊗) where:

  • (P, ≤) is preorder
  • ⊗ is a function ⊗ : PxP -> P such that
  • ⊗ is associative: a ⊗ (b ⊗ c) = (a ⊗ b) ⊗ c
  • ⊗ is unital: a ⊗ e = a = e ⊗ a
  • monotonicity condition holds: if a ≤ b and b ≤ c then a ⊗ b ≤ c ⊗ d

Examples of monoidal preorders:

  • Bool = ({true, false}, =>, T, and)
  • Cost = ([0, ∞], >=, 0, +)
  • Power set of X = (P(X), ⊆, X, ∩)

Wiring diagrams for monoidal preorder (P, ≤, e, ⊗)

  • element of P is represented as a label
  • ≤ is represented as a box
  • e (TODO we can omit?)
  • p ⊗ q are parallel lines from/to box

Monoidal preorder (P, ≤, e, ⊗) is symmetric when:

  • a ⊗ b ≤ b ⊗ a (symmetry condition).

Enriched categories

Let V = (P, ≤, e, ⊗) be a symmetric monoidal preorder (SMP) then a V-category is a

  • set V of objects
  • function c: V x V -> P

such that

  • e ≤ c(x,x) (identity condition)
  • c(x,y) ⊗ c(y,z) ≤ c(x,z) (composition condition)

Examples of V-categories:

  • when V is Bool - we have Bool enriched category - Can we get where we want?
  • when V is Cost - we have Cost enriched category - How much it will cost?
  • when V is Set (power set?) - we have Set enriched category - How many ways there is?

Preorders are Bool-enriched categories. TODO picture Mango, Peach, Strawbery, Banana
TODO table

(TODO In a way we have a change of base ?)

... in logic ... subobject clasifier ... TODO

Metric spaces

A metric space is:

  • a set X
  • a function d: (X,X) -> [0,∞)

such that:

  • d(x,x) = 0
  • d(x,y) = d(y,x)
  • d(x,y) + d(y,z) >= d(x,z)

Examples:

A cost category (Lawvere metric space) is:

  • a set X
  • a function d: (X,X) -> [0,∞)
    such that
  • 0 >= d(x,x)
  • d(x,y) + d(y,z) >= d(x,z)