Proof irrelevance

Stream: general

[Patrick Massot]

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.

[Gabriel Ebner]

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

[Mario Carneiro]

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

[Gabriel Ebner]

(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).)

[Mario Carneiro]

also the lambdas

[Mario Carneiro]

what is the intuition behind these squash types?

[Mario Carneiro]

are they like HoTT propositions or lean propositions?

[Gabriel Ebner]

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.

[Mario Carneiro]

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