As an author of this paper, I think I would write it a little bit differently if I had the chance today. Before I begin, let me echo Andrej's comment that Nuprl is a very significant moment in the history of type theory and even constructive mathematics, and none of what I say (then or now) is meant to detract from that. I obviously have immense respect for Nuprl and the people who built it, who were in many ways pioneers in type theory and in interactive proof assistants. Much of what we have today (like Coq and Agda) owes its present shape to the ideas developed by the PRL Group.
To me the difficulty with relating Nuprl to mathematics is basically one of methodology. As Andrej says, Nuprl's Computational Type Theory is based on "truth in one model"; as a result, there are many things that are true in this specific model that are false in the category of sets, false in many categories of presheaves, and false in many categories of sheaves. This is not the fault of (e.g.) realizability semantics, but rather the fault of confounding syntax and semantics. Both are important, but semantics benefits from multiplicity --- and the multiplicity of semantics is embodied in syntax. We can therefore expect strange results if we say that syntax is just a way to speak about one single example of semantics.
So my aim is not to say "realizability is bad" --- realizability is clearly very good. But I think it is bad on balance to base a proof assistant on one single model (bad in ways that COULD NOT have been anticipated [clarification: by that community] in the early 1980s when this was going on!) because it limits the applicability of your results.
Because Nuprl incorporates axioms that are not true in ordinary math, nor in the relative ordinary math of topoi, we cannot take a Nuprl proof about groups and use it as evidence to a "proper mathematician" for the truth of that statement about groups in a way that applies to that mathematician's work. This limits the ability to communicate and re-use results, but that is to me the entire point of mathematics.
I want to end by saying that my perspective on mathematics is not the only one. Nuprl is much inspired by the ideas of L.E.J. Brouwer who took a very different viewpoint --- a proof in Brouwer's style about groups also does not necessarily lead to evidence that a mathematician would accept for the truth of that statement about groups. But Brouwer's perspective was that all the mathematicians were wrong, and that only he was right. If that was actually so, then one could not blame him for doing his proofs in a way that was not backward compatible.
Therefore, the question that Nuprl raises is nothing less than: is mainstream mathematics wrong? Back when I was building tools based on Nuprl, I believed that normal mathematics was wrong. I no longer believe that though.
Lastly, I want to say that the above applies to Nuprl when viewed as a general-purpose language for mathematics --- for the reasons I describe, it cannot be a general-purpose language in that sense. But this is not the only thing Nuprl has been: Nuprl has also been a "synthetic domain theory" (an implementation of the slogan "domains are just types, don't worry about continuity" --- albeit quite different from the one pursued by the category theorists). Nuprl's synthetic domain theory aimed to let you reason about programs that use partial functions in ways that don't terminate, like LCF. One can argue today whether their approach was the best or not, but I think this is a very interesting aspect of Nuprl that is less well known than it should be. Nuprl qua synthetic domain theory doesn't claim to be general purpose, only useful for a specific purpose. So I think that's a good way to think about Nuprl that respects the great accomplishments of that team.
Bsuch that every type
Ais a subquotient of
B." (It may take some care to state this properly though.) $\endgroup$