anuyts
anuyts
In general, anything whose type mentions a datatype or record defined in the same module, doesn't need all the parameters explicitly as they can be inferred thanks to injectivity of...
In the above examples I would use it on `_++_`, `frst` and `scnd` so that these functions can be called from outside the module without the explicit argument `A`.
Well this was a baby example of course. What if my module doesn't have 1 but 10 parameters? Then your approach has a few drawbacks: * Every definition that needs...
As a real-life example, the definitions [`FunNatL→isLeftRelativeRightAdhocAdjunction`](https://github.com/anuyts/cubical/blob/d39b7b651262e063a6e5565a73d6184e701ac1a6/Cubical/Categories/Adjoint/Relative.agda#L88) and [`InvNatL→isLeftRelativeRightAdhocAdjunction`](https://github.com/anuyts/cubical/blob/d39b7b651262e063a6e5565a73d6184e701ac1a6/Cubical/Categories/Adjoint/Relative.agda#L92) in my [draft pull request about (relative) adjunctions](https://github.com/agda/cubical/pull/873), could use the proposed keyword (let's call it **subinjective** as it is usable...
The situation would be analogous to implicit arguments. Agda allows any argument to be declared to be implicit, but it's only a good idea if the argument can actually be...
In general this keyword would just be a "nice thing to have" but I think it's particularly important because it is already applied silently and automatically to constructors and record...
Point 1: I guess in principle you could consider this even for each individual module parameter in scope. I would say the most important thing is enabling the user to...
See also #6036.
For what it's worth, I'm having a similar issue. On [line 216 here](https://github.com/anuyts/ctx-alg/blob/c294cfef1b43b88827f761e922fd49364c12a2ea/src/Mat/Free/Term.agda#L216), I have a functor definition that does not type-check within reasonable time. The functor is defined by...