<div dir="ltr"><div><div>Markov axiom (for Nat) doesn't leed to a total excluded third.<br>Constructive logic together with Markov axiom (for Nat) is still constructive.<br></div>Here is really nice <a href="http://scs.hosted.panopto.com/Panopto/Pages/Sessions/List.aspx#folderID=%2207756bb0-b872-4a4a-95b1-b77ad206dab3%22">course</a> (and <a href="http://homotopytypetheory.org/book/">book</a>) explaining in very deep details all that stuff with constructive vs classic vs whatever.<br>
<br></div>Dmytro <br></div>