Definition Markov prefibration [efr-0019]

Let \mathcal {C} be a Markov category, and let p: \mathcal {D} \to \mathcal {C} be a functor into it. Then we call p a Markov prefibration if the following two conditions hold:

1. The pullback \mathcal {D} \times _\mathcal {C} \mathcal {C}_\mathrm {det} \to \mathcal {C}_\mathrm {det} is a (Grothendieck) fibration
2. Given maps f: A \to C, g:B \to C in \mathcal {D}, such that p(f),p(g) are deterministic and f,g are Cartesian for the above fibration, p induces a bijection between maps h: A \to B \in \mathcal {C} such that gh = f, and maps h': p(A) \to p(B) so that p(g)h' = p(f). Note that when restricted to those maps where p(h) is deterministic, this being a bijection is the defining property of g being Cartesian (for any f, not necessarily a Cartesian one).

Given a Markov prefibration \mathcal {D}, we write \mathcal {D}|_\mathrm {det} for \mathcal {D} \times _\mathcal {C} \mathcal {C}_\mathrm {det}. We will refer to this as the deterministic part of \mathcal {D}---note that this does have the potential for confusion, as when \mathcal {D} is itself a Markov category, this is not necessarily the same as the deterministic subcategory of \mathcal {D}. When f \in \mathcal {D} lies inside \mathcal {D}|_\mathrm {det}, and is Cartesian for that fibration, we will simply refer to it as a Cartesian map in \mathcal {D} (there are no other types of Cartesian maps, so this should not lead to confusion). A morphism of Markov prefibrations is a functor \mathcal {D} \to \mathcal {D}' over \mathcal {C} which preserves Cartesian maps. The category of Markov prefibrations over \mathcal {C} thus defined is denoted \mathsf {MarkPreFib}(\mathcal {C}). Taking the deterministic part defines a functor (-)|_\mathrm {det}: \mathsf {MarkPreFib}(\mathcal {C}) \to \mathsf {Fib}(\mathcal {C}_\mathrm {det}).