Journal article
Formalizing category theory in Agda
Abstract
The generality and pervasiveness of category theory in modern mathematics makes it a frequent and useful target of formalization. It is however quite challenging to formalize, for a variety of reasons. Agda currently (i.e. in 2020) does not have a standard, working formalization of category theory. We document our work on solving this dilemma. The formalization revealed a number of potential design choices, and we present, motivate and explain …
Authors
Hu JZS; Carette J
Journal
, , , pp. 327–342
Publisher
Association for Computing Machinery (ACM)
Publication Date
January 17, 2021
DOI
10.1145/3437992.3439922