[Agda] Avoiding implicit argument proliferation?

[Nils Anders Danielsson]

On 2011-03-29 00:23, Brandon Moore wrote:
> A structure is introduced as a parameterized record containing all the
> interesting fields.
>
> record FunctorP(C D : Category) : Set where ...
>
> Then to hide indices another record contains just the parameters and
> an instance of the parametrized record.
>
> record Functor : Set₁ where
>    field
>      C D : Category
>      F : FunctorP C D

The standard library's algebra and binary relation hierarchies also use
two levels of modules (see README.agda).

-- 
/NAD