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.

Optics are bidirectional data accessors that capture data transformation patterns such as accessing subfields or iterating over containers. Profunctor optics are a particular choice of representation supporting modularity, meaning that we can construct accessors for complex structures by combining simpler ones. Profunctor optics have previously been studied only in an unenriched and non-mixed setting, in which both directions of access are modelled in the same category. However, functional programming languages are arguably better described by enriched categories; and we have found that some structures in the literature are actually mixed optics, with access directions modelled in different categories. Our work generalizes a classic result by Pastro and Street on Tambara theory and uses it to describe mixed V-enriched profunctor optics and to endow them with V-category structure. We provide some original families of optics and derivations, including an elementary one for traversals. Finally, we discuss a Haskell implementation.