IntersectMBO / IntersectMBO/formal-ledger-specifications
Make `Functor` instance for `ℙ_`
Open
enhancement
investigation
- Dominant language
- Agda
- Stars
- 52
- Forks
- 20
- Avg merge
- 6d 14h
- Merged PRs (30d)
- 7
Description
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.
Contributor guide
Assessment
This issue has not been assessed yet.