Powers of a relation?

Stream: Is there code for X?

[Scott Morrison]

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]

There is list.chain

[Mario Carneiro]

you could existentially quantify over the chain to get this

[Scott Morrison]

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

[Mario Carneiro]

Oh I missed the negative thing

[Mario Carneiro]

yeah you are on your own for that

[Mario Carneiro]

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

[Scott Morrison]

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