Can `Squash.mk x = Squash.mk y` be made true by definition?

Stream: Type theory

[Eric Wieser]

Would lean's type theory survive a change which made

example : Squash.mk true = Squash.mk false := rfl

true?

[Eric Wieser]

Motivation: passing computationally relevent arguments in a way that is kernel-irrelevant

[Eric Wieser]

(we have docs#Erased for the other direction)

[Aaron Liu]

I think this makes defeq undecidable again

[Eric Wieser]

By again you mean "in yet another way" as opposed to "which we only just fixed"?

[Aaron Liu]

You get any two terms are defeq in an inconsistent context

[Aaron Liu]

Unless you drop more transitivity

[Aaron Liu]

For example, let t be your proof of False, and

true
  = id (fun _ => true) t
  = Squash.lift (Squash.mk fun _ => true) id t
  = Squash.lift (Squash.mk fun _ => false) id t
  = id (fun _ => false) t
  = false

[Aaron Liu]

Right now all of those are defeqs except for the line converting Squash.mk fun _ => true to Squash.mk fun _ => false

[Eric Wieser]

Thanks, I hate it

[Mario Carneiro]

You would need Squash.lift to be limited to DefeqSubsingleton B instead of Subsingleton B

[Mario Carneiro]

It would be pretty cool if that was a thing, but I think you start to end up with a variation on cubical TT if you take it to its logical conclusion

[Niels Voss]

Is DefeqSubsingleton an actual class, or is it some meta-theoretic property that applies to types like propositions and Unit, but not Unit -> Unit and Empty?

[Aaron Liu]

Unit → Unit looks like it would be a defeq subsingleton because it's a pi type whose codomain is a defeq subsingleton

[Mario Carneiro]

I was meaning DefeqSubsingleton is an actual class with the magic property that if you have two elements of it (even with a variable type) then the kernel knows that they are defeq

[Mario Carneiro]

Structures like Prod Unit Unit are also defeq subsingletons

[Eric Wieser]

Is Squash X a defeq subsingleton?

[Mario Carneiro]

it would be after this suggestion

[Niels Voss]

Ohh so you mean that the kernel would specifically look for DefeqSubsingleton instances and modify its behavior on account of them. I originally thought you meant we would have a typeclass for instances that were already DefeqSubsingletons according to the kernel

[Niels Voss]

If we get the ability to modify defeq behavior using the typeclass system, could we also make it so that propositionally equal but not definitionally equal diamonds now unify with each other?

[François G. Dorais]

Mario Carneiro said:

I was meaning DefeqSubsingleton is an actual class with the magic property that if you have two elements of it (even with a variable type) then the kernel knows that they are defeq

I've been wanting this magic for a long time. Do they teach Lean at Hogwarts? :grinning: