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

DOI10.1007/BFB0105394zbMATH Open1543.68413MaRDI QIDQ6567701FDOQ6567701

Authors: Sten Agerholm, Ilya Beylin, Peter Dybjer 

Publication date: 5 July 2024

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

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Inductive families
• Title not available (Why is that?)
• Title not available (Why is that?)
• A higher-order implementation of rewriting
• Title not available (Why is that?)

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)