[draft] Add draft definition of a double category

[Boarders]

Opening this pull request to get style advice / denunciations for aesthetic crimes.

Still to do:

• Defining the underlying vertical and horizontal 2-categories

[Boarders]

It looks like these unicode characters are variable width in different fonts so I might have to re-think the diagrams (which I do think are valuable once you have higher dimensions happening).

[JacquesCarette]

@maxsnew can you give this another look?

[maxsnew]

I'm on vacation so I won't be able to look for about a week and a half

On Mon, May 2, 2022, 4:20 PM Jacques Carette @.***> wrote:

@maxsnew https://github.com/maxsnew can you give this another look?

— Reply to this email directly, view it on GitHub https://github.com/agda/agda-categories/pull/346#issuecomment-1115552045, or unsubscribe https://github.com/notifications/unsubscribe-auth/AALJIPI2OBT2UBKW7HQ4VPTVICEQTANCNFSM5TRHGBAA . You are receiving this because you were mentioned.Message ID: @.***>

[Boarders]

@JacquesCarette Thanks for the review, I'll make these changes shortly.

[Boarders]

@JacquesCarette Apologies for the huge delay, life got in the way. I have made the changes you suggested and updated the name to FrameEquality. Let me know if there are more style changes you would like and I'll be happy to get this over the line.

[JacquesCarette]

No worries. My life is quite eventful in all of July, this may end up waiting until early August. Though I will try next week, we'll see.