[Agda] congruence on dependent types

[Sergei Meshveliani]

On Fri, 2013-06-21 at 14:38 +0400, Sergei Meshveliani wrote:
> 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?
> 

But there is something in it!  Thank you.

Instead of setting    PSSmg a,  PSSmg b,   for  a, b : C,

build the quotient set    C' = C/associated

by the relation  associated : Rel C _  (which I described earlier).
This can be expressed as a dependent type in Agda.

Then apply  PSSmg  to  C'  rather than to  C.
Probably, this will remove the problem of replacing  a  with equivalent
b  in  f : PSSmg a.  Because they project to the same element in C'.

If so, then the language extension becomes not so actual.

------
Sergei