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

Coend #78

Open
wants to merge 11 commits into
base: main
Choose a base branch
from
Open

Coend #78

wants to merge 11 commits into from

Conversation

bond15
Copy link
Collaborator

@bond15 bond15 commented May 8, 2024

Should the Set-Coend go in a separate "Instances" file?

@bond15 bond15 self-assigned this May 8, 2024
Copy link
Owner

@maxsnew maxsnew left a comment

Choose a reason for hiding this comment

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

Looks good except for minor notational comments. Also fix the line lengths and white space. You can just run the fix-whitespace utility (cabal install fix-whitespace to install IIRC)

Cubical/Categories/Bifunctor/Base.agda Outdated Show resolved Hide resolved
Cubical/Categories/Constructions/Coend/Base.agda Outdated Show resolved Hide resolved
Cubical/Categories/Constructions/Coend/Base.agda Outdated Show resolved Hide resolved
@bond15 bond15 requested a review from maxsnew May 25, 2024 02:47
@bond15
Copy link
Collaborator Author

bond15 commented Aug 2, 2024

@maxsnew
So should I scrap this and use a similar construction to your definition of Ends ?

@maxsnew
Copy link
Owner

maxsnew commented Aug 2, 2024

Typically we would have two versions: one concrete like yours which is easy to read and understand and one compositional like mine where it's easier to get common properties. Then we would define a function that goes from the concrete to the compositional one.

@bond15
Copy link
Collaborator Author

bond15 commented Aug 3, 2024

Typically we would have two versions: one concrete like yours which is easy to read and understand and one compositional like mine where it's easier to get common properties. Then we would define a function that goes from the concrete to the compositional one.

I can attempt this once both branches are merged in.

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.

2 participants