It looks like you're new here. If you want to get involved, click one of these buttons!

- All Categories 2.3K
- Chat 494
- ACT Study Group 5
- Azimuth Math Review 6
- MIT 2020: Programming with Categories 53
- MIT 2020: Lectures 21
- MIT 2020: Exercises 25
- MIT 2019: Applied Category Theory 339
- MIT 2019: Lectures 79
- MIT 2019: Exercises 149
- MIT 2019: Chat 50
- UCR ACT Seminar 4
- General 64
- Azimuth Code Project 110
- Drafts 1
- Math Syntax Demos 15
- Wiki - Latest Changes 1
- Strategy 110
- Azimuth Project 1.1K

Options

Show that the product of two preorders is a preorder.

## Comments

Let \(\mathcal{P} := \langle P, \preceq_P \rangle\) and \(\mathcal{Q} := \langle Q, \preceq_Q \rangle\). Define \(\mathcal{P} \times \mathcal{Q} := \langle P \times Q, \preceq_{P\times Q} \rangle\) where:

\[ (a,b) \preceq_{P\times Q} (c,d) \text{ if and only if } a \preceq_P c \text{ and } b \preceq_Q d \]

We need to check reflexivity and transitivity.

Reflexivity- Since \(a \preceq_P a\) and \(b \preceq_Q b\) then \((a,b) \preceq_{P \times Q} (a,b)\ \ \ \Box\)Transitivity- Let \((a,b) \preceq_{P \times Q} (c,d)\) and \((c,d) \preceq_{P \times Q} (e,f)\). Then we have \(a \preceq_P c \preceq_P e\) and \(b \preceq_Q d \preceq_Q f\).Since \(\preceq_P\) and \(\preceq_Q\) are transitive, then \(a \preceq_P e\) and \(b \preceq_P f\).

Hence \((a,b) \preceq_{P \times Q} (e,f)\ \ \ \Box\)

We can also show that this product order is the product in the category of preorders where the morphisms are order-preserving maps.

In fact, the category of preorders is

bicartesian closed. There's an initial preorder, a final preorder, products and coproducts and an exponential. If this is interesting we can go into this construction and the proof.`Let \\(\mathcal{P} := \langle P, \preceq_P \rangle\\) and \\(\mathcal{Q} := \langle Q, \preceq_Q \rangle\\). Define \\(\mathcal{P} \times \mathcal{Q} := \langle P \times Q, \preceq_{P\times Q} \rangle\\) where: \\[ (a,b) \preceq_{P\times Q} (c,d) \text{ if and only if } a \preceq_P c \text{ and } b \preceq_Q d \\] We need to check reflexivity and transitivity. _Reflexivity_ - Since \\(a \preceq_P a\\) and \\(b \preceq_Q b\\) then \\((a,b) \preceq_{P \times Q} (a,b)\ \ \ \Box\\) _Transitivity_ - Let \\((a,b) \preceq_{P \times Q} (c,d)\\) and \\((c,d) \preceq_{P \times Q} (e,f)\\). Then we have \\(a \preceq_P c \preceq_P e\\) and \\(b \preceq_Q d \preceq_Q f\\). Since \\(\preceq_P\\) and \\(\preceq_Q\\) are transitive, then \\(a \preceq_P e\\) and \\(b \preceq_P f\\). Hence \\((a,b) \preceq_{P \times Q} (e,f)\ \ \ \Box\\) -------------------------------- We can also show that this product order is the product in the category of preorders where the morphisms are order-preserving maps. In fact, the category of preorders is _bicartesian closed_. There's an initial preorder, a final preorder, products and coproducts and an exponential. If this is interesting we can go into this construction and the proof.`

Hi @MatthewDoty,

Yes, it's interesting, please go on. Thanks

`Hi @MatthewDoty, Yes, it's interesting, please go on. Thanks`

Okay, let's first prove that the product preorder is the Product in the category of preorders.

