[Agda] congruence on dependent types

Nils Anders Danielsson nad at cse.gu.se
Fri Jun 21 12:08:33 CEST 2013

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.


More information about the Agda mailing list