Name
Title | ||
|---|---|---|
Extracting a Proof of Coherence for Monoidal Categories from a Proof of Normalization for Monoids |
Abstract | ||
|---|---|---|
This paper studies a connection between intuitionistic type theory and coherence problems inthe sense of category theory. We first show how a Curry-Howard interpretation of a formal proof ofnormalization for monoids almost directly yields a coherence proof for monoidal categories. Thenwe formalize the coherence proof in type theory and show how this proof relies on "metacoherence",that is, the unicity of certain proofs of equality in intuitionistic type theory. This formalization hasalso... |
Year | DOI | Venue |
|---|---|---|
1995 | 10.1007/3-540-61780-9_61 | TYPES |
Keywords | Field | DocType |
monoidal categories,category theory,type theory | Discrete mathematics,Enriched category,Intuitionistic type theory,Monoidal category,Algebra,Computer science,Type theory,Symmetric monoidal category,Higher category theory,Formal proof,Proof assistant | Conference |
Volume | ISSN | ISBN |
1158 | 0302-9743 | 3-540-61780-9 |
Citations | PageRank | References |
12 | 1.77 | 9 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ilya Beylin | 1 | 20 | 3.52 |
| Peter Dybjer | 2 | 540 | 76.99 |