The classic presentation of products introduces them with this commuting diagram (which I've taken from wikipedia):

Let's turn this into some equational laws. I'll be roughly following Conal Elliot's Compiling to Categories (2017) and John Wiegley's formalization in Coq

A

Product\((\times)\) for a category \(\mathcal{C}\) has three components:morphism compositionoperation \((\triangle):(A \to B) \Rightarrow (A \to C) \Rightarrow A \to B \times C\) obeying the laws below(The reason for the two kinds of arrows is to distinguish between morphisms in the Category and functions in the meta-language. See the Conal Elliot and John Wiegley linked above for formulations with Haskell and Coq as the meta languages, respectively.)

I've seen \(\pi_1\) and \(\pi_2\) called

projections. John Wiegley refers to \((\triangle)\) as"fork"in his code, which seems a fine name to me.A product obeys the following laws:

\[ \pi_1 \cdot f \triangle g = f\\ \pi_2 \cdot f \triangle g = g\\ (\pi_1 \cdot f) \triangle (\pi_2 \cdot f) = f \]

In Haskell, using itself as its own meta-language, we have \((\times)\) is the type constructor

`(,)`

, \(\pi_1\) is`fst :: (a,b) -> a`

and \(\pi_2\) is`snd :: (a,b) -> b`

. Lastly, we have \((\triangle)\) is`Control.Arrow.(&&&)`

. You can check that`fst . (f &&& g) = f`

and`snd . (f &&& g) = g`

by looking at the instantiation of the`Arrow`

class for`(->)`

in base.So let's extend the definition of the product preorder \(\mathcal{P} \times \mathcal{Q}\) to a product by defining \(\pi_1\), \(\pi_2\) and \((\triangle)\).

These definitions are

verysimilar to the Haskell correlates. Checking the laws are obeyed is just evaluating the functions.It's a bit less trivial to check that \(\pi_1\), \(\pi_2\) and \(f \triangle g\) are all morphisms. In this case, we need them to be

order preserving maps.I'll try to find the time next week to show the other properties that make \(PreOrder\) Bicartesian closed. It's my opinion that it's important to learn the algebraic formulations of the category theoretic laws rather than just the traditional commuting diagrams. But thankfully we can always find correlates in Haskell, since

`(->)`

is also Bicartesian closed.I might do a little less proving, though. I think if we want to get serious about writing proofs we should consider formulating this stuff in

`Coq`

or`Lean`

. These systems really drive home the connection between CT and programming.[EDIT: Adding third law for products, fixing up proper usage of terms.] [EDIT2: Adding uniqueness constraint]

`Okay, let's first prove that the product preorder is the Product in the category of preorders. The classic presentation of products introduces them with this commuting diagram (which I've taken from [wikipedia](https://en.wikipedia.org/wiki/Product_(category_theory))): ![Product](https://upload.wikimedia.org/wikipedia/commons/b/b2/CategoricalProduct-03.png) Let's turn this into some equational laws. I'll be roughly following Conal Elliot's [Compiling to Categories (2017)](http://conal.net/papers/compiling-to-categories/compiling-to-categories.pdf) and John Wiegley's [formalization in Coq](https://github.com/jwiegley/category-theory/blob/master/Structure/Cartesian.v) A _Product_ \\((\times)\\) for a category \\(\mathcal{C}\\) has three components: - A family of morphisms \\(\pi_1 : A \times B \to A\\) - Another family of morphisms \\(\pi_2 : A \times B \to A\\) - A unique _morphism composition_ operation \\((\triangle):(A \to B) \Rightarrow (A \to C) \Rightarrow A \to B \times C\\) obeying the laws below (The reason for the two kinds of arrows is to distinguish between morphisms in the Category and functions in the meta-language. See the Conal Elliot and John Wiegley linked above for formulations with Haskell and Coq as the meta languages, respectively.) I've seen \\(\pi_1\\) and \\(\pi_2\\) called _projections_. John Wiegley refers to \\((\triangle)\\) as _"fork"_ in his code, which seems a fine name to me. A product obeys the following laws: \\[ \pi_1 \cdot f \triangle g = f\\\\ \pi_2 \cdot f \triangle g = g\\\\ (\pi_1 \cdot f) \triangle (\pi_2 \cdot f) = f \\] In Haskell, using itself as its own meta-language, we have \\((\times)\\) is the type constructor `(,)`, \\(\pi_1\\) is `fst :: (a,b) -> a` and \\(\pi_2\\) is `snd :: (a,b) -> b`. Lastly, we have \\((\triangle)\\) is [`Control.Arrow.(&&&)`](https://hackage.haskell.org/package/base-4.12.0.0/docs/Control-Arrow.html#v:-38--38--38-). You can check that `fst . (f &&& g) = f` and `snd . (f &&& g) = g` by looking at the [instantiation of the `Arrow` class for `(->)` in base](https://hackage.haskell.org/package/base-4.12.0.0/docs/src/Control.Arrow.html#line-143). -------------------------------- So let's extend the definition of the product preorder \\(\mathcal{P} \times \mathcal{Q}\\) to a product by defining \\(\pi_1\\), \\(\pi_2\\) and \\((\triangle)\\). - \\(\pi_1\\) is the map \\((a,b) \mapsto a\\) - \\(\pi_2\\) is the map \\((a,b) \mapsto b\\) - \\((\triangle)\\) is the map \\(f \mapsto g \mapsto (a \mapsto (f (a), g (a)))\\) These definitions are _very_ similar to the Haskell correlates. Checking the laws are obeyed is just evaluating the functions. It's a bit less trivial to check that \\(\pi_1\\), \\(\pi_2\\) and \\(f \triangle g\\) are all morphisms. In this case, we need them to be _order preserving maps_. - Suppose that \\((a,b) \preceq_{P \times Q} (c,d)\\). Then \\(a \preceq_{P} c\\) by definition, hence \\(\pi_1(a,b) \preceq \pi_1(c,d)\\) - The proof that \\(\pi_2\\) is order preserving is similar to the proof of \\(\pi_1\\) above. - Let \\(f : A \to B\\) and \\(g: A \to C\\) be order preserving maps. Moreover, let \\(a \preceq_A b\\). We need to show \\((f \triangle g)(a) \preceq_{B \times C} (f \triangle g)(b)\\). This is the same thing as showing \\((f (a), g(a)) \preceq_{B \times C} (f(b), g(b))\\). But since \\(f\\) and \\(g\\) are both order preserving, we know that \\(f(a) \preceq_B f(b)\\) and \\(g(a) \preceq_C g(b)\\), hence we have the result by definition. I'll try to find the time next week to show the other properties that make \\(PreOrder\\) Bicartesian closed. It's my opinion that it's important to learn the algebraic formulations of the category theoretic laws rather than just the traditional commuting diagrams. But thankfully we can always find correlates in Haskell, since `(->)` is also Bicartesian closed. I might do a little less proving, though. I think if we want to get serious about writing proofs we should consider formulating this stuff in `Coq` or `Lean`. These systems really drive home the connection between CT and programming. [EDIT: Adding third law for products, fixing up proper usage of terms.] [EDIT2: Adding uniqueness constraint]`

Okay, so far we've shown that \(PreOrder\) has products. We can go a bit further to show it's a

Cartesian category.In order for a category to be a Cartesian category, it must have a Cartesian category which is

Monoidal. In this case we just need an object \(\mathbf{1}\) which obeys the following axiom:\[ X \times \mathbf{1} \simeq X \]

Here \(\mathbf{1}\) is called a

unit.Here I'm following Hinze's axiomatization of a Bicartesian closed category in Reason Isomorphically! (2010). In the general case of Monoidal categories the axioms are more complicated.

Before looking at \(PreOrder\), lets see how \(Hask\) is a Cartesian category.

In the case of Hask, the unit \(\mathbf{1}\) is

`()`

. In order to show this, we need to find an isomorphism between`(a,())`

and`a`

. The following two functions do the trick:In \(PreOrder\), \(\mathbf{1}\) is the preorder with just one element. In this setting we take analogues of

`pairUnit`

and`unpairUnit`

and observer they are order-preserving.`Okay, so far we've shown that \\(PreOrder\\) has products. We can go a bit further to show it's a _Cartesian category_. In order for a category to be a Cartesian category, it must have a Cartesian category which is [_Monoidal_](https://en.wikipedia.org/wiki/Monoidal_category). In this case we just need an object \\(\mathbf{1}\\) which obeys the following axiom: \\[ X \times \mathbf{1} \simeq X \\] Here \\(\mathbf{1}\\) is called a _unit_. Here I'm following Hinze's axiomatization of a Bicartesian closed category in [Reason Isomorphically! (2010)](http://www.cs.ox.ac.uk/people/daniel.james/iso/iso.pdf). In the general case of Monoidal categories the axioms are more complicated. ------------------------------- Before looking at \\(PreOrder\\), lets see how \\(Hask\\) is a Cartesian category. In the case of Hask, the unit \\(\mathbf{1}\\) is `()`. In order to show this, we need to find an isomorphism between `(a,())` and `a`. The following two functions do the trick: pairUnit :: a -> (a,()) pairUnit x = (x,()) unpairUnit :: (a,()) -> a unpairUnit (x,()) = x ------------------------------- In \\(PreOrder\\), \\(\mathbf{1}\\) is the preorder with just one element. In this setting we take analogues of `pairUnit` and `unpairUnit` and observer they are order-preserving.`

@MatthewDoty wrote:

So:

What are the exponential of two preorders? I'm guessing that \(A^B\) is the set of order preserving maps from \(B\) to \(A\), where the maps are ordered by pointwise comparisons: \(f \le g\) means \(f(x) \le g(x)\) for all \(x\).

Guessing again, is the coproduct formed by taking the disjoint union of the underlying sets, and the disjoint union of the ordering relations?

`@MatthewDoty wrote: > In fact, the category of preorders is _bicartesian closed_. There's an initial preorder, a final preorder, products and coproducts and an exponential. If this is interesting we can go into this construction and the proof. So: * Initial preorder = empty set * Final preorder = terminal preorder = singleton set What are the exponential of two preorders? I'm guessing that \\(A^B\\) is the set of order preserving maps from \\(B\\) to \\(A\\), where the maps are ordered by pointwise comparisons: \\(f \le g\\) means \\(f(x) \le g(x)\\) for all \\(x\\). Guessing again, is the coproduct formed by taking the disjoint union of the underlying sets, and the disjoint union of the ordering relations?`

Those seem like such natural candidates that it would be surprising if it weren't them. I know it's just a homework exercise to draw the diagrams and check the claims. Maybe tomorrow when I'm feeling more fresh. I had a professor in college who would scribble all kinds of long detailed computations on the board. One day he said: when in doubt, do the dog work.

Since I'm feeling tired and lazy tonight, anyone feel free to cut in and prove or disprove my hypotheses.

`Those seem like such natural candidates that it would be surprising if it weren't them. I know it's just a homework exercise to draw the diagrams and check the claims. Maybe tomorrow when I'm feeling more fresh. I had a professor in college who would scribble all kinds of long detailed computations on the board. One day he said: when in doubt, do the dog work. Since I'm feeling tired and lazy tonight, anyone feel free to cut in and prove or disprove my hypotheses.`

From my understanding this is all correct.

So... drawing and scanning diagrams by hand is a lot of work, or making them with TikZ and exporting them to png and so on (this forum doesn't support svgs sadly).

I find the equational approach is a bit easier online, and it often corresponds super nicely with Haskell.

So let's start with coproducts. They are very similar to the products. They have morphisms \(i_1 : A \to A + B\) and \(i_2 : B \to A + B\) and morphism composition \((\nabla) : (A \to C) \Rightarrow (B \to C) \Rightarrow A + B \to C\). I'll come back later and write the equations out unless someone else wants to. The analogues in Haskell can all be found in the

`Prelude`

, unlike products where we need`Control.Arrow.(&&&)`

.For exponentials, one way of defining them is via the adjunction \(\bullet \times A \dashv \bullet^A\). In this case we would want to show, for all \(B\):

\[ Hom(- \times A, B) \simeq Hom(-, B^A) \]

Finally, it's possible to define coproducts via an adjunction and exponentials via equations. These aren't as natural in Haskell, however.

I'll come back later and chip away at these proofs @DavidTanzer.

[EDIT: Clarifying exponential adjunction equation to follow usual notation]

`> What are the exponential of two preorders? I'm guessing that \\(A^B\\) is the set of order preserving maps from \\(B\\) to \\(A\\), where the maps are ordered by pointwise comparisons: \\(f \leq g\\) means \\(f(x) \leq g(x)\\) for all \\(x\\). > Guessing again, is the coproduct formed by taking the disjoint union of the underlying sets, and the disjoint union of the ordering relations? From my understanding this is all correct. > I know it's just a homework exercise to draw the diagrams and check the claims. So... drawing and scanning diagrams by hand is a lot of work, or making them with TikZ and exporting them to png and so on (this forum doesn't support svgs sadly). I find the equational approach is a bit easier online, and it often corresponds super nicely with Haskell. ------ So let's start with coproducts. They are very similar to the products. They have morphisms \\(i_1 : A \to A + B\\) and \\(i_2 : B \to A + B\\) and morphism composition \\((\nabla) : (A \to C) \Rightarrow (B \to C) \Rightarrow A + B \to C\\). I'll come back later and write the equations out unless someone else wants to. The analogues in Haskell can all be found in the `Prelude`, unlike products where we need `Control.Arrow.(&&&)`. ------ For exponentials, one way of defining them is via the adjunction \\(\bullet \times A \dashv \bullet^A\\). In this case we would want to show, for all \\(B\\): \\[ Hom(- \times A, B) \simeq Hom(-, B^A) \\] ------ Finally, it's possible to define coproducts via an adjunction and exponentials via equations. These aren't as natural in Haskell, however. I'll come back later and chip away at these proofs @DavidTanzer. [EDIT: Clarifying exponential adjunction equation to follow usual notation]`

Great, thanks @MatthewDoty!

This is informative. All chippings away are appreciated. I can almost see the co-products. Equational presentation would be great to see. Maybe that would help me to better parse Haskell. I'm more comfortable with the straight mathematical language, and with "ordinary" languages like Python, but when I look at Haskell code it can look blurry.

Another option for these kinds of focussed explanations would be to create small discussions, in the category "Forum Mini-Talks". A wrote a few there. They're not meant to be some kind of earth shaking thing, just to have a useful point that is intended to be made, and to be explained in a way that tries to help the reader get from point A to point B.

Or these approaches could be combined. Answers made in the context of a discussion here could later be culled and organized into a mini-talk.

`Great, thanks @MatthewDoty! This is informative. All chippings away are appreciated. I can almost see the co-products. Equational presentation would be great to see. Maybe that would help me to better parse Haskell. I'm more comfortable with the straight mathematical language, and with "ordinary" languages like Python, but when I look at Haskell code it can look blurry. Another option for these kinds of focussed explanations would be to create small discussions, in the category "Forum Mini-Talks". A wrote a few there. They're not meant to be some kind of earth shaking thing, just to have a useful point that is intended to be made, and to be explained in a way that tries to help the reader get from point A to point B. Or these approaches could be combined. Answers made in the context of a discussion here could later be culled and organized into a mini-talk.`

I have to admit I really like Haskell and I think its great for studying category theory. Equational reasoning in Haskell is quite common in research papers.

That being said, I'll try to balance these discussions with more traditional mathematics.

Anyhow, here's the usual commutative diagram for the coproduct:

The diagram doesn't mention the morphism composition operation \((\nabla) : (A \to C) \Rightarrow (B \to C) \Rightarrow A + B \to C\), but it takes the place of \(f\). Instead of \(f\), we would write \(f_1 \nabla f_2\).

The morphism composition operation \((\nabla)\) is unique in obeying the equations for the coproduct, are quite similar to the product equations:

\[ f \nabla g \cdot i_1 = f\\ f \nabla g \cdot i_2 = g\\ (f \cdot i_1) \nabla (f \cdot i_2) = f \]

In

Hask, \(i_1\) is`Left :: a -> Either a b`

, \(i_2\) is`Right :: b -> Either a b`

, and \((\nabla)\) is`either :: (a -> c) -> (b -> c) -> Either a b -> c`

Once again, I feel the only real challenge in the case of

PreOrderis showing all of the morphisms involved are order preserving maps. I did something similar above so I'll just wave my hand at that.The adjunction \( \bullet \times A \dashv \bullet^A \) is realized by the functors

`(,a)`

and`(->) a`

. That second functor is called thereader monad. It comes up pretty often when you have to read information from a config for a web app and you don't want to carry a parameter around.The isomorphism

`Hom(- \times A, B) \simeq Hom(-, B^A)`

is realized by two functions:Okay, it's getting a bit late, more tomorrow...

[EDIT: Formatting, mentioning uniqueness]

`> Equational presentation would be great to see. Maybe that would help me to better parse Haskell. I'm more comfortable with the straight mathematical language, and with "ordinary" languages like Python, but when I look at Haskell code it can look blurry. I have to admit I really like Haskell and I think its great for studying category theory. Equational reasoning in Haskell is quite common in research papers. That being said, I'll try to balance these discussions with more traditional mathematics. Anyhow, here's the usual commutative diagram for the coproduct: ![Coproduct](https://upload.wikimedia.org/wikipedia/commons/thumb/2/2b/Coproduct-03.svg/200px-Coproduct-03.svg.png) The diagram doesn't mention the morphism composition operation \\((\nabla) : (A \to C) \Rightarrow (B \to C) \Rightarrow A + B \to C\\), but it takes the place of \\(f\\). Instead of \\(f\\), we would write \\(f_1 \nabla f_2\\). The morphism composition operation \\((\nabla)\\) is unique in obeying the equations for the coproduct, are quite similar to the product equations: \\[ f \nabla g \cdot i_1 = f\\\\ f \nabla g \cdot i_2 = g\\\\ (f \cdot i_1) \nabla (f \cdot i_2) = f \\] In *Hask*, \\(i_1\\) is `Left :: a -> Either a b`, \\(i_2\\) is `Right :: b -> Either a b`, and \\((\nabla)\\) is `either :: (a -> c) -> (b -> c) -> Either a b -> c` Once again, I feel the only real challenge in the case of *PreOrder* is showing all of the morphisms involved are order preserving maps. I did something similar above so I'll just wave my hand at that. ----------------------------------- The adjunction \\( \bullet \times A \dashv \bullet^A \\) is realized by the functors `(,a)` and `(->) a`. That second functor is called the _reader monad_. It comes up pretty often when you have to read information from a config for a web app and you don't want to carry a parameter around. The isomorphism `Hom(- \times A, B) \simeq Hom(-, B^A)` is realized by two functions: uncurry :: (c -> a -> b) -> (c,a) -> b curry :: ((c,a) -> b) -> (c -> a -> b) Okay, it's getting a bit late, more tomorrow... [EDIT: Formatting, mentioning uniqueness]`

Sounds good! I'm glad to try on some new glasses.

`> I have to admit I really like Haskell and I think its great for studying category theory. Equational reasoning in Haskell is quite common in research papers. Sounds good! I'm glad to try on some new glasses.`