Zulip Chat Archive

Stream: Is there code for X?

Topic: Powers of a relation?


view this post on Zulip Scott Morrison (Apr 07 2021 at 01:52):

Do we have "integer powers of a relation"? e.g. if r : ι → ι → Prop, I would like the relations that say things like: there is a length k chain r i0 i1, r i1 i2 ... r _ r ik. (Ideally for both positive and negative lengths, interpreting negative lengths by reversing the relation.)

view this post on Zulip Mario Carneiro (Apr 07 2021 at 01:54):

There is list.chain

view this post on Zulip Mario Carneiro (Apr 07 2021 at 01:54):

you could existentially quantify over the chain to get this

view this post on Zulip Scott Morrison (Apr 07 2021 at 01:55):

hmm... seems maybe easier to define it by induction. The fact that I want negative lengths makes it pretty messy, however.

view this post on Zulip Mario Carneiro (Apr 07 2021 at 01:55):

Oh I missed the negative thing

view this post on Zulip Mario Carneiro (Apr 07 2021 at 01:55):

yeah you are on your own for that

view this post on Zulip Mario Carneiro (Apr 07 2021 at 01:56):

Or you could use ^[k] to apply the function comp R to eq

view this post on Zulip Scott Morrison (Apr 07 2021 at 01:57):

I guess it will be cleanest if I do the nat case first, and then just tack on negative lengths as an outside layer.


Last updated: May 16 2021 at 05:21 UTC