Simple Type Theory is not too Simple: Grothendieck's Schemes without Dependent Types

Anthony Bordg, Lawrence Paulson, Wenda Li

Church's simple type theory is often deemed too simple for elaborate mathematical constructions. In particular, doubts were raised whether schemes could be formalized in this setti…