Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Merged
merged 8 commits into from
Jan 11, 2023

Conversation

Boarders
Copy link
Contributor

@Boarders Boarders commented Apr 15, 2022

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

Still to do:

  • Defining the underlying vertical and horizontal 2-categories

@Boarders
Copy link
Contributor Author

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).

src/Categories/Double/Core.agda Outdated Show resolved Hide resolved
src/Categories/Double/Core.agda Outdated Show resolved Hide resolved
src/Categories/Double/Core.agda Outdated Show resolved Hide resolved
src/Categories/Double/Core.agda Show resolved Hide resolved
src/Categories/Double/Core.agda Outdated Show resolved Hide resolved
@JacquesCarette
Copy link
Collaborator

@maxsnew can you give this another look?

@maxsnew
Copy link
Contributor

maxsnew commented May 3, 2022 via email

Copy link
Collaborator

@JacquesCarette JacquesCarette left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks like there's still some stuff that needs looked at.

src/Categories/Double/Core.agda Outdated Show resolved Hide resolved
src/Categories/Double/Core.agda Outdated Show resolved Hide resolved
src/Categories/Double/Core.agda Outdated Show resolved Hide resolved
src/Categories/Double/Core.agda Outdated Show resolved Hide resolved
src/Categories/Double/Core.agda Outdated Show resolved Hide resolved
@Boarders
Copy link
Contributor Author

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

@Boarders
Copy link
Contributor Author

Boarders commented Jul 7, 2022

@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
Copy link
Collaborator

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
Copy link
Collaborator

Oh my, this completely slipped through. Reviewing now.

@JacquesCarette JacquesCarette merged commit 39a5f9a into agda:master Jan 11, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants