[Agda] Trust me regarding Dan Licata's trick

[Martin Escardo]

Thanks, Dan, for your thoughts.

It is interesting that in a paper (and corresponding Agda file) by 
Nicolai Kraus, Thierry Coquand, Thorten Altenkirch and myself we can do 
a lot (both positively and negatively) with hpropositional reflection 
without assuming that the elimination rule holds definitionally.

In the discussion in this thread, the fact the the elimination rule 
holds definitionally is crucial (without that, we don't get 
extensionlity, for instance).

One question we had, and still have, is whether hpropositional 
reflection is definable, without requiring that the elimination rule 
holds definitionally. This seems unlikely (even more now), but it also 
seems difficult to argue about that.

So I would like to repeat an open problem we posed in the paper: is 
hpropositional reflection definable in intensional type theory, assuming 
that the elimination rule holds propositionally but not necessarily 
definitionally? This seems to be an interesting open question.

The answer is likely to be negative, but I expect to learn something new 
from it.

Best,
Martin

On 15/06/13 13:44, Dan Licata wrote:
>
> 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
>
>