You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Jake Gillberg (Apr 17 2020 at 23:26):I have been having fun learning the basics by implementing exercise proofs from the recent Programming with Categories course in Idris and packaging them up as submissions to the statebox idris-ct project. Here is my most recent, proving CoProducts, Products, and Terminial/Initial Objects are Isomorphic. The similarity of these proofs has me wondering what a nice generalization would look like: a description of a universal property using the universal morphism definition? moving to the context of comma categories?
Evan Patterson (Apr 18 2020 at 00:01):Products and terminal objects are examples of limits, while coproducts and initial objects are examples of colimits. You could try giving the uniqueness-up-to-isomorphism proof for arbitrary limits or colimits. I'm not an Idris programmer, so I have no idea what that would look like in Idris.
Jake Gillberg (Apr 18 2020 at 13:22):It looks like I might be able to prove that they are all examples of initial objects in a comma category or its dual, and then prove that initial objects in a comma category (or the dual of one) are isomorphic