## Stream: Is there code for X?

### Topic: Powers of a relation?

#### 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.)

#### Mario Carneiro (Apr 07 2021 at 01:54):

There is list.chain

#### Mario Carneiro (Apr 07 2021 at 01:54):

you could existentially quantify over the chain to get this

#### 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.

#### Mario Carneiro (Apr 07 2021 at 01:55):

Oh I missed the negative thing

#### Mario Carneiro (Apr 07 2021 at 01:55):

yeah you are on your own for that

#### Mario Carneiro (Apr 07 2021 at 01:56):

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

#### 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