I’ve been playing with this proof which I already found quite neat in pure Coq and adapting it to HoTT using truncation instead of double negation. In two words, it works! HoTT_Markov (source, requires the HoTT library).