About a month ago, it was brought up on the fediverse that it should be possible to overload function application in agda. There is a use-case brought up in that thread, but I will mention another here
In agda-categories a NaturalTransformation contains a family of maps (a function from objects to homs) called η. This works well if you would like to refer to your natural transformation by η. However, I often find myself using other natural transformations (such as the counit of an adjunction) refered to by other letters, such as ε. Then, one must write things like adj.ε.η x to refer to what one in mathematics would call $\varepsilon_x$ . Instead, it would be better to refer to this as adj.ε x.
Several libraries, such as the 1lab, already have partial solutions to this. For example, the FunLike typeclass allows users to write ε # x, which resolves to the desired ε .η x
Under this proposal, the user would write
and then F x would implicitly mean F # x, which would find a suitable FunLike instance for F through typeclass search.
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4