[FOM] Foundational Challenge

[Gabbay, Murdoch]

> >   "Equivariant ZFA and the foundations of nominal techniques"
> > https://arxiv.org/abs/1801.09443)

> 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?

Thanks for the questions.

I can't comment on univalence and proof size.  Perhaps somebody else on FOM could elaborate?  Also to my knowledge, no direct mathematical analogy has been drawn between equivariance and univalence.

However, something has been said on this topic by Andrew Pitts in "Nominal Presentation of Cubical Sets Models of Type Theory"
https://drops.dagstuhl.de/opus/volltexte/2015/5498/
The connection, from my EZFAC paper to univalence via Pitts' paper, goes like this:

Equivariance (which EZFAC hosts quadratically better than ZFC) is prototypical for a bundle of techniques and models which are collectively called "nominal techniques".

Nominal techniques have rich structure, including a notion of a "set with a monoid of substitutions" --- I'd like to honour Martin Hofmann with a mention of his paper<https://link.springer.com/chapter/10.1007/978-3-540-89439-1_11> with me on this topic.  Pitts used sets with a nominal monoid of substitutions give a presentation of cubical sets, which as you may know model univalence<https://link.springer.com/article/10.1007/s10817-018-9472-6>.

In brief: equivariance -> nominal techniques -> nominal monoid of substitutions -> model of cubical sets -> univalence.

Jamie Gabbay
________________________________

Heriot-Watt University is The Times & The Sunday Times International University of the Year 2018

Founded in 1821, Heriot-Watt is a leader in ideas and solutions. With campuses and students across the entire globe we span the world, delivering innovation and educational excellence in business, engineering, design and the physical, social and life sciences. This email is generated from the Heriot-Watt University Group, which includes:

  1.  Heriot-Watt University, a Scottish charity registered under number SC000278
  2.  Heriot- Watt Services Limited (Oriam), Scotland's national performance centre for sport. Heriot-Watt Services Limited is a private limited company registered is Scotland with registered number SC271030 and registered office at Research & Enterprise Services Heriot-Watt University, Riccarton, Edinburgh, EH14 4AS.

The contents (including any attachments) are confidential. If you are not the intended recipient of this e-mail, any disclosure, copying, distribution or use of its contents is strictly prohibited, and you should please notify the sender immediately and then delete it (including any attachments) from your system.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20200117/47d16717/attachment-0001.html>