[FOM] Structural set theory for proof assistants

[Timothy Y. Chow]

Josh Chen wrote:

> Have structural set theories been considered as foundations for formal 
> *computer* mathematics before? Maybe some people who know the details of 
> these foundations, and have perhaps tried to work out some mathematics 
> in them, could comment on the prospects of such an undertaking? Even the 
> more recent developments in set-theoretic systems seem to mostly use 
> ZF(C), and I would like to know if this is a historical/cultural 
> accident, or if there is some deeper obstruction.

I don't keep up with all the latest developments, but I have not heard of 
anyone specifically using ETCS (or something like it) as the basis for a 
proof assistant.  But if indeed it hasn't been done, I doubt that there is 
any deep obstruction.  In fact, since ETCS has both type-theoretic and 
set-theoretic aspects, perhaps it can take advantage of the best of both 
worlds.  See also:

https://mathoverflow.net/a/118248
http://aitp-conference.org/2018/slides/JH.pdf

Tim