The question still stands because agda handles classical mathematics just fine too. You need to postulate lem, which blocks computation, but that is a non-issue

The question still stands because agda handles classical mathematics just fine too. You need to postulate lem, which blocks computation, but that is a non-issue for proof checking.