On a fibrational construction for optics, lenses, and Dialectica categories

(Examples of fibrations) For a category \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi, we denote by \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi ^\downarrow the category of morphisms in \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi with arrows given by the commutative squares.

1. Domain fibration. For any category \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi, the domain projection \mathrm{dom} := \mathrm{dom}_{ \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi } : { \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi }^\downarrow \to \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi is a fibration. For u:I \to J in \relax \StrLen{X}[\catarglen] \ifnum\catarglen=1 \mathcal{X} \else \mathbf{X} \fi, a cartesian lift of u with respect to an arrow g : J\to Y is given by the square:

   \begin{tikzcd}[sep=4ex] I & J \\ X & Y \arrow["u\fatsemi g"', from=1-1, to=2-1] \arrow[Rightarrow, no head, from=2-1, to=2-2] \arrow["u", from=1-1, to=1-2] \arrow["g", from=1-2, to=2-2] \end{tikzcd}

2. Codomain fibration. If \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi has all pullbacks, then the codomain projection \mathrm{cod} := \mathrm{cod}_{ \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi } : \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi ^\downarrow \to \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi is a fibration, also called the fundamental fibration of \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi. If \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi is locally cartesian closed, the codomain fibration gives rise to a model of dependent type theory with \Sigma- and \Pi-types [seely1984locally]. The idea is to interpret a type X in context (i.e., a list of free variables) I as a morphism X \to I, hence an object of the slice \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi /I, which is the fiber of \mathrm{cod} at I : \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi.

   Given an arrow u : J \to I in \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi together with a map p : X \to I, a \mathrm{cod}-cartesian lift of u with respect to p is given by pullback:

   \begin{tikzcd}[sep=4ex] {u^*X} & X \\ J & I \arrow["u", from=2-1, to=2-2] \arrow["p", from=1-2, to=2-2] \arrow[from=1-1, to=2-1] \arrow[from=1-1, to=1-2] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2] \end{tikzcd}

   This corresponds to substituting the variables in context I along u.

3. Simple fibration. Whereas the codomain fibration models arbitrary dependent types in context I, we might want to restrict to the case of simple types. A constant type is a dependent type over the terminal context 1, hence a map X \to 1, or equivalently, just an object X. We can then view X as a type over any context, by considering the pullback:

   \begin{tikzcd}[sep=4ex] {I \times X} & X \\ I & 1 \arrow[from=2-1, to=2-2] \arrow[from=1-2, to=2-2] \arrow[from=1-1, to=2-1] \arrow[from=1-1, to=1-2] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2] \end{tikzcd}

   Therefore, as soon as \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi admits finite products, the simple fibration is given by the subfunctor of \mathrm{cod}_{ \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi } spanned by product projections I \times X \to I. It can also be described, up to fibered equivalence, as follows. Define the category \relax \StrLen{S}[\catarglen] \ifnum\catarglen=1 \mathcal{S} \else \mathbf{S} \fi ( \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi ) by taking as objects pairs (I,X) of \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi and as morphisms (I,X) \to (J,Y) pairs of morphisms (u : I \to J,f : I \times X \to Y) in \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi. The simple fibration S : \relax \StrLen{S}[\catarglen] \ifnum\catarglen=1 \mathcal{S} \else \mathbf{S} \fi ( \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi ) \to \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi is the functor defined by S(I,X) := I and S(u,f) := u. This is indeed a fibration, where a cartesian lift of u : I \to J with respect to (J,Y) is given by the map (u,\pi_Y): (I,Y) \to (J,Y) with \pi_Y : I \times Y \to Y.

4. Subobject fibration. Let \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi have all pullbacks. We can consider the full subfibration

   \begin{tikzcd}[sep=4ex] {{ \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi }^\downarrow\vert_\mathsf{mono}} && { \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi ^\downarrow} \\ & { \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi } \arrow[hook, from=1-1, to=1-3] \arrow[from=1-1, to=2-2] \arrow[from=1-3, to=2-2] \end{tikzcd}

   of monomorphisms in \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi. Quotienting out by the relation that two monomorphisms shall be equal if and only if they factor through each other (necessarily through a monomorphism), we obtain the subobject fibration \mathrm{sub}:{ \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi ^\subseteq} \to \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi. The subobject fibration is typically used as an elementary example of fibration of predicates on the objects of \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi.

