[Agda] congruence on dependent types
mechvel at botik.ru
Fri Jun 21 12:58:33 CEST 2013
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.
More information about the Agda