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

DOI10.1007/3-540-61780-9_61zbMATH Open1407.68432OpenAlexW1489565250MaRDI QIDQ4647569FDOQ4647569

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

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

zbMATH Keywords

category theorytype theoryproof assistantmonoidal categorynatural isomorphism

Mathematics Subject Classification ID

Cites Work

• Categorical reconstruction of a reduction free normalization proof
• Title not available (Why is that?)
• Internal type theory
• Coherence for tricategories
• Title not available (Why is that?)
• Intuitionistic model constructions and normalization proofs
• Normalising the associative law: An experiment with Martin-Löf's type theory
• Title not available (Why is that?)

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)