## Stream: general

### Topic: Proof irrelevance

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

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

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

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

also the lambdas

#### Mario Carneiro (Dec 13 2018 at 18:43):

what is the intuition behind these squash types?

#### Mario Carneiro (Dec 13 2018 at 18:43):

are they like HoTT propositions or lean propositions?

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

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