[Agda] Re: comlicated equivalence: need help to prove: errh, addres of repository

[Nils Anders Danielsson]

On 2011-02-24 15:36, Daniel Peebles wrote:
> If you're wondering why the name includes the underlying category, so
> am I. It's very puzzling, but if I don't include the C parameter (by
> making it implicit) even in the type of refl, it'll turn yellow. I
> could understand it having trouble if C were an index to the type, but
> as a parameter, the unsolved metas make no sense to me.

If you make the irrelevant fields relevant, then the parameter can be
inferred. Andreas may know more.

-- 
/NAD