[Agda] Trust me regarding Dan Licata's trick

[Bas Spitters]

On Sat, Jun 15, 2013 at 2:44 PM, Dan Licata <drl at cs.cmu.edu> wrote:
> Interesting!  That kind of makes sense, in retrospect, because bracket
> types can be thought of as quotienting by the full relation, and, if I
> recall correctly, quotients give you function extensionality.
> (What kinds of quotients are used in the known proofs of this fact?)

Check Martin Hofmann's thesis for this result.
I don't have the time to look for the precise reference now, sorry.

Bas