mathlib

mathlib copied to clipboard

We have a diamond of complete boolean algebras on sets:

import data.set.lattice

variables {α : Type*}

-- Succeeds
example : @set.boolean_algebra α = pi.boolean_algebra := rfl

-- Fails
example : @set.complete_boolean_algebra α = pi.complete_boolean_algebra := rfl

Although set is a type synonym, parts of our library abuse this and rely on the definitional equality between set α and α → Prop. A notable example is our measure theory library which currently relies on this definitional equality in order to share the concept of functions being "almost equal" with that of sets.

It would be desirable if we could resolve this diamond. See also Zulip thread