Custom infi

Stream: general

[Yury G. Kudryashov]

In some cases (e.g., docs#uniform_space), it makes sense to have a custom infi function to ensure definitional equality for to_topological_space projection. I suggest that we add (may be, after the port) a protected definition uniform_space.infi (f : ι → uniform_space α) with to_topological_space := ⨅ i, (f i).to_topological_space and use it, e.g, for the pi instance.

[Eric Wieser]

Is this definitional equality to avoid diamonds, or just for convenience?

[Eric Wieser]

The problem with custom infis is that if expressed as a typeclass they need to be universe polymorphic

[Yury G. Kudryashov]

Not a TC, just a definition. The first use that comes to my mind is docs#Pi.uniform_space

[Eric Wieser]

I suppose if you did the TC route you could have

class has_infi (ι) (α) :=
(infi : (ι → α)→ α)
(Infi_eq_Inf (f) : Inf (range f) = infi f)

[Yury G. Kudryashov]

But we can't include this in complete_lattice, so we can't turn this into the "main" interface for infi.

[Yury G. Kudryashov]

And if it's not a part of complete_lattice, then any generic lemma about this TC infi will need lots of [has_infi _ _] instances.

[Eric Wieser]

Yury G. Kudryashov said:

Not a TC, just a definition. The first use that comes to my mind is docs#Pi.uniform_space

How would you deal with the uniform space over a double-indexed pi type?

[Eric Wieser]

Most infis are built out of other infis, aren't they? In which case, I think typeclasses are hard to avoid.

[Yury G. Kudryashov]

Probably, we shouldn't do this till we have more than 1 use for the new function.

[Anatole Dedecker]

Just to be sure, making sure that docs#uniform_space.has_Inf has nice definitional equality (which is not the case right now) wouldn’t help because of range having bad defeq, is that right ?

[Eric Wieser]

Would Inf ((λ u, 𝓤[u]) '' s) be better or worse than the current (⨅u∈s, 𝓤[u])?

[Yury G. Kudryashov]

It doesn't matter because the to_topological_space projection is not defeq

[Eric Wieser]

defeq to what?

[Yury G. Kudryashov]

To infi (λ i, (u i).to_topological_space)

[Eric Wieser]

Ah, so you want ⨅ i, (u i).to_topological_space = (⨅ i, u i).to_topological_space to be true definitionally

[Yury G. Kudryashov]

I wanted to define a custom function uniform_space.infi (no notation) with this property.

[Yury G. Kudryashov]

But I don't have good use cases except for the uniform_space structure on a pi type.