# Zulip Chat Archive

## Stream: new members

### Topic: finset <-> boolean algebra, universes

#### Eric Meinhardt (Jan 11 2022 at 22:48):

I'd like to associate every finite set (over a finite type with decidable equality) with its boolean algebra, i.e. make use of https://github.com/leanprover-community/mathlib/blob/40b6b45c052e188122ec9a25e8aedf00232e4633/src/data/fintype/basic.lean#L125

My reading of the typeclass instance there is that for every α s.t. `fintype α`

and `decidable_eq α`

, every `s : finset α`

has a boolean algebra instance associated with it. How do I actually make use of this to associate any particular `s : finset α`

with its boolean algebra instance?

```
-- typechecks
def foo {α : Type _} [fintype α] [decidable_eq α] : boolean_algebra (finset α) :=
finset.boolean_algebra
-- tweak of foo whose explicit type is what I think I want
def bar {α : Type _} [fintype α] [decidable_eq α] (h : finset α) : boolean_algebra h :=
finset.boolean_algebra
```

results in the following error on the body of `bar`

:

```
type mismatch, term
finset.boolean_algebra
has type
boolean_algebra (finset ?m_1) : Type ?
but is expected to have type
boolean_algebra ↥h : Type ?
```

My current guess as to the meaning of the error is something related to universes?

#### Henrik Böving (Jan 11 2022 at 23:20):

I'd say that the precise thing you are asking for here is not possible, you want to return an instance of a typeclass on a specific term of a type but that is not possible, the boolean_algebra typeclass can only be implemented by types themselves. That is, the mathlib boolean algebras are (to my understanding of the types, I don't actually have a clue of the mathematics involved here) not defined over a concrete carrier set of values but rather over an entire type.

#### Eric Wieser (Jan 11 2022 at 23:28):

When you say `boolean_algebra h`

lean is translating it to `boolean_algebra (coe_sort h)`

, which is what that funny arrow means

#### Eric Wieser (Jan 11 2022 at 23:29):

docs#finset.has_coe_to_sort implements that arrow as "the type of elements contained in `h`

"

#### Alex J. Best (Jan 11 2022 at 23:29):

I don't think your reading of the instance is correct. docs#finset.boolean algebra says that given a finite type `\alpha`

the type of all possible finite subsets has the structure of a boolean algebra, that is there is an algebra structure where the sup of two finite subsets is their union, etc. Each `s : finset \alpha`

doesn't have its own boolean algebra structure, there is just a way to sup finsets.

#### Alex J. Best (Jan 11 2022 at 23:30):

If you say a bit more about what you want to use this for then we can try and see how to phrase this in Lean

Last updated: Dec 20 2023 at 11:08 UTC