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.

Sign up for GitHub

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

Jump to bottom

Make Functor instance for ℙ_ #322

Open
WhatisRT opened this issue Dec 5, 2023 · 0 comments
Open

Make Functor instance for ℙ_ #322

WhatisRT opened this issue Dec 5, 2023 · 0 comments
Labels
enhancement New feature or request investigation

Comments

@WhatisRT
Copy link
Collaborator

WhatisRT commented Dec 5, 2023

This is a bit non-trivial because of level issues. Functor is by definition level-polymorphic, but the current set-theory isn't quite level-polymorphic enough to support this yet. So we can either make a level-monomorphic version of Functor, or (preferred) make the set-theory more level-polymorphic. See #24.
@WhatisRT WhatisRT mentioned this issue Dec 5, 2023
Closed
33 tasks
@WhatisRT WhatisRT added enhancement New feature or request investigation labels Dec 5, 2023
@WhatisRT WhatisRT added this to the Nov - Feb milestone Dec 6, 2023
@WhatisRT WhatisRT modified the milestones: Nov - Feb, Feb - Apr Feb 5, 2024
@WhatisRT WhatisRT removed this from the Feb - Apr milestone Apr 15, 2024
@WhatisRT WhatisRT mentioned this issue May 8, 2024
Closed
5 tasks
@WhatisRT WhatisRT mentioned this issue Jun 21, 2024
Closed
21 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
enhancement New feature or request investigation
Projects
None yet
Milestone
No milestone
Development

When branches are created from issues, their pull requests are automatically linked.

322-functor-instance-for-powerset IntersectMBO/formal-ledger-specifications
1 participant
@WhatisRT