A comparison of HOL and ALF formalizations of a categorical coherence theorem

DOI10.1007/BFB0105394MaRDI QIDQ6567701zbMATH OpenFDO

Authors Sten Agerholm, Ilya Beylin, Peter Dybjer

Publication date 5 July 2024

Mathematics Subject Classification ID

Formalization of mathematics in connection with theorem provers (68V20) Monoidal categories, symmetric monoidal categories (18M05)

Recommendations

• Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids
• scientific article; zbMATH DE number 1696616
• Towards a readable formalisation of category theory
• Formal categorical reasoning
• Automating free logic in HOL, with an experimental application in category theory

Cites work

• scientific article; zbMATH DE number 2185699 (Why is no real title available?)
• scientific article; zbMATH DE number 3859117 (Why is no real title available?)
• scientific article; zbMATH DE number 46995 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 107664 (Why is no real title available?)
• scientific article; zbMATH DE number 3521950 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• scientific article; zbMATH DE number 3367095 (Why is no real title available?)
• A higher-order implementation of rewriting
• Inductive families

This page was built for publication: A comparison of HOL and ALF formalizations of a categorical coherence theorem

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