A Higher-Order Calculus for Categories describes a system where you can conveniently perform manipulations with categories, functors, Yoneda embeddings etc. An example of the rules is: $$\frac{\Gamma , X {:} \mathcal C^{\mathsf{op}}, Y {:} \mathcal C \vdash E : \mathcal D, \quad \mathcal D\textsf{ complete}, \quad \mathcal C\textsf{ small}}{\Gamma \vdash \int_{X, Y} E : \mathcal D}$$

Is there an actual implementation for this system? Embedding into an existing proof assistant also counts. Internet searches don't seem to yield anything.

  • $\begingroup$ Of interest: "A Higher-Order Calculus for Categories" (pdf) $\endgroup$
    – Guy Coder
    Mar 29, 2022 at 10:07
  • $\begingroup$ If this answers your question let me know and I will post as an answer. "Category Theory" by Alexander Katovsky (pdf). (Code page) $\endgroup$
    – Guy Coder
    Mar 29, 2022 at 10:12
  • $\begingroup$ @GuyCoder I think that formalizes category theory inside Isabelle/HOL. What I'm expecting is something like Isabelle/Cat, which directly implements the manipulations as typing rules (instead of lemmata and theorems). Nonetheless I think your link is quite cool, and I'll look into it. $\endgroup$
    – Trebor
    Mar 29, 2022 at 10:20
  • $\begingroup$ @Trebor It looks like the authors describe an implementation of the calculus in Isabelle/Pure in the first paper cited by Guy Coder. I would be interested in taking a look at the implementation if it is still available somewhere. $\endgroup$ Mar 29, 2022 at 13:57
  • 3
    $\begingroup$ I've started implementing it in agda-categories, but had to pause because I got too busy with my day job as a prof... I'd warmly welcome PRs that would continue that work. $\endgroup$ Mar 30, 2022 at 13:06


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.