Proposition [efr-XFAO]

Suppose \mathcal {D} is a Markov fibration so that each pullback functor f^*: \mathcal {D}_Y \to \mathcal {D}_X for f: X \to Y \in \mathcal {C}_\mathrm {det} can be taken to be bijective on objects, and that these can furthermore be chosen strictly functorial (so that (fg)^* = g^*f^*). Then, writing objects \bar {X} \in \mathcal {D}_X as \binom {A \in \mathcal {D}_*}{X \in \mathcal {C}}, where A is the unique object in \mathcal {D}_* which pulls back to \bar {X} under the deletion X \to *, (note that this means f^*\binom {A}{Y} = \binom {A}{X}) we may characterize the fiberwise dual as having hom-sets \mathcal {D}^{\mathrm {fop}}(\binom {A}{X},\binom {B}{Y}) = \mathcal {D}(\binom {B}{X},\binom {A}{Y})

Proof

The correspondence in both directions is obvious by just formally reversing the direction of the map f: \binom {A}{M} \to \binom {B}{M} in a representing tuple X \leftarrow M \to Y, a: X \to M, f---the fact that this assignment respects the equivalence relation follows from the fact that the monad preserves fiberwise opposites.

Context

Markov Fibrations [efr-U4RA]

Recall that, given a functor R: \mathcal {C} \to \mathcal {D} with left adjoint L, there is a "standard resolution" of any object X \in \mathcal {C}, given by the "cofork" LRLRX \rightrightarrows LRX \to X, where the two parallel maps are the two possible applications of the adjunction counit. The adjunction is monadic if and only if this is always a coequalizer, in which case the RL-algebra corresponding to X is RLRX \to RX---conversely, given an algebra \alpha : RLA \to A, there are two parallel maps LRLA \rightrightarrows LA (given by L(\alpha ) and the counit,) and the object in \mathcal {C} corresponding to this algebra is given by this coequalizer.

Example

Consider the adjunction |-|: \mathsf {Mon} \leftrightarrows \mathsf {Set} : (-)^* between the category of monoids and the category of sets. Given a monoid M, |M|^* consists of lists of elements in M, and ||M|^*|^* consists of lists of such lists. The two maps ||M|^*|^* \to |M|^* consist in either concatenating the lists, or replacing each list with its product. Clearly these two maps are coequalized by the product map |M|^* \to M. Moreover it's clear that two lists have the same product if and only if they are identified in this coequalizer (simply consider a singleton list-of-lists, which identifies any given list with the singleton corresponding to its product).

As a generalization of this, if this coequalizer exists for every algebra, they form a left adjoint to the canonical functor \mathcal {C} \to \mathsf {Alg}_\mathcal {D}(RL). Since we have seen that the monad of free Markov prefibrations commutes with taking fiberwise opposites, we may hope that such a left adjoint exists---a simple argument shows that, if it is, it is fully faithful, and we may say that those prefibrations in the image are the "fibrations" and define their fiberwise opposite as the fiberwise opposite applied to their underlying algebras. Although it turns out to not be quite so simple, we will take this idea as our starting point.

Example

Let \mathsf {GrpTop} be the category of topological groups, and let R: \mathsf {GrpTop} \to \mathsf {Set} forget both the group structure and the topology. Clearly this is right adjoint to the free group in the discrete topology, and the monad of this adjunction is the free group monad, which we write RL for now. The canonical comparison functor \mathsf {GrpTop} \to \mathsf {Grp} just forgets the topology. Given a (non-topological) group, described by a map RLG \to G, we can form the diagram of topological groups LRLG \rightrightarrows LG. Here LG is the free, discrete group on G and LRLG is the free discrete group on the underlying set of LG. Their coequalizer is simply G equipped with the discrete topology, which is indeed the left adjoint to \mathsf {GrpTop} \to \mathsf {Grp}

In what follows, we will denote the monad \overline {(-)}|_\mathrm {det} simply by \operatorname {Free} to avoid too many complicated nestings of overlines and parentheses.

