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

DOI10.1007/3-540-61780-9_61zbMath1407.68432OpenAlexW1489565250MaRDI QIDQ4647569

Peter Dybjer, Ilya Beylin

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 theorymonoidal categorytype theoryproof assistantnatural isomorphism

Mathematics Subject Classification ID

Related Items

A well-known representation of monoids and its application to the function ‘vector reverse’ ⋮ Unnamed Item ⋮ Internal type theory ⋮ Revisiting the categorical interpretation of dependent type theory

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Normalising the associative law: An experiment with Martin-Löf's type theory
• Intuitionistic model constructions and normalization proofs
• Internal type theory
• Coherence for tricategories
• Categorical reconstruction of a reduction free normalization proof

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