[Agda] Trust me regarding Dan Licata's trick

[Martin Escardo]

On 10/06/13 10:36, Martin Escardo wrote:
> In any case, the above says that implementing hpropositional truncation
> in intensional type theory so that canonicity is not lost is at least as
> hard as implementing the axiom of function extensionality for
> hset-valued functions.

Nicolai Kraus produced a nice improvement of this, which I recorded as
a second part in the Agda file gives before:

http://www.cs.bham.ac.uk/~mhe/truncation-and-extensionality/hsetfunext.html

 From extensionality for dependent hprop-valued functions, one gets
extensionality for arbitrary dependent functions.

Thus, hpropositional truncation with definitional elimination rules
gives full (dependent) function extensionality.

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.

I had the naive view that bracket types amount to "just information
hiding". I will have to seriously revise this view.

Martin