Zulip Chat Archive

Stream: new members

Topic: Heterogenous/Dependent Equality

Johan Commelin (Jun 14 2020 at 08:12):

Reed Mullanix said:

Also, what is the general take on heterogenous equality?

I think: try to avoid it as much as possible.

Johan Commelin (Jun 14 2020 at 08:13):

What we typically do in mathlib is to move the carrier type (A : C) out of the structure fields, and into the hypotheses.

Johan Commelin (Jun 14 2020 at 08:14):

Once you do that, writing ext is no longer a problem.

Johan Commelin (Jun 14 2020 at 08:16):

Of course, this doesn't work if you are trying to build the underlying type for the category of algebras over a monad...

Johan Commelin (Jun 14 2020 at 08:16):

But in that case, you should use isomorphisms in the category, instead of equality.

Reed Mullanix (Jun 14 2020 at 08:17):

I think: try to avoid it as much as possible.

I've definitely been burned by it in other systems, so this makes sense

And yeah, I was just going to bring that up. The result I was working on only works for strict equality as far as I know (uniqueness of the comparison functor for Eilenberg-Moore)

Johan Commelin (Jun 14 2020 at 08:19):

Ok, I don't know the details of the maths there

Johan Commelin (Jun 14 2020 at 08:19):

@Scott Morrison Do you know what to do here?

Scott Morrison (Jun 14 2020 at 08:20):

You might look at src#functor.ext and src#functor.hext

Scott Morrison (Jun 14 2020 at 08:20):

Bah, wrong links.

Reed Mullanix (Jun 14 2020 at 08:23):

Yeah, I saw something similar done with https://github.com/leanprover-community/mathlib/blob/c8c18697d4019608b756edf7989290303a96071a/src/category_theory/eq_to_hom.lean#L47

Scott Morrison (Jun 14 2020 at 08:25):

Yes, those two variants were what I was trying to link to!

Scott Morrison (Jun 14 2020 at 08:25):

eq_to_hom seems like a pretty good solution most of the time.

Scott Morrison (Jun 14 2020 at 08:26):

They seem to successfully dissolve out of the way under simp in the actual goals you see.

Scott Morrison (Jun 14 2020 at 08:27):

I don't know what it is you're trying to prove, but I'll be surprised if it's intrinsically "evil".

Last updated: Dec 20 2023 at 11:08 UTC