agda/agda-stdlib — pull request #42 by jmchapman (2014-10-21 06:10:33+00:00)
Title: Added Relation/Binary/HeterogeneousEquality/Quotients.agda

It contains a definition of quotients as a record that you can postulate
as you would for extensionality and some useful lemmas. Also added a
hetergeneous version of proof irrelevance to
HeterogeneousEquality.agda.