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.