The Coq mailing list

[Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk>]

Yes this is an interesting observation. Containers give rise to a model of 
type theory with beta-eta but without funext. 

It is interesting that container are a subset of a large presheaf category 
but Tamara’s interpretation doesn’t use the presheaf exponential but actually 
exploits that the category of containers is Cartesian closed. But not an 
lcccc. I’d like to understand this better.

To soften my previous remark: yes it can be fun to play games to understand 
the system better. But we shouldn’t design type theory with the whole intent 
of playing games.

Sent from my iPhone

> On 25 Jun 2020, at 15:11, Bob Atkey <bob.atkey AT gmail.com> wrote:
> 
> 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
> 



This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.