A mechanically assisted constructive proof in category theory

DOI10.1007/3-540-52885-7_110MaRDI QIDQ6488555zbMATH OpenFDO

Authors Prakash Panangaden

Publication date 28 April 2023

Full work available at URL https://doi.org/10.1007/3-540-52885-7_110

Mathematics Subject Classification ID

Adjoint functors (universal constructions, reflective subcategories, Kan extensions, etc.) (18A40) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Nuprl as logical framework for automating proofs in category theory
• Automating Proofs in Category Theory
• scientific article; zbMATH DE number 193170
• Experience implementing a performant category-theory library in Coq
• scientific article; zbMATH DE number 3999258

Cites work

• A mechanically assisted constructive proof in category theory
• scientific article; zbMATH DE number 4179333 (Why is no real title available?)
• scientific article; zbMATH DE number 3928956 (Why is no real title available?)
• scientific article; zbMATH DE number 3723838 (Why is no real title available?)
• scientific article; zbMATH DE number 41806 (Why is no real title available?)
• scientific article; zbMATH DE number 193170 (Why is no real title available?)
• scientific article; zbMATH DE number 4126684 (Why is no real title available?)
• scientific article; zbMATH DE number 3367095 (Why is no real title available?)
• scientific article; zbMATH DE number 3417640 (Why is no real title available?)

Cited in

(9)

• Experience implementing a performant category-theory library in Coq
• Nuprl as logical framework for automating proofs in category theory
• \textsf{Globular}: an online proof assistant for higher-dimensional rewriting
• A proof of the associated sheaf theorem by means of categorical logic
• Automating Proofs in Category Theory
• Globular: an online proof assistant for higher-dimensional rewriting
• Proof nets and semi-star-autonomous categories
• scientific article; zbMATH DE number 7715469 (Why is no real title available?)
• A mechanically assisted constructive proof in category theory

This page was built for publication: A mechanically assisted constructive proof in category theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6488555)