[Agda] congruence on dependent types

[Nils Anders Danielsson]

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.

-- 
/NAD