Category Theory III 6.2, Ends

[@Bratjuuc]

Are dinatural transformations enough to map one Haskell arrow into another? The restriction to just diagonally indexed profunctors seem to be insufficient.

I'm a little confused by the dinatural transformation. Is it deliberately switching order of the objects when going from p b a -> q a b? Shouldn't the lifting of morphisms at the bottom of the diamond be reversed so we get q b a?

[@mzg147]

Aren't natural transformations and polymorphic functions the same? (In category Hask) I thought the naturality square is equivalent to saying that α is defined "in one way for all types", i.e. by a single formula. Is there a counterexample of natural transformation that isn't polymorphic?

[@BartoszMilewski]

They are the same in system F, which defines parametric polymorphism-- the "single formula" thing. It's hard to express a counter-example, since even functors in a programming language are parametric. You'd have to use ad-hoc polymorphism.

[@keithmanzi8891]

For of deserts hope does express wait

[@themathguy3149]

I guess I reached the end(s) of mathematics 🤔 when will the launch the sequel (mathematics 2.0)? 😅

[@cooperating.systems]

The limit of a category of 2 points is a product and the co-limit a co-product. I wonder what the limit of a category with two points and two arrows is. ie s,e: A -> B. In "Category Theory for Computer Science" Michael Bell and Charles Wells state that a functor from that category always selects a graph. A being the arrows and B the endpoints, and s selects that start point and e the end point of the arrow in B. Actually A could be the same as B, in which case the start and end points would be arrows, presumably identity arrows. So you started session 6 with limits, I was wondering what a limit of such a diagram would be. How would I find out? Note these graphs are called Quivers in ncatlab ncatlab.org/nlab/show/quiver

[@cooperating.systems]

I asked it on Math Stack Exchange math.stackexchange.com/questions/2895114/what-is-the-colimit-of-a-quiver :-)

[@DrBartosz]

This limit is called the equalizer. A graph is a functor from this category to Set. It picks the set of arrows and the set of vertices.

[@cooperating.systems]

yes, that was the conclusion I came to on stackexchange with some help :-) Then I wondered if you may not have covered that in your first courses, which I may have skipped. If so that is my mistake, one always needs to get back to basics... Comparing those limits with products and co-products one gets this interesting similarity. The equivalent to products for a quiver is the set of loops - which in a way are the most independent types of arrows, since they only need the objects they start from, the way one can think of a product as bringing two dimensions together in the most independent manner. And the limit equivalent for a co-product brings together all connected graphs into one object, which feels a bit like a disjoing union. Except that here it finds the disjoint unions in the graph.

[@ShimshonDI]

The video whose existence you postulate is video II: 3.1, in which Milewski spends the first 11 min discussing equalizers. kzbin.info/www/bejne/iqXZh3uloM2Gpa8

[@stephanevernede8107]

Thanks so much for those amazing lectures Have you played around with the language Julia ? Its type system forms a beautiful category with a initial object `any` and a terminal object `bitarray` It has a flexible polymorphism that can encode wedges and last but not least it has performance close to C (and often better) It is the next level of programming language and a great playground for category lovers.