We consider the problem of constructing the free bifibration generated by a functor of categories $𝑝:𝐷\to 𝐶$. This problem was previously considered by Lamarche, and is closely related to the problem, considered by Dawson, Paré, and Pronk, of “freely adjoining adjoints” to a category. We develop a proof-theoretic approach to the problem, beginning with a construction of the free bifibration ${\mathrm{\Lambda }}_{𝑝}:𝐵𝑖𝑓𝑖𝑏(𝑝)\to 𝐶$ in which objects of $𝐵𝑖𝑓𝑖𝑏(𝑝)$ are formulas of a primitive “bifibrational logic”, and arrows are derivations in a cut-free sequent calculus modulo a notion of permutation equivalence. We show that instantiating the construction to the identity functor generates a _zigzag double category_ $\mathbb{Z}(𝐶)$, which is also the free double category with companions and conjoints (or fibrant double category) on $𝐶$. The approach adapts smoothly to the more general task of building $(𝑃,𝑁)$-fibrations, where one only asks for pushforwards along arrows in $𝑃$ and pullbacks along arrows in $𝑁$ for some subsets of arrows; this encompasses Kock and Joyal’s notion of _ambifibration_ when $(𝑃,𝑁)$ form a factorization system. We establish a series of progressively stronger normal forms, guided by ideas of _focusing_ from proof theory, and obtain a canonicity result under assumption that the base category is factorization preordered relative to $𝑃$ and $𝑁$. This canonicity result allows us to decide the word problem and to enumerate relative homsets without duplicates. Finally, we describe several examples of a combinatorial nature, including a category of plane trees generated as a free bifibration over $𝜔$, and a category of increasing forests generated as a free ambifibration over $\mathrm{\Delta }$, which contains the lattices of noncrossing partitions as quotients of its fibers by the Beck-Chevalley condition for bicartesian squares.

We develop fibrational perspectives on context-free grammars and on nondeterministic finite-state automata over categories and operads. A generalized CFG is a functor from a free colored operad (aka multicategory) generated by a pointed finite species into an arbitrary base operad: this encompasses classical CFGs by taking the base to be a certain operad constructed from a free monoid, as an instance of a more general construction of an operad of spliced arrows $\mathrm{𝒲︀}\mathrm{𝒞︀}$ for any category $\mathrm{𝒞︀}$. A generalized NFA is a functor from an arbitrary bipointed category or pointed operad satisfying the unique lifting of factorizations and finite fiber properties: this encompasses classical word automata and tree automata without $𝜖$-transitions, but also automata over non-free categories and operads. We show that generalized context-free and regular languages satisfy suitable generalizations of many of the usual closure properties, and in particular we give a simple conceptual proof that context-free languages are closed under intersection with regular languages. Finally, we observe that the splicing functor $\mathrm{𝒲︀}:\text{Cat}\to \text{Oper}$ admits a left adjoint $\mathrm{𝒞︀}:\text{Oper}\to \text{Cat}$, which we call the contour category construction since the arrows of $\mathrm{𝒞︀}\mathrm{𝒪︀}$ have a geometric interpretation as oriented contours of operations of $\mathrm{𝒪︀}$. A direct consequence of the contour / splicing adjunction is that every pointed finite species induces a universal CFG generating a language of tree contour words. This leads us to a generalization of the Chomsky-Schützenberger Representation Theorem, establishing that a subset of a homset $𝐿\subseteq \mathrm{𝒞︀}(𝐴,𝐵)$ is a CFL of arrows if and only if it is a functorial image of the intersection of a $\mathrm{𝒞︀}$-chromatic tree contour language with a regular language.

We sketch a tentative proof of P-completeness for the $𝛽$-convertibility problem on untyped planar (a.k.a. ordered or non-commutative) $𝜆$-terms.

Motivated by compositional categorical rewriting theory, we introduce a convolution product over presheaves of double categories which generalizes the usual Day tensor product of presheaves of monoidal categories. One interesting aspect of the construction is that this convolution product is in general only oplax associative. For that reason, we identify several classes of double categories for which the convolution product is not just oplax associative, but fully associative. This includes in particular framed bicategories on the one hand, and double categories of compositional rewriting theories on the other. For the latter, we establish a formula which justifies the view that the convolution product categorifies the rule algebra product.