Definition Markov Fibration [efr-HVUT]

If \mathcal {D} is a Markov prefibration, we call it a Markov fibration if the diagram \overline {\operatorname {Free}(\mathcal {D}|_\mathrm {det})} \rightrightarrows \overline {\mathcal {D}|_\mathrm {det}} \to \mathcal {D} is a coequalizer in \mathsf {Cat}_{/\mathcal {C}}.

Given an algebra \alpha : \operatorname {Free}(\mathcal {D}_0) \to \mathcal {D}_0 of the free Markov prefibration monad, let \overline {\operatorname {Free}(\mathcal {D}_0)} \rightrightarrows \overline {\mathcal {D}_0} \in \mathsf {MarkPreFib} be as above. We say \alpha presents a Markov fibration if the coequalizer of these maps in \mathsf {Cat}_{/\mathcal {C}} is a Markov prefibration.

The terminology "presents a Markov fibration" is justified by the following proposition.

Proposition [efr-MAUM]

Let \alpha : \operatorname {Free}(\mathcal {D}_0) \to \mathcal {D}_0 be stochastic module which presents a Markov fibration. Then the underlying algebra of the Markov prefibration obtained as the coequalizer of \overline {\operatorname {Free}(\mathcal {D}_0)} \rightrightarrows \bar {\mathcal {D}_0} is isomorphic to \alpha , and in particular this prefibration is a Markov fibration.

This correspondence determines an equivalence of categories between the full subcategory \mathsf {MarkFib}(\mathcal {C}) of \mathsf {MarkPreFib}(\mathcal {C}) spanned by the Markov fibrations, and the full subcategory \mathsf {SFib}(\mathcal {C})^p \subseteq \mathsf {SFib}(\mathcal {C}) spanned by those algebras which present a Markov fibration.

Proof

Let \alpha be an algebra as assumed, and let \mathcal {D}_0^\alpha \in \mathsf {MarkPreFib} denote the coequalizer given. By general nonsense there is an induced functor \mathcal {D}_0 \to \mathcal {D}_0^\alpha |_\mathrm {det} which is moreover an algebra homomorphism---the claim is that this is an isomorphism. By Lemma [efr-L7L2], pullback to the deterministic part preserves these coequalizers, so this amounts to the claim that the diagram \operatorname {Free}^2(\mathcal {D}_0) \rightrightarrows \operatorname {Free}(\mathcal {D}_0) \to \mathcal {D}_0 is a coequalizer. But this is true for any algebra of any monad (in fact, the unit gives a splitting of this coequalizer).

By general nonsense the fibration associated to an algebra which presents a fibration forms a partial left adjoint to \mathsf {MarkPreFib}(\mathcal {C}) \to \mathsf {SFib}(\mathcal {C}). This left adjoint, by the above, has its image inside \mathsf {MarkFib}, and hence there is an adjunction \mathsf {MarkFib}(\mathcal {C}) \leftrightarrows \mathsf {SFib}(\mathcal {C})^p. The preceding furthermore proves that the unit of this adjunction is the identity, which implies that the left adjoint is fully faithful---but by definition it is essentially surjective, finishing the argument.

Let us briefly summarize the relationship between Markov prefibrations, Markov fibrations, and stochastic module fibrations at this stage.

  • A stochastic module fibration is a (Grothendieck) fibration \mathcal {D} over \mathcal {C}_\mathrm {det}, equipped with some extra structure involving the whole category \mathcal {C}. Given a deterministic map f: A \to B two objects X,Y \in \mathcal {D}_B, and a map \phi : f^*X \to f^*Y, we can think of this as a map parameterized by the fibers A_b. Given a stochastic section s: B \to A, the stochastic module structure picks out a map X \to Y \in \mathcal {D}_B corresponding to choosing this parameter randomly according to s.
  • A Markov prefibration is a category \mathcal {D} over \mathcal {C} with a particular unique lifting property. In the above situation, it gives a unique lift X \to f^*X of s, corresponding to choosing a \in A_b according to s and leaving the x \in X-coordinate unchangd. By composing this lift with \phi , then with the Cartesian f^*Y \to Y, we get a stochastic module structure on the part of \mathcal {D} lying over deterministic maps (which is also a Grothendieck fibration).

    • Given a stochastic module structure, there is a way of generating a category over \mathcal {C}, by freely adding the lifts corresponding to a Markov prefibration, then quotienting by the relations implied by the stochastic module structure. This does not necessarily yield a Markov prefibration.

    A Markov prefibration is called a Markov fibration if it is presented by its underlying stochastic module in the above sense.

