Higher computational properties of computational identity types

[fredrik-bakke]

• Refactors ap-binary to compute as one of the sides in the gray interchange diagram.
• Adds whiskering and horizontal concatenation of Yoneda identifications
• Renames inv-(yoneda|involutive|computational)-Id to inv(ʸ|ⁱ|ʲ)
• Some touch-ups for the file on the Eckmann-Hilton argument

[fredrik-bakke]

So, turns out it's possible to make horizontal concatenation for any identity type one-sided strictly unital, but I don't know if this is desirable.

[fredrik-bakke]

I don't feel particularly inspired to continue working on this atm, so I'm just going to mark it as ready for review.

[fredrik-bakke]

Apologies, I forgot to mark this PR ready for review. Would it be possible to get it merged before 13:00 on Monday? I'd like to use the webpage for my supervisor meeting.