FOM: Functorial Constructions and Wiles's proof

[Joe Shipman]

McLarty says that the reason the Universes can be eliminated from
Wiles's proof is that all the derived functor cohomology and similar
constructions in it can be done in a more cumbersome way using
explicitly defined functorial relations.  But in the absence of a
metatheorem, this still needs to at least be verified and remarked
upon.  In the same way that arguments in logic papers regularly take the
form

1) <Proof of X>
2) Observation that the proof in 1) only used Y and not Z
3) Application of metatheorem to conclude something stronger or more
general than X,

Wiles and his colleagues owe us at least a statement that "reflecting on
the proof confirms that all functorial constructions used were
explicitly definable and so the conclusion does not depend on the
Universes assumption".  We should insist on at least this much lip
service to proper foundations.

-- Joe Shipman