A sketchpad repository for formalizations of a bunch of concepts from category theory and examples in various categories, modeled with setoids so each category can come equipped with its own sense of morphism equality. --type-in-type is invoked unapologetically for the sake of convenience.