See here. Has anyone attempted to use this to verify category theoretic proofs? Given the relationship between categories and graphs, are there some applications with respect to graph algorithms? What other possible uses are there for this package and those associated with it?
I realize this is a broad, open-ended question, which may not be entirely appropriate for Stack Exchange. A better place to post this question could also be a helpful answer.