IntersectMBO / IntersectMBO/formal-ledger-specifications
Equality in the PDF
Open
documentation
enhancement
latex
- Dominant language
- Agda
- Stars
- 52
- Forks
- 20
- Avg merge
- 6d 14h
- Merged PRs (30d)
- 7
Description
This is somewhat similar to #281 and related to #241. We need some consistent strategy for how to deal with equalities. In particular: Do we assume/pretend to have/use (e.g. via `--erased-cubical`) quotients?
Here are some equalities we're using:
- [ ] `_≡_`
- [ ] `_≗_`
- [ ] `_≡ᵉ_`
Note: this issue is only for the presentation. The underlying problem of what to actually do in Agda is a much bigger, separate task.
Contributor guide
Assessment
This issue has not been assessed yet.