>>250
>Colin McLarty has looked into this
>The large structures of Grothendieck founded on finite order arithmetic, Review of Symbolic Logic 13 issue 2 (2020) pp. 296--325, doi:10.1017/S1755020319000340, arxiv.org/abs/1102.1773

これ、リンクのarxivは 2014年版だな
30 Apr 2014 COLIN MCLARTY
1. Outline
Finite order arithmetic (Takeuti, 1987, Part II), or simple type theory with infinity, is n-th order arithmetic for all finite n. It deals with numbers, sets of numbers, and sets of those, up through any fixed finite level. Sections 2– 3 develop basic cohomology in any one of several set theories equivalent to this.
Sections 4–5 give a weak notion of a universe U, and a simpler notion of Ucategory than Grothendieck’s (SGA 4 I.1.2), in a theory of classes and collections conservative over set theory. Section 6 proves standard theorems on toposes, derived categories, and fibered categories. This is the weakest possible level for Grothendieck’s tools since a single elementary topos of sets with infinity is already as strong as finite order arithmetic.
Section 7 relates this to proofs of Fermat’s Last Theorem.

つづく