On: Functors and Monads for People Who Have Read Too Many “Tutorials”

[drdeca]

Do you happen to know of any programming language which has explicit support for multiple categories?

[hiker → drdeca]

Lean[0]'s mathlib has quite nice formalisation of category theory[1] with plenty examples of concrete categories even sheaves and toposes.

[0] https://leanprover.github.io/programming_in_lean/#01_Introdu...

[1] https://github.com/leanprover-community/mathlib/blob/master/...