Strength of Nonempty α → Squash α

Stream: maths

[Daniel Weber]

What are the consequences of Nonempty α → Squash α as an axiom, compared to choice (Nonempty α → α)? I can see it's equivalent to choice for subsingletons (Nonempty α → Subsingleton α → α). Is it a well known axiom?

[Kevin Buzzard]

docs#Squash

[Kevin Buzzard]

Ooh, this was trunc in lean 3 IIRC

[Daniel Weber]

Huh, there's still docs#Trunc

[Floris van Doorn]

This is an axiom knows as "unique choice". It is a much safer version of choice. Mathematically, it is nicer, since you cannot use it to define "unknowable objects," e.g. a natural number for which it is impossible (even in principle) to know whether it is 0 or not. From a type-theoretic view, there are variants of type theory where (a version of) unique choice is provable (e.g. HoTT) or even computable (e.g. cubical type theory).

[Daniel Weber]

Interesting. Thanks

[Kevin Buzzard]

I've also heard the claim that this function is available in ZF set theory with no extra axioms (and this sounds reasonable, because this is kind of the definition of a function in ZF set theory)

[Patrick Massot]

The duplication Squash vs Truc is probably a porting accident that should be fixed by deleting the Mathlib version (probably keeping lemmas that are not in Core).

[Kim Morrison]

Would someone be able to delete Trunc?

[Daniel Weber]

Kim Morrison said:

Would someone be able to delete Trunc?

I'm working on it on #14619, but it's used in quite a few places

[Daniel Weber]

Is there any reason for docs#CategoryTheory.Groupoid.ofTruncSplitMono to use Trunc? docs#CategoryTheory.IsSplitMono is a Prop... Is it supposed to be docs#SplitMono ?

[Kim Morrison]

@Daniel Weber, I'm pretty sure this is an incomplete refactor, and we can remove the Trunc here.

[Daniel Weber]

There's also a problem with docs#Fintype.truncRecEmptyOption, which presumably we want for Sorts but docs#Squash is defined only for Types. Is there any possible problem with making Squash take Sort instead of Type?

[Eric Wieser]

Daniel Weber said:

There's also a problem with docs#Fintype.truncRecEmptyOption, which presumably we want for Sorts

Option and Fintype don't exist for Sort*, so I doubt we want this

[Eric Wieser]

It does seem possibly problematic that docs#Trunc takes Sort u and docs#Squash takes Type u though

[Daniel Weber]

Eric Wieser said:

Daniel Weber said:

There's also a problem with docs#Fintype.truncRecEmptyOption, which presumably we want for Sorts

Option and Fintype don't exist for Sort*, so I doubt we want this

What? Currently P : Type u → Sort v, and it returns Trunc (P α), which is Sort v. Option is only used in P (Option α), where it's a Type u.

[Daniel Weber]

In fact docs#Fintype.induction_empty_option uses it with P : Type u → Prop

[Eric Wieser]

Apologies, I misread the types there, you're right indeed.

[Violeta Hernández]

What's the significance of Trunc p for p : Prop? Isn't this just another Prop equivalent to it?

[Daniel Weber]

It is, but it can be used on a Sort*

[Violeta Hernández]

Oh, I see

[Violeta Hernández]

Would it make sense to do a core PR generalizing Squash to Sort*?

[Daniel Weber]

Have you had a chance to do that? I'm attempting to do this again, but this time I'll just deprecate it and disable the linter in places I don't manage to fix

[Violeta Hernández]

Well, my message was meant as somewhat of a hypothetical. But sure, I can take it up.

[Violeta Hernández]

Huh, just changing Type into Sort seems to not break anything

[Violeta Hernández]

lean4#6074

[Violeta Hernández]

So, surely we can just drop and replace Squash into Mathlib, right?

[Violeta Hernández]

We can even redefine Trunc to be def-eq to it before deprecating it

[Daniel Weber]

It is defeq already

[Daniel Weber]

Feel free to take over #18952 (which deprecates Trunc to Squash), I haven't had time to work on it

[Violeta Hernández]

I'm running into a weird issue with docs#Trunc.finChoice. The definition works just fine as is, but if I replace Trunc by Squash it breaks despite the def-eq. What's going on?

[Violeta Hernández]

I think the issue is that Squash α is defined in terms of Quot rather than Quotient, and so the setoid argument can't be inferred

[Violeta Hernández]

That seems a bit silly, given that Squash is actually defined after Quotient in Init.Core

[Violeta Hernández]

Opened lean4#6642 which should take care of that