# Zulip Chat Archive

## Stream: maths

### Topic: Type expected error

#### Ashvni Narayanan (Feb 26 2021 at 12:12):

I am trying to define `dir_sys`

as the following : a collection of finite sets `(X_i)_{i ∈ ℕ}`

such that for `j ≤ i`

, there exists a surjective map `π_{ij}`

such that for `k ≤ j ≤ i`

, `π_{ij} ∘ π_{jk} = π_{ik}`

. I get stuck here:

```
import ring_theory.int.basic
import set_theory.zfc
structure dir_sys :=
( α : Type* )
(h : ℕ → finset α )
(sys : ∀ i j : ℕ, j ≤ i → ∃ f : (h i).1 → (h j).1, function.surjective f )
```

The error I get is :

```
type expected at
(h i).val
term has type
quot setoid.r
```

I don't understand the error. Does Lean want me to specify the type of `(h i).val`

? Any help is appreciated, thank you!

#### Eric Wieser (Feb 26 2021 at 12:15):

Adding an explicit `↥`

might help

#### Eric Wieser (Feb 26 2021 at 12:15):

`↥(h i).1 → ↥(h j).1`

or similar

#### Eric Wieser (Feb 26 2021 at 12:15):

Why the `.1`

which turns your finset into a multiset?

#### Ashvni Narayanan (Feb 26 2021 at 12:21):

Eric Wieser said:

Adding an explicit

`↥`

might help

I get the following error :

```
type expected at
↥(h i)
term has type
has_coe_to_sort.S (finset α)
```

#### Ashvni Narayanan (Feb 26 2021 at 12:21):

Eric Wieser said:

Why the

`.1`

which turns your finset into a multiset?

I was just experimenting..

#### Kevin Buzzard (Feb 26 2021 at 12:37):

My instinct is that we might already have some far more general kind of directed systems in mathlib already. I think that the functions themselves should be part of the data, not just some assumption that they exist. Might it be easier to work with types rather than finsets, which are terms?

#### Eric Wieser (Feb 26 2021 at 12:40):

We have docs#direct_limit which seems to have some things in common with what you're after

#### Eric Wieser (Feb 26 2021 at 12:42):

This works:

```
import data.finset.basic
structure dir_sys :=
( α : Type* )
(h : ℕ → finset α )
(sys : ∀ i j : ℕ, j ≤ i → ∃ f : (h i : set α) → (h j : set α), function.surjective f )
```

#### Eric Wieser (Feb 26 2021 at 12:42):

finset has no coercion to sort

#### Eric Wieser (Feb 26 2021 at 12:42):

Only coercion to set, which then has a coercion to sort

Last updated: May 18 2021 at 06:15 UTC