[Agda] difficult "unsolved metas"

[Serge D. Mechveliani]

On Thu, Feb 07, 2013 at 08:45:41PM +0400, Serge D. Mechveliani wrote:
> [..]
> Agda-2.3.2 MAlonzo (lib-0.7)
> [..]
> "unsolved metas" is reported exactly for the line of  "cong = eCong"
> in the final fragment of
>   ...
>   eTo : sub-Setoid ->c baseSetoid
>   eTo = record{ _($)_ = fromSub     -- : subCarrier -> baseCarrier
>               ; cong  = eCong  }
>         where
>         eCong : _=s_ =[ fromSub ]=> _\equiv_
>         eCong {x} {y} x-=s-y  = ...
> [..]
> and eCong needs to express that  fromSub  preserves the equivalence
> with respect to  _=s_  on subCarrier  and  _\equiv_ on  baseCarrier
> -- which part must be most trivial in this case.

Now I find that I have missed the precise meaning of   =[ fromSub ]=>.
In
   P =[ fromSub ]=> Q,

I have set _=s_ for P  and _\equiv_ for Q.
But  Q  occurs not like  P : Rel A l1,  it is   Q : Rel (A -> Set b) l2.

And it occurs that I do not understand, so far, how to use   =[ fromSub ]=>
for my aim of expressing the congruensy of  fromSub.

May be, I shall find this meaning.
On the other hand, I shall be grateful if somebody happens to find and
show how to correct the code.

------
Sergei