[Agda] congruence on dependent types

Guillaume Brunerie guillaume.brunerie at gmail.com
Fri Jun 21 12:55:31 CEST 2013

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

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?


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

More information about the Agda mailing list