Nobody seems to care or notice. I'm watching in disbelief how nobody is pointing out the article is full of inaccuracies. See my sibling thread for a (very) incomplete list, which should disqualified this as a serious reading: https://news.ycombinator.com/item?id=47814213
My conclusion cannot be other than this ought to be useless for the general practitioner, since even wrong mathematics is appreciated the same as correct mathematics.
Writing a program and proving a theorem are the same act. (Curry–Howard–Lambek.) For well-behaved programs, every program is a proof of something and every proof is a program. The match is exact for simple typed languages and leaks a bit once you add general recursion (an infinite loop “proves” anything in Haskell), but the underlying identity is real. Lambek added the third leg: these are also morphisms in a category. [1]
Algebra and geometry are one thing wearing different costumes. (Stone duality and cousins.) A system of equations and the shape it cuts out aren’t related, they’re the same object seen from opposite sides. Grothendieck rebuilt algebraic geometry on this idea, with schemes (so you can do geometry on the integers themselves) and étale cohomology (topological invariants for shapes with no actual topology). His student Deligne used that machinery to settle the Weil conjectures in 1974. Wiles’s Fermat proof lives in the same world, though it leans on much more than the categorical foundations. [2]
[0] https://en.wikipedia.org/wiki/Yoneda_lemma
[1] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
We should strive to name all things by their function not by their inventor or discoverer IMO. But people like their ribbons.
A morphism from orange to yellow means "O <= Y". From this, antisymmetry (and the hidden assumption) implies that "Y not <= O".
Totality is just the other way around (all two distinct elements are comparable in one direction).
"All diagrams that look something different than the said chain diagram represent partial orders"
"The different linear orders that make up the partial order are called chains"
The Birkhoff theorem statement, which is materially wrong. A finite distributive lattice is not isomorphic to "the inclusion order of its join-irreducible elements".
The 'not accurate' diagram says that orange-less-than-yellow implies yellow-not-less-than-orange. Hard to find fault with.
> NO. Antisymmetry doesn't exclude `x = y`. Ties are permitted in the equality case. Antisymmetry for a non-strict order says that if both directions hold, the two elements must in fact be the same element. The author is describing strict comparison or total comparability intuition, not antisymmetry.
I like the article's "imprecise prose" better:
You have x ≤ y and y ≤ x only if x = yThe prose "It also means that no ties are permitted - either I am better than my grandmother at soccer or she is better at it than me" is inaccurate for describing antisymmetry. In the same short section, you first state the correct condition:
You have x ≤ y and y ≤ x only if x = y
from which it doesn't follow that "It also means that no ties are permitted". The "no ties" idea belongs to a stronger notion such as a strict total order, not to antisymmetry.
I'm unclear what the last 10% of 'category theory' gives us.
In a preorder seen as a category, there is at most one arrow between any two objects. So every diagram commutes and uniqueness is basically free. Then products and coproducts stop looking like magic diagrams and become something very familiar: greatest lower bounds and least upper bounds.
Small nit: preorders are thin categories, but posets are the skeletal thin categories. In a preorder you can have distinct a and b with both a <= b and b <= a, which means they are isomorphic, not literally the same. Quotienting by that equivalence gives you the poset.
The software angle is the part I find most useful. This kind of bugs shows up when we force a total order onto something that is only partially ordered, or only preordered. Dependency graphs, versions, permissions, type hierarchies, CRDT states, rule specificity, build steps. A lot of these don’t really want a comparator and a sort. Sometimes they want a quotient, a topological sort, a join, or just the honest answer that two things are not comparable.
That feels like the practical lesson here: category theory is not always adding abstraction. Sometimes it is just a good way to stop pretending two different structures are the same thing.