My understanding is that Coq is based on (extensions to) Martin-Löf Type Theory while Isabelle/HOL is not (it is based on higher order logic instead). Voevodsky has said in his Unimath talk that he is using a subset of Coq in his UniMath library efforts, a subset that approximates the original MLTT.
Rest in peace, Dr. Voevodsky.
Have the slides been posted?
Prof. Voevodsky, why did you choose Coq instead of Isabelle/HOL as your main choice?
My understanding is that Coq is based on (extensions to) Martin-Löf Type Theory while Isabelle/HOL is not (it is based on higher order logic instead). Voevodsky has said in his Unimath talk that he is using a subset of Coq in his UniMath library efforts, a subset that approximates the original MLTT.
@@fbkintanar I agree with your line of thought.