[Agda] congruence on dependent types

[Sergei Meshveliani]

On Fri, 2013-06-21 at 12:08 +0200, Nils Anders Danielsson wrote:
> On 2013-06-20 20:49, Sergei Meshveliani wrote:
> > Is it possible to add some construct foo to the language so that the
> > checker would allow to replace f : PSSmg a with f : PSSmg b, if p :
> > associated a b and foo is set for PSSmg ?
> 
> I didn't read all of your question, but I think you're looking for
> something like quotients.
> 

The word `quotient' is overloaded with various meanings:
quotient of numbers, quotient of two relations, may be, something from
the Agda library ...
Which one do you mean?

------
Sergei