[FOM] Foundational Challenge

[Timothy Y. Chow]

Murdoch Gabbay wrote:

>   "Equivariant ZFA and the foundations of nominal techniques"
> (to appear in the Journal of Logic and Computation; available online at 
> https://arxiv.org/abs/1801.09443)
> I describe an alternative sets foundation EZFAC on ground similar to 
> item (b) above.
>
> EZFAC is very close to ZFC and easily proved equivalent to it.

This is very interesting!

I wonder if you can comment on the analogy between your (Equivar) axiom 
and the univalence axiom in univalent foundations?  Superficially, they 
seem somewhat similar.  For example, does the univalence axiom reduce 
quadratic blowups in much the same way that (Equivar) does?

Tim