[Agda] Avoiding implicit argument proliferation?

[Nils Anders Danielsson]

On 2011-03-23 08:00, Brandon Moore wrote:
> Here's some code, extracted from an attempt at formalizing early excercies
> in "Categories for the Working Mathematician". The hidden arguments
> continue to accumulate as higher structures are build. They can be inferred,
> so working with these definitions in expressions is not too bad, but to state
> any types it seems I need to quantify over (and manually provide) all these
> implicit arguments.

See the following thread for a previous discussion about this issue:

   Why aren't free vars in types automatically generalized
   http://thread.gmane.org/gmane.comp.lang.agda/772

-- 
/NAD