We begin by explaining how any context-free grammar encodes a functor of operads from a freely generated operad into a certain “operad of spliced words”. This motivates a more general notion of CFG over any category $𝐶$, defined as a finite species $𝑆$ equipped with a color denoting the start symbol and a functor of operads $𝑝:𝐹𝑟𝑒𝑒[𝑆]\to 𝑊[𝐶]$ into the operad of spliced arrows in $𝐶$. We show that many standard properties of CFGs can be formulated within this framework, and that usual closure properties of CF languages generalize to CF languages of arrows. We also discuss a dual fibrational perspective on the functor $𝑝$ via the notion of “displayed” operad, corresponding to a lax functor of operads $𝑊[𝐶]\to 𝑆𝑝𝑎𝑛(𝑆𝑒𝑡)$.

We then turn to the Chomsky-Schützenberger Representation Theorem. We describe how a non-deterministic finite state automaton can be seen as a category $𝑄$ equipped with a pair of objects denoting initial and accepting states and a functor of categories $𝑄\to 𝐶$ satisfying the unique lifting of factorizations property and the finite fiber property. Then, we explain how to extend this notion of automaton to functors of operads, which generalize tree automata, allowing us to lift an automaton over a category to an automaton over its operad of spliced arrows. We show that every CFG over a category can be pulled back along a ND finite state automaton over the same category, and hence that CF languages are closed under intersection with regular languages. The last important ingredient is the identification of a left adjoint $𝐶[-]:𝑂𝑝𝑒𝑟𝑎𝑑\to 𝐶𝑎𝑡$ to the operad of spliced arrows functor, building the “contour category” of an operad. Using this, we generalize the C-S representation theorem, proving that any context-free language of arrows over a category $𝐶$ is the functorial image of the intersection of a $𝐶$-chromatic tree contour language and a regular language.

Szlachányi’s skew monoidal categories are a well-motivated variation of monoidal categories in which the unitors and associator are not required to be natural isomorphisms, but merely natural transformations in a particular direction. We present a sequent calculus for skew monoidal categories, building on the recent formulation by one of the authors of a sequent calculus for the Tamari order (skew semigroup categories). In this calculus, antecedents consist of a stoup (an optional formula) followed by a context, and the connectives behave like in the standard monoidal sequent calculus except that the left rules may only be applied in stoup position. We prove that this calculus is sound and complete with respect to existence of maps in the free skew monoidal category, and moreover that it captures equality of maps once a suitable equivalence relation is imposed on derivations. We then identify a subsystem of focused derivations and establish that it contains exactly one canonical representative from each equivalence class. This coherence theorem leads directly to simple procedures for deciding equality of maps in the free skew monoidal category and for enumerating any homset without duplicates. Finally, and in the spirit of Lambek’s work, we describe the close connection between this proof-theoretic analysis and Bourke and Lack’s recent characterization of skew monoidal categories as left representable skew multicategories. We have formalized this development in the dependently typed programming language Agda.

We present a surprisingly new connection between two well-studied combinatorial classes: rooted connected chord diagrams on one hand, and rooted bridgeless combinatorial maps on the other hand. We describe a bijection between these two classes, which naturally extends to indecomposable diagrams and general rooted maps. As an application, this bijection provides a simplifying framework for some technical quantum field theory work realized by some of the authors. Most notably, an important but technical parameter naturally translates to vertices at the level of maps. We also give a combinatorial proof to a formula which previously resulted from a technical recurrence, and with similar ideas we prove a conjecture of Hihn. Independently, we revisit an equation due to Arquès and Béraud for the generating function counting rooted maps with respect to edges and vertices, giving a new bijective interpretation of this equation directly on indecomposable chord diagrams, which moreover can be specialized to connected diagrams and refined to incorporate the number of crossings. Finally, we explain how these results have a simple application to the combinatorics of lambda calculus, verifying the conjecture that a certain natural family of lambda terms is equinumerous with bridgeless maps.

