[Agda] congruence on dependent types

Nils Anders Danielsson nad at cse.gu.se
Sun Jun 23 19:50:57 CEST 2013

On 2013-06-21 12:38, Sergei Meshveliani wrote:
> 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?

Quotient types. (Note that this term may also have multiple meanings.)

You may want to take a look at "Definable Quotients in Type Theory" by
Altenkirch, Anberrée and Li
(http://www.cs.nott.ac.uk/~txa/publ/defquotients.pdf). This paper
describes a technique which, in some cases, can be used in the current
version of Agda. The paper also contains references to other work on
quotient types.


More information about the Agda mailing list