The Coq mailing list

[Bob Atkey <bob.atkey AT gmail.com>]

On 25/06/2020 14:57, Pierre-Marie Pédrot wrote:

> Accepting funext unconditionally breaks most of the models I design for
> a living. A lot of people have been working in a theory without funext
> without fuss, it would be sad to prevent them from using whatever
> logical principles these models implement.

Another example of how life can be fun without funext is the 
interpretation of type theory in containers / polynomial functors. This 
has Pi-types with eta, but refutes funext. I believe this observation is 
due to Tamara von Glehn in her Phd thesis [1]. I made a little 
formalisation of the model in Agda [2] and formally proved that funext 
is refuted.

[1] https://www.repository.cam.ac.uk/handle/1810/254394

[2] https://gist.github.com/bobatkey/0d1f04057939905d35699f1b1c323736


Bob