[FOM] Upper bounds on what is needed to prove FLT

[Andrej Bauer]

In a recent discussion Martin Davis mentioned that it is not precisely
known how much of heavy category-theoretic artilery is needed to prove
Fermat's Last Theorem. I know we discussed this before, but can
someone knowledgable in these matters comment on upper bounds?

Which part of the known proof (seemingly) requires strong assumptions?
For example, would it be enough to assume Grothendieck's universes?
How many? What would that correspond to in set-theoretic terms?

With kind regards,

Andrej Bauer