search

agda / agda-categories

A new Categories library for Agda
https://agda.github.io/agda-categories
MIT License
362 stars 68 forks source link

[draft] Add draft definition of a double category #346

Closed Boarders closed 1 year ago

Boarders commented 2 years ago

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

Still to do:

Boarders commented 2 years ago

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 commented 2 years ago

@maxsnew can you give this another look?

maxsnew commented 2 years ago

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 commented 2 years ago

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

Boarders commented 2 years ago

@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 commented 2 years ago

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.

JacquesCarette commented 1 year ago

Oh my, this completely slipped through. Reviewing now.