[Agda] congruence on dependent types

[Guillaume Brunerie]

I think you would be interested in the univalence axiom, see in particular
section 2.14 of the recently released HoTT book.

Guillaume
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

_______________________________________________
Agda mailing list
Agda at lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130621/5149d1b3/attachment.html