Turkish Journal of Mathematics
Article Title
DOI
10.55730/1300-0098.3178
Abstract
In this paper, we present a category theory library developed in the proof assistant Coq. We discuss the design principles of the library in comparison with those existing out there. To explicitly demonstrate the utility of the library, we conclude with a case study in which a Coq formalized soundness proof of the intuitionistic propositional logic within a category theoretical settings is examined.
First Page
1538
Last Page
1552
Recommended Citation
EKİCİ, BURAK
(2022)
"Formal categorical reasoning,"
Turkish Journal of Mathematics: Vol. 46:
No.
4, Article 31.
https://doi.org/10.55730/1300-0098.3178
Available at:
https://journals.tubitak.gov.tr/math/vol46/iss4/31
