Zulip Chat Archive

Stream: general

Topic: Proof irrelevance


view this post on Zulip Patrick Massot (Dec 13 2018 at 17:31):

Does anyone know whether https://hal.inria.fr/hal-01859964 is something Lean should care about? It's a paper about "Definitional Proof-Irrelevance without K" which explicitly mentions Lean's type theory.

view this post on Zulip Gabriel Ebner (Dec 13 2018 at 18:27):

Their typesetting ate the → symbols. :sad: Maybe I'm missing something, but the results are not very exciting to me. In summary, they add a universe sProp u of squashed types, whose elements are then made definitionally equal. They don't have any good ideas for the problems with acc that make type-checking undecidable in Lean. They just disallow subsingleton elimination completely, so you can't even cast along equations...

view this post on Zulip Mario Carneiro (Dec 13 2018 at 18:42):

only some of them... the Agda code also has some missing → symbols, but also some visible ones

view this post on Zulip Gabriel Ebner (Dec 13 2018 at 18:42):

(By exciting I mean exciting for math/programming in Lean. The idea of using squash types with definitional equality could be nice in HoTT (I guess we could even squash in Lean by going into Prop).)

view this post on Zulip Mario Carneiro (Dec 13 2018 at 18:42):

also the lambdas

view this post on Zulip Mario Carneiro (Dec 13 2018 at 18:43):

what is the intuition behind these squash types?

view this post on Zulip Mario Carneiro (Dec 13 2018 at 18:43):

are they like HoTT propositions or lean propositions?

view this post on Zulip Gabriel Ebner (Dec 13 2018 at 18:45):

They're essentially just quotients with the universal relation + definitional equality. The rules are on page 10. Edit: no they're even less---you can't eliminate into Type at all from squash types.

view this post on Zulip Mario Carneiro (Dec 13 2018 at 19:05):

I think the moral of the story is that everything you can do with sType is already possible in lean, this paper just describes how


Last updated: May 14 2021 at 12:18 UTC