The Independence of Markov's Principle in Type Theory

Thierry Coquand, Bassel Mannaa

In this paper, we show that Markov's principle is not derivable in dependent type theory with natural numbers and one universe. One way to prove this would be to remark that Markov…