Definition Weak supports [efr-YFV2]

Let \mathcal {D}_0 \to \mathcal {C}_\mathrm {det} be a stochastic module fibration.

Let \alpha : X \to M be a stochastic section, let \bar {X} \in \mathcal {D}_{0,X} be an object, and let \phi : \bar {X}_M \to \bar {X}_M \in \mathcal {D}_{0,M} be an endomorphism of its pullback. Observe that if there exists f: N \to M so that f^*(\phi ) = 1 and \alpha factors over f, then \alpha _*(\phi ) = 1. We say \mathcal {D}_0 has weak supports if this implication is an equivalence

We will make use of the following lemma:

Lemma [efr-L7L2]

Let F,G: \mathcal {D} \rightrightarrows \mathcal {D}' be a parallel pair in \mathsf {Cat}_{/\mathcal {C}}, and suppose both are identity on objects. Suppose moreover this is a reflexive pair, i.e there is some S: \mathcal {D}' \to \mathcal {D} so that FS = GS = 1_{\mathcal {D}'}. Then the coequalizer in \mathsf {Cat}_{/\mathcal {C}} is again identity on objects, and is given on hom-sets simply by the coequalizer of the parallel pair \mathcal {D}(x,y) \rightrightarrows \mathcal {D}'(x,y)

Proof

The only nontrivial part is to verify that composition is well-defined on the equivalence classes in \mathcal {D}'(x,y)/\sim . It suffices to see that post- and precomposition with a fixed morphism both preserve this equivalence relation. Take some f: x \to y \in \mathcal {C}, and h : y \to z \in \mathcal {C}'. We must show that hF(f) = hG(f). But simply write hF(f) = F(S(h)f) \sim G(S(h)f) = hG(f), and we are done. Clearly the other side follows by duality, finishing the proof.

Proposition Construction of \mathsf {SChart}(\mathcal {D}_0) [efr-TBZZ]

Let \mathcal {D}_0 be a fibration equipped with a stochastic module structure. Consider the equivalence relation on \overline {\mathcal {D}_0}(\bar {X},\bar {Y}) which identifies two precharts (M, \phi ), (N, \phi ') if there exists a map f: N \to M over X,Y and a stochastic section s of f which preserves the section from X, so that s^*\phi ' = \phi (note that this makes sense because pullbacks compose).

Then:

  1. This equivalence relation respects composition, and so defines a category which we denote \mathsf {SChart}(\mathcal {D}_0)
  2. In \mathsf {Cat}_{/\mathcal {C}}, \overline {\operatorname {Free}(\mathcal {D}_0)} \rightrightarrows \overline {\mathcal {D}_0} \to \mathsf {SChart}(\mathcal {D}_0) is a coequalizer diagram. In particular, \mathcal {D}_0 presents a Markov fibration if and only if \mathsf {SChart}(\mathcal {D}_0) is a Markov prefibration (in which case \mathsf {SChart}(\mathcal {D}_0) is the fibration it presents)
  3. If \mathcal {D}_0 has weak supports, \mathsf {SChart}(\mathcal {D}_0) is a prefibration

Proof

Recall that the fibration \operatorname {Free}(\mathcal {D}_0) has fibers whose morphisms \bar {X} \to \bar {X}' are given by tuples s: X \to M: p, p^*\bar {X} \to p^*\bar {X}' (up to a certain equivalence relation). Forming the free Markov prefibration \overline {\operatorname {Free}(\mathcal {D}_0)} on this fibration, we find that the morphisms are given by diagrams

equipped with a map \phi : p^*q^*\bar {X} \to p^*r^*\bar {Y}. The two maps \overline {\operatorname {Free}(\mathcal {D}_0)} \to \overline {\mathcal {D}_0} carry such a thing to first, the map resulting from forgetting M and just composing q,r with p to get a span (and composing the sections to get a new section), and secondly, the map with apex M obtained by using the stochastic module structure to push \phi down into a map over M. It is clear that this is equivalently the equation described in the theorem. This establishes points 1. and 2., since by Lemma [efr-L7L2] we can compute such coequalizers hom-set by hom-set.

Now we wish to prove that \mathsf {SChart}(\mathcal {D}_0) is a Markov prefibration given weak supports. Since by the coequalizer presentation, its deterministic part is isomorphic to \mathcal {D}_0, the fibration property is automatic. It remains to verify that, given a triangle

in \mathcal {C} with the vertical and horizontal maps deterministic, an object \bar {A} \in \mathcal {D}_{0,Y} and Cartesian maps \bar {A}_X \to \bar {A} \leftarrow \bar {A}_Z, there exists a unique lift \bar {A}_X \to \bar {A}_Z in \mathsf {SChart}(\mathcal {D}_0).

Such a lift is given by a diagram

equipped with p^*\bar {A}_X \to q^*\bar {A}_Z. By taking the equalizer of the two maps M \to Y (the section factors over this), we may assume these two are equal, which implies that the pulled-back objects are equal---denote this object \bar {A}_M. Now the hypothesis is that after postcomposing with the Cartesian map \bar {A}_Z \to \bar {A}, this gives the map \bar {A}_X \to \bar {A}. This postcomposition is given simply by postcomposing the leg M \to Z with the map Z \to Y (and observing that, by functoriality of pullbacks, this does not alter the pulled-back object). Then the claim is that integrating this map \bar {A}_M \to \bar {A}_M down into a map \bar {A}_X \to \bar {A}_X, it gives the identity. But by assumption this means we can pull back to some object M' \to M (lifting the section from X) where the two maps are already equal to the identity. But this pull-back can be applied to the original map \bar {A}_X \to \bar {A}_Z as well. But this implies every such map is equal to the one represented by the diagram
and the identity on \bar {A}_{X \otimes Y}, with the map M' \to X \otimes Y giving the witness, since identities pull back. This map only depends on the underlying X \to Y, hence \mathsf {SChart}(\mathcal {D}_0) is indeed a prefibration.

It is not apparent whether weak supports are necessary for \mathsf {SChart}(\mathcal {D}_0) to be a prefibration. We have not found any counterexample, but in general the equivalence relation on charts is fairly complicated, so it is not apparent how to prove the necessity. We will generally not be too bothered about assuming weak supports instead of the more nebulous assumption that \mathcal {D}_0 presents a Markov fibration.

Lemma [efr-26SF]

Let (M,\phi ) and (N,\psi ) be two representatives of charts. Given some possibly stochastic map f: M \to N over X and Y, recall (Lemma [efr-VF6V]) that we can define f^*\psi , regardless of whether f is deterministic or the section of a deterministic map. If there exists such a map f, we can always factor it over the pullback M \times _{X \times Y} N as a section followed by a deterministic map. Hence the equivalence relation defining \mathsf {SChart} is equivalent to the relation identifying two representatives whenever there exists such an f with f^*\psi = \phi

Remark [efr-XZRN]

By construction, for each Markov prefibration \mathcal {D}, there is a canonical functor \mathsf {SChart}(\mathcal {D}|_\mathrm {det}) \to \mathcal {D} over \mathcal {C}, which restricts to an isomorphism on the deterministic part (and in particular preserves Cartesian morphisms). \mathcal {D} is a Markov fibration if and only if this is an isomorphism.

Also by construction, given a morphism of stochastic modules F: \mathcal {D}_0 \to \mathcal {D}_0', there is an induced functor \mathsf {SChart}(\mathcal {D}) \to \mathsf {SChart}(\mathcal {D}') over \mathcal {C}. This restricts to F on the deterministic part and in particular preserves Cartesian morphisms.

Proposition [efr-1YS9]

Let \mathcal {D}_0 be a stochastic module fibration. Then \mathcal {D}_0 presents a Markov fibration if and only if \mathcal {D}_0^\mathrm {fop} does it.

Proof

Consider a triangle of this for in \mathcal {C}:

where the maps to Z are deterministic. Suppose given Cartesian lifts \bar {X} \to \bar {Z}, \bar {Y} \to \bar {Z} of the cospan. These are the same in both cases, coming from Cartesian maps in \mathcal {D}_0 \mathcal {D}_0^\mathrm {fop} (which are the same). We must show that there is a unique lift of f to a chart in \mathsf {SChart}(\mathcal {D}_0) if and only if there is a unique lift to a chart in \mathsf {SChart}(\mathcal {D}_0^\mathrm {fop}). Clearly it suffices to prove the "only if" implication, so suppose \mathsf {SChart}(\mathcal {D}_0) is a prefibration.

By passing to the equalizer as in the proof that \overline {\mathcal {D}_0} is a prefibration, we may assume that any such lift is represented by a diagram

where the outer square and the triangle X \to M \to Y commutes, and f' is a section.

Take such a diagram and let \phi : \bar {Z}_M \to \bar {Z}_M be the map representing a chart. Then the claim is there exists some zig-zag of chart equivalences identifying (M,\phi ) with (M,1). But clearly this is invariant under passing to the fiberwise opposite, and so \mathcal {D}^\mathrm {fop} is also a prefibration.

Definition Stochastic charts and lenses [efr-ANBC]

We refer to \mathsf {SChart}(\mathcal {D}_0) as the category of stochastic charts in \mathcal {D}_0. We refer to \mathsf {SChart}(\mathcal {D}_0^\mathrm {fop}) as stochastic lenses and denote it also \mathsf {SLens}(\mathcal {D}_0)

Example [efr-IAFO]

Kl(\Delta )^\to is a Markov fibration. We have already seen that it is a Markov prefibration, and that the map from the coreflection is full. So it suffices to prove faithfulness. Consider a map in {Kl(\Delta )^\to |_\mathrm {det}}, given by a diagram

We can factor the section X \to M as X \to X \times Y \to M, where the first map is just the pairing and the second is a conditional distribution. This induces a factorization of the lift \bar {X} \to M \times _X \bar {X} over \bar {X} \to \bar {X} \times Y. By composing the map M \times _X \bar {X} \to \bar {Y} with this factorization to build the map \bar {X} \times Y \to \bar {Y}, we have found a new representative for the same map.

Hence every map over X \to Y has a representative where the residual is X \times Y. We would like to argue that, since the map \bar {X} \times Y \to \bar {Y} is given by the conditional distribution of the composite map \bar {X} \to \bar {Y}, it is uniquely determined by it, and thus if two distinct maps in \overline {Kl(\Delta )^\to |_\mathrm {det}} have the same underlying map in Kl(\Delta )^\to , they must have equal representatives of this form, and so be identified in the coreflection (which must therefore be isomorphic to Kl(\Delta )^\to ). But of course, the two maps may only be almost certainly equal.

In this case, there is a simple fix: instead of taking X \times Y as the residual, take the subset S given by those pairs (x,y) where y has positive probability given x. The pairing factors over this, of course, and two maps \bar {X} \times _X S \to \bar {Y} which give the same distribution \bar {X} \to \bar {Y} really must have the same value on every point. This proves that \mathsf {SChart}(Kl(\Delta )^\to ) \to (Kl(\Delta ))^\to is faithful and hence an isomorphism.

Example [efr-C5RE]

\mathsf {BorelStoch}^\to , as we have noted, is a Markov prefibration, and hence induces a stochastic module structure on \mathsf {BorelStoch}^\to |_\mathrm {det}. This structure does not present a Markov fibration. To see this, note that in that case its fiberwise opposite would also present a Markov fibration. Then this fibration, \mathsf {SLens}(\mathsf {BorelStoch}^\to |_\mathrm {det}), would be a prefibration whose deterministic part was \mathsf {BorelStoch}^\to |_\mathrm {det}^\mathrm {fop}. But Example [efr-8B5X] shows that this is impossible.

Proposition [efr-8SXB]

Let \mathcal {C} be a Markov category with supports. Then the stochastic module induced by \mathcal {C}^\to \to \mathcal {C} presents a Markov fibration. If \mathcal {C} has conditionals, this Markov fibration is isomorphic to \mathcal {C}^\to .

Proof

Given a section s: X \to M:p and \phi : A \times _X M \to A \times _X A, simply take the pullback to the support of s. It must be the case that \phi (a,m) = (a,m) s-almost surely, which implies strict equality on the support. Hence by Proposition [efr-TBZZ], \mathcal {C}^\to presents a Markov fibration.

There is an induced map \mathsf {SChart}(\mathcal {C}^\to |_\mathrm {det}) \to \mathcal {C}^\to , which we claim is an isomorphism. So consider a map in \mathcal {C}^\to :

This map is in the image of
where the map \bar {X} \times Y \to \bar {Y} is taken to be a conditional. Note that every map in \mathsf {SChart}(\mathcal {C}^\to |_\mathrm {det}) can be represented in this form, by taking a conditional of M given Y to build a section to M \to X \otimes Y. Since conditionals are almost-surely equal, by restricting to the support of X \to X \otimes Y, we can find a representative which only depends on the overall map \bar {X} \to \bar {Y}, which proves that the map from \mathsf {SChart} is faithful, concluding the proof.

Continuing from Example [efr-CJTH], we have the following trivial case:

Proposition [efr-Z75A]

If \mathcal {C} is Cartesian (even if it does not admit pullbacks), the definition of Markov fibration over \mathcal {C} still makes sense, the Markov fibrations are exactly the Grothendieck fibrations, and their fiberwise opposites are simply their fiberwise opposites in the usual sense.

Proof

This is trivial because \mathsf {MarkPreFib}(\mathcal {C}) \to \mathsf {Fib}(\mathcal {C}_\mathrm {det} = \mathcal {C}) is simply the identity functor, hence it is monadic (with the identity monad,) hence every fibration/prefibration presents a Markov fibration, namely itself, and is in particular a Markov fibration. The fiberwise opposite is simply given by applying the identity (taking the stochastic module on the deterministic part), taking the fiberwise opposite, then applying the identity again (passing to the presented markov fibration).

It is worth noting that, even in the case where \mathsf {SChart}(\mathcal {D}_0^\mathrm {fop}) is not a prefibration, it may still deserve the name "stochastic lenses". For example the stochastic lenses in \mathsf {BorelStoch} can be seen to contain \mathsf {Optic}(\mathsf {BorelStoch}) as a full subcategory, even though it does not form a Markov fibration (see Theorem [efr-K6NM] below).

Part of the motivation for the theory of dependent optics is to identify a category of stochastic optics which admits all coproducts. If \mathcal {C} is distributive, \mathsf {Optic}(\mathcal {C}) satisfies \binom {A}{X} + \binom {A}{Y} = \binom {A}{X+Y}, but this coproduct fails to exist in general if the two secondary objects are distinct. The idea is that this coproduct \binom {A}{X} + \binom {A'}{Y} should exist as a family indexed by X + Y, where E_x = A for x \in X, and E_y = A' for y \in Y. Our theory accommodates this example under the mild additional hypothesis of extensiveness

Definition Extensive Markov Category [efr-B2P7]

A Markov category is said to be an extensive Markov category if it admits finite coproducts, whose injections are deterministic, and which satisfy the following equivalent conditions:

  1. If we let \mathcal {C}_{/a}^\mathrm {det} refer to the full subcategory of the slice spanned by the deterministic morphism x \to a, we have an equivalence of categories \mathcal {C}_{/a}^\mathrm {det} \times \mathcal {C}_{/b}^\mathrm {det} \cong \mathcal {C}_{/a + b}^\mathrm {det}, given by taking coproducts
  2. \mathcal {C}_\mathrm {det} is an extensive category in the usual sense and the inclusion \mathcal {C}_\mathrm {det} \to \mathcal {C} preserves pullbacks along coproduct inclusions.

More generally, for an infinite regular cardinal \kappa , we say that \mathcal {C} is \kappa -extensive if \mathcal {C}_\mathrm {det} is a \kappa -extensive category in the ordinary sense and both coproduct inclusions and pullbacks along them are preserved by the functor \mathcal {C}_\mathrm {det} \to \mathcal {C}.

Proposition [efr-QAV2]

Let \mathcal {C} be an extensive Markov category, let \mathcal {D}_0 \to \mathcal {C}_\mathrm {det} be a fibration which satisfies \mathcal {D}_{0,X+Y} = \mathcal {D}_{0,X} \times \mathcal {D}_{0,Y}. Note that this implies \mathcal {D}_0 admits finite coproducts, and they're given exactly by this pairing. Suppose \mathcal {D}_0 is equipped with a stochastic module structure. Then \mathcal {D}_0 \hookrightarrow \mathsf {SChart}(\mathcal {D}_0) preserves the finite coproducts. In particular, \mathcal {D}_0^\mathrm {fop} has the same coproducts as \mathcal {D}_0, and \mathcal {D}_0^\mathrm {fop} \to \mathsf {SLens}(\mathcal {D}_0) preserves them as well.

Proof

This is straightforward to check---the residual M \to X_1 + X_2 splits into M_1 + M_2 by extensivity of \mathcal {C}, which also implies the section must split as the copairing of a section s_1: X_1 \to M_1, s_2: X_2 \to M_2. By the condition on the fibration, the map in the fiber over M splits into a map over M_1 and a map over M_2. Using the extensivity again, it is straightforward to see that this decomposition respects the equivalence relation.

In particular, \mathsf {SChart}(\mathcal {C}^\to |_\mathrm {det}), \mathsf {SLens}(\mathcal {C}^\to |_\mathrm {det}) both admit coproducts given simply as coproducts in \mathcal {C}^\to , if \mathcal {C} is extensive.

Proposition [efr-XFAO]

Suppose \mathcal {D} is a Markov fibration so that each pullback functor f^*: \mathcal {D}_Y \to \mathcal {D}_X for f: X \to Y \in \mathcal {C}_\mathrm {det} can be taken to be bijective on objects, and that these can furthermore be chosen strictly functorial (so that (fg)^* = g^*f^*). Then, writing objects \bar {X} \in \mathcal {D}_X as \binom {A \in \mathcal {D}_*}{X \in \mathcal {C}}, where A is the unique object in \mathcal {D}_* which pulls back to \bar {X} under the deletion X \to *, (note that this means f^*\binom {A}{Y} = \binom {A}{X}) we may characterize the fiberwise dual as having hom-sets \mathcal {D}^{\mathrm {fop}}(\binom {A}{X},\binom {B}{Y}) = \mathcal {D}(\binom {B}{X},\binom {A}{Y})

Proof

The correspondence in both directions is obvious by just formally reversing the direction of the map f: \binom {A}{M} \to \binom {B}{M} in a representing tuple X \leftarrow M \to Y, a: X \to M, f---the fact that this assignment respects the equivalence relation follows from the fact that the monad preserves fiberwise opposites.