We introduce a sequent calculus with a simple restriction of Lambek’s product rules that precisely captures the classical Tamari order, i.e., the partial order on fully-bracketed words (equivalently, binary trees) induced by a semi-associative law (equivalently, right rotation). We establish a focusing property for this sequent calculus (a strengthening of cut-elimination), which yields the following coherence theorem: every valid entailment in the Tamari order has exactly one focused derivation. We then describe two main applications of the coherence theorem, including: 1. A new proof of the lattice property for the Tamari order, and 2. A new proof of the Tutte-Chapoton formula for the number of intervals in the Tamari lattice ${𝑌}_{𝑛}$.

Any refinement system (= functor) has a fully faithful representation in the refinement system of presheaves, by interpreting types as relative slice categories, and refinement types as presheaves over those categories. Motivated by an analogy between side effects in programming and context effects in linear logic, we study logical aspects of this ‘positive’ (covariant) representation, as well as of an associated ‘negative’ (contravariant) representation. We establish several preservation properties for these representations, including a generalization of Day’s embedding theorem for monoidal closed categories. Then, we establish that the positive and negative representations satisfy an Isbell-style duality. As corollaries, we derive two different formulas for the positive representation of a pushforward (inspired by the classical negative translations of proof theory), which express it either as the dual of a pullback of a dual or as the double dual of a pushforward. Besides explaining how these constructions on refinement systems generalize familiar category-theoretic ones (by viewing categories as special refinement systems), our main running examples involve representations of Hoare logic and linear sequent calculus.

The main aim of the paper is to give a simple and conceptual account for the correspondence (originally described by Bodini, Gardy, and Jacquot) between α-equivalence classes of closed linear lambda terms and isomorphism classes of rooted trivalent maps on compact-oriented surfaces without boundary, as an instance of a more general correspondence between linear lambda terms with a context of free variables and rooted trivalent maps with a boundary of free edges. We begin by recalling a familiar diagrammatic representation for linear lambda terms, while at the same time explaining how such diagrams may be read formally as a notation for endomorphisms of a reflexive object in a symmetric monoidal closed (bi)category. From there, the “easy” direction of the correspondence is a simple forgetful operation which erases annotations on the diagram of a linear lambda term to produce a rooted trivalent map. The other direction views linear lambda terms as complete invariants of their underlying rooted trivalent maps, reconstructing the missing information through a Tutte-style topological recurrence on maps with free edges. As an application in combinatorics, we use this analysis to enumerate bridgeless rooted trivalent maps as linear lambda terms containing no closed proper subterms, and conclude by giving a natural reformulation of the Four Color Theorem as a statement about typing in lambda calculus.

The standard reading of type theory through the lens of category theory is based on the idea of viewing a type system as a category of well-typed terms. We propose a basic revision of this reading: rather than interpreting type systems as categories, we describe them as functors from a category of typing derivations to a category of underlying terms. Then, turning this around, we explain how in fact any functor gives rise to a generalized type system, with an abstract notion of typing judgment, typing derivations and typing rules. This leads to a purely categorical reformulation of various natural classes of type systems as natural classes of functors.

The main purpose of this paper is to describe the general framework (which can also be seen as providing a categorical analysis of refinement types), and to present a few applications. As a larger case study, we revisit Reynolds’ paper on “The Meaning of Types” (2000), showing how the paper’s main results may be reconstructed along these lines.

The concept of refinement in type theory is a way of reconciling the “intrinsic” and the “extrinsic” meanings of types. We begin with a rigorous analysis of this concept, settling on the simple conclusion that the type-theoretic notion of “type refinement system” may be identified with the category-theoretic notion of “functor”. We then use this correspondence to give an equivalent type-theoretic formulation of Grothendieck’s definition of (bi)fibration, and extend this to a definition of monoidal closed bifibrations, which we see as a natural space in which to study the properties of proofs and programs. Our main result is a representation theorem for strong monads on a monoidal closed fibration, describing sufficient conditions for a monad to be isomorphic to a continuations monad “up to pullback”.