[Agda] Why no impredicative prop?

[Timothy Carstens]

Forgive me, I errored in my description of the issue.

In their example they define ref : type -> type, but the definition
witnesses an equality over type, which pushes ref into Set (i + 1).

-t


On Tue, Dec 29, 2015 at 7:13 PM, Timothy Carstens <intoverflow at gmail.com>
wrote:

> For most of the work I've done I haven't needed an impredicative universe;
> that is, the main reason I'd use Prop in Coq was that the OCaml extractor
> would eliminate Prop terms, which was nice.
>
> But then I tried to implement indirection theory in the style of Hobor,
> Dockins, Appel [1]. One can carry out their construction just fine, but
> (from what I can tell) using the construction in the manner shown in their
> examples requires an impredicative sort.
>
> Namely, in section 4.1 they wind up in a situation where they have
>
> T some type, say Set i
>
> type = memtype * value -> T
>
> ref : type -> type
>
> At this point, their usage of 'ref' seems to require (type -> type : T),
> which only seems possible if T is impredicative.
>
> I'm unsure whether or not their construction could be carried out in a
> satisfactory way by (for example) trying to make a universe-polymoprhic
> version of 'type'. Regardless, running into this obstacle got me to
> wondering whether or not there was a theoretical obstruction to Agda having
> an impredicative prop.
>
> [1] http://vst.cs.princeton.edu/msl/indirection.pdf
>
> -t
>
>
> On Tue, Dec 29, 2015 at 2:11 PM, Thorsten Altenkirch <
> Thorsten.Altenkirch at nottingham.ac.uk> wrote:
>
>> Actually why do you need an impredicative universe?
>>
>> From a purely pragmatic point it is a bit strange if one universe behaves
>> different from the other one. But having two impredicative universes is
>> already unsound.
>>
>> More on the philosphical side: impredicativity is basically a classical
>> idea which arises from the identification of Prop and Bool. I don’t know an
>> intuitionistic justification of impredicativity.
>>
>> Thorsten
>>
>> From: <agda-bounces at lists.chalmers.se> on behalf of Timothy Carstens <
>> intoverflow at gmail.com>
>> Date: Tuesday, 29 December 2015 17:19
>> To: "agda at lists.chalmers.se" <agda at lists.chalmers.se>
>> Subject: [Agda] Why no impredicative prop?
>>
>> Hello,
>>
>> I'm a relatively new Agda user, coming from a background using Coq for
>> the past few years. As is well known, Coq has an impredicative Prop sort,
>> while Agda does not.
>>
>> Why not? Is it simply a matter of project goals, or is there something
>> about Agda's underlying theory which is incompatible with having an
>> impredicative sort at the bottom of the universe hierarchy?
>>
>> Forgive me if this is an old topic or has an obvious answer; I'm not a
>> logician, but I use proof assistants at work.
>> -t
>>
>>
>> This message and any attachment are intended solely for the addressee
>> and may contain confidential information. If you have received this
>> message in error, please send it back to me, and immediately delete it.
>>
>> Please do not use, copy or disclose the information contained in this
>> message or in any attachment.  Any views or opinions expressed by the
>> author of this email do not necessarily reflect the views of the
>> University of Nottingham.
>>
>> This message has been checked for viruses but the contents of an
>> attachment may still contain software viruses which could damage your
>> computer system, you are advised to perform your own checks. Email
>> communications with the University of Nottingham may be monitored as
>> permitted by UK legislation.
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151229/18cf90f5/attachment.html