# Zulip Chat Archive

## Stream: general

### Topic: decidable heq

#### Eric Rodriguez (Jun 09 2021 at 19:05):

I know the answer is probably "don't do these cursed things", but I want to get `decidable_eq`

instance for `quiver.total`

and am really struggling:

```
import combinatorics.quiver
universes v u
instance {V : Type u} [quiver.{v} V] [decidable_eq V] : decidable_eq (quiver.total V) :=
begin
intros a b,
apply decidable_of_decidable_of_iff _ (quiver.total.ext_iff a b).symm,
haveI : decidable (a.hom == b.hom) := sorry,
apply_instance
end
```

now, the very big issue is how in the hell I decide equality of `heq`

. I know I certainly need more `decidable`

instances, but not sure which or how to string them together. The reason I want decidability here is because there's going to be parts where I'm hoping `dec_trivial`

can do the book-keeping and not me.

#### Eric Wieser (Jun 09 2021 at 19:17):

docs#quiver.total for reference

#### Kevin Buzzard (Jun 09 2021 at 19:18):

I doubt this is provable unless you also have decidable equality on all the hom sets. Let's say a.left = b.left and a.right = b.right. Then you want to decide equality of two terms of type `a.left ⟶ a.right`

.

#### Eric Wieser (Jun 09 2021 at 19:19):

Yeah, I think you need ` [Π a b : V, decidable_eq (a ⟶ b)]`

(edit: or something dependent but weaker)

#### Kevin Buzzard (Jun 09 2021 at 19:20):

For example (I should say that I have no idea what a quiver is so please check what I'm saying) if V = just `unit`

but `Hom(star,star)`

is the real numbers, V has decidable equality but I doubt `quiver.total V`

does.

#### Eric Rodriguez (Jun 09 2021 at 19:25):

No, for sure I think I need more instances. But not sure which and then how to proceed with it

#### Eric Wieser (Jun 09 2021 at 19:27):

Does `derive decidable_eq`

work?

#### Eric Wieser (Jun 09 2021 at 19:28):

Worst case scenario you show it's equivalent to a sigma type, and then instances should kick in

#### Eric Wieser (Jun 09 2021 at 19:28):

But the derive_handler ought to do that for you

#### Eric Rodriguez (Jun 09 2021 at 19:32):

Eric Wieser said:

Does

`derive decidable_eq`

work?

putting that on `quiver.total`

wants the instance that you thought it'd need, but I'm not sure how to tell `derive`

"just assume it"

#### Eric Rodriguez (Jun 09 2021 at 19:32):

and if I try to use `tactic.mk_dec_eq_instance`

directly it gives me a `match failed`

error

#### Eric Rodriguez (Jun 09 2021 at 19:35):

aha! this works but probably isn't optimal

```
instance [quiver.{v} V] [decidable_eq V] [Π a b : V, decidable_eq (a ⟶ b)] : decidable_eq (quiver.total V) :=
by tactic.mk_dec_eq_instance
```

#### Kevin Buzzard (Jun 09 2021 at 20:09):

Oh nice! You used black magic!

#### Eric Wieser (Jun 09 2021 at 20:31):

Looks optimal to me

Last updated: Dec 20 2023 at 11:08 UTC