Behavior of ap(f) on concatenations and inverses

[kristinas]

Namely, the identities

ap(f,p@q) = ap(f,p)@ap(q)
ap(f,!p) = !ap(f,p)

Is this stated somewhere? I would expect to find it in the chapter "Functions are functors" but I can't seem to locate it. It is used very often so it should probably be a separate lemma.

Kristina

[andrejbauer]

It would be nice to have a table of common equations, with references to places in the book.

[mikeshulman]

That would be an improvement on the current section 2.3. Maybe put the
table at the end of chapter 2? Or the end of the whole book?

Regarding the original question, it doesn't seem to be there. We should
add it.

On Fri, Mar 8, 2013 at 3:58 PM, Andrej Bauer notifications@github.comwrote:

It would be nice to have a table of common equations, with references to
places in the book.

—
Reply to this email directly or view it on GitHubhttps://github.com//issues/9#issuecomment-14645129
.

[mikeshulman]

I've added the original equations as Lemma 2.2.2.