[FOM] proof assistants and foundations of mathematics

[José Manuel Rodriguez Caballero]

Joe Shipman said:
“It seems to me that no professional mathematician who is not working in logic and set theory, in his everyday work, uses anything that?s not formalizable in ?ZFC plus a proper class of Inaccessibles? (Grothendieck Universes) in well-established ways.”

I am not sure that VERY, as defined by Jean Benabou in elementary topos, can be formalized in ZFC.

Kind Regards,
Jose M.