[Agda] Trust me regarding Dan Licata's trick

[Dan Licata]

On Jun10, Martin Escardo wrote:
> hPropositionally truncated types are also known as bracket types in
> NuPrl, a well-known implementation of extensional type theory. You may
> wish to check Awodey and Bauer's paper "Propositions as [types]" for a
> theoretical treatment of bracket types in extensional type theory.
>
> It comes to me as a shock that introducing bracket types in
> intensional type theory so that canonicity is preserved is at least as
> hard, if not more, than introducing the axiom of function
> extensionality for dependent functions so that canonicity is
> preserved.

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?)

Also, I think that some of the issues in this thread are related to the
distinction between:

1) hprops, or types where any two elements are propositionally equal

2) what one might call "strict hprops", or types where any two elements
   are definitionally equal.  

The rules for hprop-truncations that we use in HoTT are the "best way of
making any type into an hprop, in the sense of (1)".  I think what you
have noticed in this thread is that a similar construct for "the best
way of making any type into a strict hprop, in the sense of (2)" has
some unexpected consequences.  

-Dan