Reference. Coherence for bicategorical cartesian closed structure
We prove a strictification theorem for cartesian closed bicategories. First, we adapt Power’s proof of coherence for bicategories with finite bilimits to show that every bicategory with bicategorical cartesian closed structure is biequivalent to a 2-category with 2-categorical cartesian closed structure. Then we show how to extend this result to a Mac Lane-style “all pasting diagrams commute” coherence theorem: precisely, we show that in the free cartesian closed bicategory on a graph, there is at most one 2-cell between any parallel pair of 1-cells. The argument we employ is reminiscent of that used by Čubrić, Dybjer, and Scott to show normalisation for the simply-typed lambda calculus (Čubrić et al., 1998). The main results first appeared in a conference paper (Fiore and Saville, 2020) but for reasons of space many details are omitted there; here we provide the full development.
Cite
Cites 46 works (5 here)
With notes (5)
Coherence and normalisation-by-evaluation for bicategorical cartesian closed structure fiore_saville_2020
We present two proofs of coherence for cartesian closed bicategories. Precisely, we show that in the free cartesian closed bicategory on a set of objects there is at most one structural 2-cell between any parallel pair of 1-cells. We thereby reduce the difficulty of constructing structure in arbitrary cartesian closed bicategories to the level of 1-dimensional category theory. Our first proof follows a traditional approach using the Yoneda lemma. For the second proof, we adapt Fiore’s categorical analysis of normalisation-by-evaluation for the simply-typed lambda calculus. Modulo the construction of suitable bicategorical structures, the argument is not significantly more complex than its 1-categorical counterpart. It also opens the way for further proofs of coherence using (adaptations of) tools from categorical semantics.
Normalization and the Yoneda embedding NormalizationAndTheYonedaEmbedding
We show how to solve the word problem for simply typed λβη-calculus by using a few well-known facts about categories of presheaves and the Yoneda embedding. The formal setting for these results is 𝒫-category theory, a version of ordinary category theory where each hom-set is equipped with a partial equivalence relation. The part of 𝒫-category theory we develop here is constructive and thus permits extraction of programs from proofs. It is important to stress that in our method we make no use of traditional proof-theoretic or rewriting techniques. To show the robustness of our method, we give an extended treatment for more general λ-theories in the Appendix.
Two-dimensional monad theory blackwell_kelly_power_1989
A general coherence result power_1989
Introduction to Higher-Order Categorical Logic lambek_scott_1986
External (41)
- Probabilistic concurrent game semantics (PhD thesis) (2020)
- Cartesian closed bicategories: type theory and coherence (PhD thesis) (2020)
- A language for closed cartesian bicategories (talk, CT 2019) (2019)
- Coherence of Gray categories via rewriting (2018)
- On operads, bimodules and analytic functors (2017)
- Compact closed bicategories (2016)
- Theory of para-toposes (talk, CT 2015) (2015)
- Coherence in Three-Dimensional Category Theory (2013)
- Cartesian closed 2-categories and permutation equivalence in higher-order rewriting (2013)
- A 2-Categories Companion (2010)
- Bicategories of spans as cartesian bicategories (2010)
- Cartesian bicategories II (2008)
- The cartesian closed bicategory of generalised species of structures (2007)
- Linear Logic without Units (PhD thesis) (2007)
- An Algebraic Theory of Tricategories (2006)
- Pseudo limits, biadjoints, and pseudo algebras: categorical foundations of conformal field theory (2006)
- Higher Operads, Higher Categories (2004)
- Categories of Containers (2003)
- A theory of recursive domains with applications to concurrency (1998)
- 2-categories (BRICS Notes Series) (1998)
- Categories for the Working Mathematician (2nd ed.) (1998)
- Basic Bicategories (1998)
- Monoidal Bicategories and Hopf Algebroids (1997)
- A two-dimensional extension of Lambek's categorical proof theory (MSc thesis) (1997)
- Avoiding the axiom of choice in general category theory (1996)
- Towards a proof theory of rewriting: The simply typed 2λ-calculus (1996)
- Coherence for tricategories (1995)
- Bicategories and distributors (1994)
- Introduction to extensive and distributive categories (1993)
- Braided Tensor Categories (1993)
- Coherence for bicategories with finite bilimits. I (1989)
- Cartesian bicategories I (1987)
- Coherence for bicategories and indexed categories (1985)
- Fibered categories and the foundations of naive category theory (1985)
- Basic Concepts of Enriched Category Theory (1982)
- Fibrations in bicategories (1980)
- Formal Category Theory: Adjointness for 2-Categories (1974)
- The formal theory of monads (1972)
- On closed categories of functors (1970)
- Introduction to bicategories (1967)
- Natural associativity and commutativity (1963)