English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

We describe our experience implementing a broad category-theory library inCoq. Category theory and computational performance are not usually mentioned inthe same breath, but we have needed substantial engineering effort to teach Coqto cope with large categorical constructions without slowing proof scriptprocessing unacceptably. In this paper, we share the lessons we have learnedabout how to represent very abstract mathematical objects and arguments in Coqand how future proof assistants might be designed to better support suchreasoning. One particular encoding trick to which we draw attention allowscategory-theoretic arguments involving duality to be internalized in Coq'slogic with definitional equality. Ours may be the largest Coq development todate that uses the relatively new Coq version developed by homotopy typetheorists, and we reflect on which new features were especially helpful.

Experience Implementing a Performant Category-Theory Library in Coq