Universal Properties by Jeremy Kun.
From the post:
Previously in this series we’ve seen the definition of a category and a bunch of examples, basic properties of morphisms, and a first look at how to represent categories as types in ML. In this post we’ll expand these ideas and introduce the notion of a universal property. We’ll see examples from mathematics and write some programs which simultaneously prove certain objects have universal properties and construct the morphisms involved.
Just in time for a long holiday weekend in the U.S., Jeremy continues his series on category theory.
Enjoy!