5. Family fibration. Consider a category \relax \StrLen{X}[\catarglen] \ifnum\catarglen=1 \mathcal{X} \else \mathbf{X} \fi with pullbacks and P : \relax \StrLen{E}[\catarglen] \ifnum\catarglen=1 \mathcal{E} \else \mathbf{E} \fi \to \relax \StrLen{X}[\catarglen] \ifnum\catarglen=1 \mathcal{X} \else \mathbf{X} \fi a fibration.

   Let \relax \StrLen{Fam}[\catarglen] \ifnum\catarglen=1 \mathcal{Fam} \else \mathbf{Fam} \fi (P) : P \downarrow \relax \StrLen{X}[\catarglen] \ifnum\catarglen=1 \mathcal{X} \else \mathbf{X} \fi \to \relax \StrLen{X}[\catarglen] \ifnum\catarglen=1 \mathcal{X} \else \mathbf{X} \fi be the functor constructed as follows:

   \begin{tikzcd}[sep=4ex] {P\downarrow \relax \StrLen{X}[\catarglen] \ifnum\catarglen=1 \mathcal{X} \else \mathbf{X} \fi } && { \relax \StrLen{E}[\catarglen] \ifnum\catarglen=1 \mathcal{E} \else \mathbf{E} \fi } \\ { \relax \StrLen{X}[\catarglen] \ifnum\catarglen=1 \mathcal{X} \else \mathbf{X} \fi ^\downarrow} && { \relax \StrLen{X}[\catarglen] \ifnum\catarglen=1 \mathcal{X} \else \mathbf{X} \fi } \\ \relax \StrLen{X}[\catarglen] \ifnum\catarglen=1 \mathcal{X} \else \mathbf{X} \fi \arrow[from=1-1, to=2-1] \arrow["\mathrm{dom}", from=2-1, to=2-3] \arrow[from=1-1, to=1-3] \arrow["P", from=1-3, to=2-3] \arrow["\mathrm{cod}", from=2-1, to=3-1] \arrow["{ \relax \StrLen{Fam}[\catarglen] \ifnum\catarglen=1 \mathcal{Fam} \else \mathbf{Fam} \fi (P)}"', curve={height=24pt}, from=1-1, to=3-1] \arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-3] \end{tikzcd}

   We call \relax \StrLen{Fam}[\catarglen] \ifnum\catarglen=1 \mathcal{Fam} \else \mathbf{Fam} \fi (P) : P \downarrow \relax \StrLen{X}[\catarglen] \ifnum\catarglen=1 \mathcal{X} \else \mathbf{X} \fi \to \relax \StrLen{X}[\catarglen] \ifnum\catarglen=1 \mathcal{X} \else \mathbf{X} \fi the family fibration of P. Indeed this is a fibration: any pullback of P is a fibration, so is \mathrm{dom}^*P. Since \mathrm{cod} is a fibration, as \relax \StrLen{X}[\catarglen] \ifnum\catarglen=1 \mathcal{X} \else \mathbf{X} \fi has all pullbacks, then so is their composite \mathrm{cod} \fatsemi \mathrm{dom}^*P= \relax \StrLen{Fam}[\catarglen] \ifnum\catarglen=1 \mathcal{Fam} \else \mathbf{Fam} \fi (P). Objects in the fiber \mathrm{d} \relax \StrLen{Fam}[\catarglen] \ifnum\catarglen=1 \mathcal{Fam} \else \mathbf{Fam} \fi (P)(I) are given by pairs (f:X \to I, \alpha : \mathrm{d} P(X)). In fact, if P is an arbitrary functor, \relax \StrLen{Fam}[\catarglen] \ifnum\catarglen=1 \mathcal{Fam} \else \mathbf{Fam} \fi (P) is always an opfibration, the free opfibration generated by P. Thus, \relax \StrLen{Fam}[\catarglen] \ifnum\catarglen=1 \mathcal{Fam} \else \mathbf{Fam} \fi (P) is both a fibration and an opfibration. One can show that opcartesian transport serves as taking sums (or existential quantification), and that they commute with cartesian transport, serving as reindexing, in a canonical way (via the Beck–Chevalley isomorphisms). Hence, the family construction on a fibration P can be understood as the result of freely adding sums to P, which are internally indexed, i.e., indexed by the base category \relax \StrLen{X}[\catarglen] \ifnum\catarglen=1 \mathcal{X} \else \mathbf{X} \fi. Accordingly, we also write \relax \StrLen{Fam}[\catarglen] \ifnum\catarglen=1 \mathcal{Fam} \else \mathbf{Fam} \fi (P) for \relax \StrLen{Fam}[\catarglen] \ifnum\catarglen=1 \mathcal{Fam} \else \mathbf{Fam} \fi (P).

   One could replace \mathrm{dom} in the above definition by a full subfibration of itself, corresponding to a version of the family construction that is the sum completion only with respect to a chosen class of morphisms of \relax \StrLen{X}[\catarglen] \ifnum\catarglen=1 \mathcal{X} \else \mathbf{X} \fi.

If \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi is a cartesian monoidal category, then the total category of its associated simple fibration S: \relax \StrLen{S}[\catarglen] \ifnum\catarglen=1 \mathcal{S} \else \mathbf{S} \fi ( \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi ) \to \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi is again cartesian, meaning we can form towers of arbitrary height by iterating the construction of simple fibrations.

Likewise, when \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi is finitely complete we can form towers \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi ^{\downarrow^n} \to \cdots \to \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi ^\downarrow \to \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi of arbitrary height where the i-th level is the category of i-dimensional commutative cubes in \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi.

More generally, suppose P: \relax \StrLen{E}[\catarglen] \ifnum\catarglen=1 \mathcal{E} \else \mathbf{E} \fi \to \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi is a full comprehension category [jacobs_comprehension_1993], meaning it admits a right adjoint 1: \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi \to \relax \StrLen{E}[\catarglen] \ifnum\catarglen=1 \mathcal{E} \else \mathbf{E} \fi (a fibered terminal object) as well as a further right adjoint (comprehension) \{-\}: \relax \StrLen{E}[\catarglen] \ifnum\catarglen=1 \mathcal{E} \else \mathbf{E} \fi \to \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi. By repeatedly pulling back P along \{-\} we can form towers of fibrations of arbitrary height.

As anticipated, optics can be constructed as dialenses of height 2, if of a bizarre kind. First, recall from [braithwaite_fibre_2021] that every (strict, for simplicity) action \bullet : \relax \StrLen{M}[\catarglen] \ifnum\catarglen=1 \mathcal{M} \else \mathbf{M} \fi \times \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi \to \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi of a monoidal category \relax \StrLen{M}[\catarglen] \ifnum\catarglen=1 \mathcal{M} \else \mathbf{M} \fi on a category \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi can be repackaged as a 2-opfibration \relax \StrLen{Para}[\catarglen] \ifnum\catarglen=1 \mathcal{Para} \else \mathbf{Para} \fi (\bullet) \to B \relax \StrLen{M}[\catarglen] \ifnum\catarglen=1 \mathcal{M} \else \mathbf{M} \fi, where \relax \StrLen{Para}[\catarglen] \ifnum\catarglen=1 \mathcal{Para} \else \mathbf{Para} \fi (\bullet) is the bicategory of \relax \StrLen{M}[\catarglen] \ifnum\catarglen=1 \mathcal{M} \else \mathbf{M} \fi-parametric \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi-morphisms (see [Capucci_2022]) and the projection to B \relax \StrLen{M}[\catarglen] \ifnum\catarglen=1 \mathcal{M} \else \mathbf{M} \fi is given by projection out the parameter of a morphism. Here let’s ignore the 2-dimensional information and just consider this as an opfibration (because every 2-opfibration has an underlying 1-opfibration, cf. [hermida_properties_1999, Definition 2.1]).

Recall the 1-dimensional data of \relax \StrLen{Para}[\catarglen] \ifnum\catarglen=1 \mathcal{Para} \else \mathbf{Para} \fi (\bullet): its objects are the same of \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi while its 1-cells are pairs (m \in \relax \StrLen{M}[\catarglen] \ifnum\catarglen=1 \mathcal{M} \else \mathbf{M} \fi , f:m \bullet X \to X), composing in the obvious way.

Opcartesian lifts for the functor \relax \StrLen{Para}[\catarglen] \ifnum\catarglen=1 \mathcal{Para} \else \mathbf{Para} \fi (\bullet) \to B \relax \StrLen{M}[\catarglen] \ifnum\catarglen=1 \mathcal{M} \else \mathbf{M} \fi are constructed as follows:

Further on, we’ll abbreviate (m, 1_{m \bullet X}) with m_X.

Then given two left \relax \StrLen{M}[\catarglen] \ifnum\catarglen=1 \mathcal{M} \else \mathbf{M} \fi-actegories ( \relax \StrLen{C}[\catarglen] \ifnum\catarglen=1 \mathcal{C} \else \mathbf{C} \fi ,\bullet) and ( \relax \StrLen{D}[\catarglen] \ifnum\catarglen=1 \mathcal{D} \else \mathbf{D} \fi , \circ), one can construct the following tower of opfibrations:

Then its iterated dual produces preoptics (Def. 3.4):