Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids

DOI10.1007/3-540-61780-9_61MaRDI QIDQ4647569zbMATH OpenOpenAlexFDO

Authors Ilya Beylin, Peter Dybjer

Publication date 15 January 2019

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-61780-9_61

zbMATH Keywords

category theorytype theoryproof assistantmonoidal categorynatural isomorphism

Mathematics Subject Classification ID

Recommendations

• Coherence for skew-monoidal categories
• Coherence in substructural categories
• Coherence in monoidal track categories
• Coherence for bicategories, lax functors, and shadows
• scientific article; zbMATH DE number 1696616

Cites work

• scientific article; zbMATH DE number 65535 (Why is no real title available?)
• scientific article; zbMATH DE number 1555179 (Why is no real title available?)
• scientific article; zbMATH DE number 3367095 (Why is no real title available?)
• Categorical reconstruction of a reduction free normalization proof
• Coherence for tricategories
• Internal type theory
• Intuitionistic model constructions and normalization proofs
• Normalising the associative law: An experiment with Martin-Löf's type theory

Cited in

(10)

• A comparison of HOL and ALF formalizations of a categorical coherence theorem
• A well-known representation of monoids and its application to the function ‘vector reverse’
• Internal type theory
• Coherence for skew-monoidal categories
• Zigzag normalisation for associative \(n\)-categories
• Revisiting the categorical interpretation of dependent type theory
• Coherence for monoidal groupoids in HoTT
• Proof Theory of Partially Normal Skew Monoidal Categories
• mathlib4 Module Mathlib/CategoryTheory/Bicategory/Coherence
• mathlib4 Module Mathlib/CategoryTheory/Monoidal/Free/Coherence

This page was built for publication: Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids

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