Ah okay, I think I understand, if I'm remembering my type theory correctly. I think this is downstream of "standard type theory" i.e. type theory created by Löf not accepting the excluded middle? Which does also mean rejecting choice, for sure. 

EDIT: But fwiw, I think the excluded middle is much less controversial than Choice (it should technically be strictly less controversial). I think that may be a less interesting post, but I'm sure philosophers have already written that. Though I think a post defending rejecting the excluded middle from a type theory perspective actually could be quite good, because lots of people don't seem to understand the arguments from the other side here, and think they're just being ridiculous.

I think I basically agree that this is how one should consider this.

But I think there is a reasonable defence of the "ZF-universe as somewhat transcendent entities" and that is that we do virtually all of our actual maths in ZF-universes, by saying that ultimately we will be able to appeal to ZF-axioms. This makes ZF-objects pretty different from groups. E.g. I think there's a pretty tight analogy between forcing in ZF and galois extensions (just forcing is much more complicated), but the consequences of forcing for how we do the rest of maths can be somewhat deep (e.g. CH is doomed in ZFC, consequences about Turing computability, etc). So the mystical reputation is somewhat deserved. Woodin would defend some much more complicated and involved version of this as I discussed in my post about the constructible universe.

But I agree ultimately, with our current understanding of ZF-universes that they are just another mathematical object, they just happen to be an object that we use to do other maths with, and we can step outside those objects these days with large cardinal axioms, if we'd like, and analyze other consequences of them. It's pretty similar to how we started viewing logic and logics after Gödel's results (i.e. clearly first-order logic is very useful because of compactness/completeness, but that doesn't mean "Second order logic is wrong.") 

Ah I really need to write a megasequence about the large cardinal axioms! They're awesome (I wrote a thesis on them).

If you're talking about surreals or hyperreals, the issue is basically that there's not one canonical model of infinitesimals, you can create them in many different ways. I'll hopefully end up writing more about the surreals and hyperreals at some point, but they don't solve as many issues as you'd hope unfortunately, and actually introduce some other problems.

As a motivating idea here, note that you need the Boolean Prime Ideal Theorem (which requires a weak form of choice to prove) to show that the hyperreals even exist in the first place, if you're starting from the natural numbers as "mathematically/ontologically basic." (maybe there's another way to define them but none immediately come to mind, there is another way to define the surreals, but there are other issues there).

Yes sorry to be clear I’m not talking about whether it is true, I am talking about whether they would use it or not in proving ‘standard’ results.

Oh, yeah sure. I mean I think as a matter of pragmatics it mostly is an exercise in foundations these days. But I agree that splitting up concepts of finitude -- for example -- is a super interesting investigation. Just, like, the majority of algebraic geometers, functional analysts, algebraic topologists, analytic number theorists, algebraic number theorists, galois theorists, representation theorists, differential geometers, etc etc etc, would not be all that interested in such an investigation these days.

Sorry, I think explaining without using type theory what you are trying to say may help me understand better?

EDIT: like, in particular, insofar as its relevant to the axiom of choice.

I think among working mathematicians it is that much of a minority. E.g. it is much less controversial than something like many-worlds among physicists, or something like heritability of intelligence among geneticists. It is broadly incredibly accepted.

EDIT: But I do agree it's a respected alternative view, and I do think it should stay that way because it is interesting to investigate. I just think people get the wrong idea about its degree of controversy among working mathematicians.

I think I must've not paid enough attention in type theory class to get this? Is this an excluded middle thing? (if it's a joke that I'm ruining by asking this feel free to let me know)

Well put! I guess if I can define a function from problems to math-to-model-it, then for every problem I can pick out the right math-to-model-it?

 Or, indeed, perhaps not? ;)