The free bifibration on a functor
Fuente:
arXiv
Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866915732018692096 |
|---|---|
| author | Clarke, Bryce Scherer, Gabriel Zeilberger, Noam |
| author_facet | Clarke, Bryce Scherer, Gabriel Zeilberger, Noam |
| contents | We consider the problem of constructing the free bifibration generated by a functor of categories $p : D \to C$. 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 $Λ_p : Bifib(p)\to C$ in which objects of $Bifib(p)$ 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}(C)$, which is also the free double category with companions and conjoints (or fibrant double category) on $C$. The approach adapts smoothly to the more general task of building $(P,N)$-fibrations, where one only asks for pushforwards along arrows in $P$ and pullbacks along arrows in $N$ for some subsets of arrows; this encompasses Kock and Joyal's notion of _ambifibration_ when $(P,N)$ 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 $P$ and $N$. 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2511_07314 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | The free bifibration on a functor Clarke, Bryce Scherer, Gabriel Zeilberger, Noam Category Theory Logic in Computer Science 18N10, 18D30, 03B47, 03F05 We consider the problem of constructing the free bifibration generated by a functor of categories $p : D \to C$. 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 $Λ_p : Bifib(p)\to C$ in which objects of $Bifib(p)$ 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}(C)$, which is also the free double category with companions and conjoints (or fibrant double category) on $C$. The approach adapts smoothly to the more general task of building $(P,N)$-fibrations, where one only asks for pushforwards along arrows in $P$ and pullbacks along arrows in $N$ for some subsets of arrows; this encompasses Kock and Joyal's notion of _ambifibration_ when $(P,N)$ 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 $P$ and $N$. 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. |
| title | The free bifibration on a functor |
| topic | Category Theory Logic in Computer Science 18N10, 18D30, 03B47, 03F05 |
| url | https://arxiv.org/abs/2511.07314 |