Reference. The free bifibration on a functor

Bryce Clarke, Gabriel Scherer, Noam Zeilberger · arXiv · 2025 · category-theory · arXiv
We consider the problem of constructing the free bifibration generated by a functor of categories 𝑝:𝐷→𝐶. 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 Λ𝑝:𝐵𝑖𝑓𝑖𝑏(𝑝)→𝐶 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_ ℤ(𝐶), 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 Δ, which contains the lattices of noncrossing partitions as quotients of its fibers by the Beck-Chevalley condition for bicartesian squares.

Cite
Cite as @clarke-2025-the (helia, typst) · \cite{clarke-2025-the} (LaTeX)
BibTeX
bibtex · 8 lines
@misc{clarke-2025-the,
  author = {Bryce Clarke and Gabriel Scherer and Noam Zeilberger},
  title = {The free bifibration on a functor},
  year = {2025},
  month = {11},
  eprint = {2511.07314},
  archiveprefix = {arXiv}
}
hayagriva YAML (typst)
yaml · 10 lines
clarke-2025-the:
  type: misc
  title: The free bifibration on a functor
  author:
  - Clarke, Bryce
  - Scherer, Gabriel
  - Zeilberger, Noam
  date: 2025-11
  serial-number:
    arxiv: '2511.07314'
Download: clarke-2025-the.bib · clarke-2025-the.yml
Cites 55 works (6 here)
With notes (6)

LNL polycategories and doctrines of linear logic shulman-2023-lnlLMCS · 2023
We define and study LNL polycategories, which abstract the judgmental structure of classical linear logic with exponentials. Many existing structures can be represented as LNL polycategories, including LNL adjunctions, linear exponential comonads, LNL multicategories, IL-indexed categories, linearly distributive categories with storage, commutative and strong monads, CBPV-structures, models of polarized calculi, Freyd-categories, and skew multicategories, as well as ordinary cartesian, symmetric, and planar multicategories and monoidal categories, symmetric polycategories, and linearly distributive and *-autonomous categories. To study such classes of structures uniformly, we define a notion of LNL doctrine, such that each of these classes of structures can be identified with the algebras for some such doctrine. We show that free algebras for LNL doctrines can be presented by a sequent calculus, and that every morphism of doctrines induces an adjunction between their 2-categories of algebras.
DOI · arXiv

Displayed Categories ahrens-lumsdaine-2019lmcs · 2019
We introduce and develop the notion of displayed categories. A displayed category over a category C is equivalent to “a category D and functor F : D –> C”, but instead of having a single collection of “objects of D” with a map to the objects of C, the objects are given as a family indexed by objects of C, and similarly for the morphisms. This encapsulates a common way of building categories in practice, by starting with an existing category and adding extra data/properties to the objects and morphisms. The interest of this seemingly trivial reformulation is that various properties of functors are more naturally defined as properties of the corresponding displayed categories. Grothendieck fibrations, for example, when defined as certain functors, use equality on objects in their definition. When defined instead as certain displayed categories, no reference to equality on objects is required. Moreover, almost all examples of fibrations in nature are, in fact, categories whose standard construction can be seen as going via displayed categories. We therefore propose displayed categories as a basis for the development of fibrations in the type-theoretic setting, and similarly for various other notions whose classical definitions involve equality on objects. Besides giving a conceptual clarification of such issues, displayed categories also provide a powerful tool in computer formalisation, unifying and abstracting common constructions and proof techniques of category theory, and enabling modular reasoning about categories of multi-component structures. As such, most of the material of this article has been formalised in Coq over the UniMath library, with the aim of providing a practical library for use in further developments.

We introduce and develop the notion of displayed categories. A displayed category over a category 𝐶 is equivalent to “a category 𝐷 and functor 𝐹:𝐷→𝐶, but instead of having a single collection of “objects of 𝐷” with a map to the objects of 𝐶, the objects are given as a family indexed by objects of 𝐶, and similarly for the morphisms. This encapsulates a common way of building categories in practice, by starting with an existing category and adding extra data/properties to the objects and morphisms. The interest of this seemingly trivial reformulation is that various properties of functors are more naturally defined as properties of the corresponding displayed categories. Grothendieck fibrations, for example, when defined as certain functors, use equality on objects in their definition. When defined instead as certain displayed categories, no reference to equality on objects is required. Moreover, almost all examples of fibrations in nature are, in fact, categories whose standard construction can be seen as going via displayed categories. We therefore propose displayed categories as a basis for the development of fibrations in the type-theoretic setting, and similarly for various other notions whose classical definitions involve equality on objects. Besides giving a conceptual clarification of such issues, displayed categories also provide a powerful tool in computer formalisation, unifying and abstracting common constructions and proof techniques of category theory, and enabling modular reasoning about categories of multi-component structures. As such, most of the material of this article has been formalised in Coq over the UniMath library, with the aim of providing a practical library for use in further developments.

DOI · arXiv

An Isbell duality theorem for type refinement systems mellies-2017-anMSCS · 2017
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.
DOI · arXiv

Functors are type refinement systems mellies_zeilberger_2015POPL · 2015

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.

PDF · DOI · pldb

Framed bicategories and monoidal fibrations shulman_2008TAC · 2008

In some bicategories, the 1-cells are ‘morphisms’ between the 0-cells, such as functors between categories, but in others they are ‘objects’ over the 0-cells, such as bimodules, spans, distributors, or parametrized spectra. Many bicategorical notions do not work well in these cases, because the ‘morphisms between 0-cells’, such as ring homomorphisms, are missing. We can include them by using a pseudo double category, but usually these morphisms also induce base change functors acting on the 1-cells. We avoid complicated coherence problems by describing base change ‘nonalgebraically’, using categorical fibrations. The resulting ‘framed bicategories’ assemble into 2-categories, with attendant notions of equivalence, adjunction, and so on which are more appropriate for our examples than are the usual bicategorical ones.

We then describe two ways to construct framed bicategories. One is an analogue of rings and bimodules which starts from one framed bicategory and builds another. The other starts from a ‘monoidal fibration’, meaning a parametrized family of monoidal categories, and produces an analogue of the framed bicategory of spans. Combining the two, we obtain a construction which includes both enriched and internal categories as special cases.

Web

The mathematics of sentence structure lambek58Amer. Math. Monthly · 1958
DOI
External (49)
clarke-2025-the reference entries/refs/clarke-2025-the/clarke-2025-the.hel