[Agda] Performance: opening parameterized modules before the fields of a record

[Jacques Carette]

On 2020-05-20 3:05 a.m., Andreas Abel wrote:

> > Could it be that this adds ~100 let-ins in the type of each of the 
> fields?
>
> No, but it creates a new module which contains specializations of all 
> the definitions in CCat+.  These will be positivity-checked.
>
> Could you check whether you can get some speedup by restricting to the 
> actually needed imports?  Something like
>
>   open CCat+ ccat using (Ob; foo; bar) renaming (Mor to MorC)

I did do the above in a few key places in agda-categories, and it 
definitely helped there.

Jacques