[Agda] Why no impredicative prop?

[Thorsten Altenkirch]

Hi Timothy,

in this case there is no need for impredicativity. In fact you can define an equality of types which doesn’t increase the level:

data _≡T_ {a} (A : Set a) : Set a → Set a where
    refl : A ≡T A

And this is equivalent to the usual equality only on a lower level.

Actually the view that equality of types is a type (of the same level) is supported by Univalent Type Theory which assumes that equality of types is equivalent to equivalence which is a type at the same level.

Thorsten

From: Timothy Carstens <intoverflow at gmail.com<mailto:intoverflow at gmail.com>>
Date: Wednesday, 30 December 2015 04:13
To: Thorsten Altenkirch <thorsten.altenkirch at nottingham.ac.uk<mailto:thorsten.altenkirch at nottingham.ac.uk>>
Cc: "agda at lists.chalmers.se<mailto:agda at lists.chalmers.se>" <agda at lists.chalmers.se<mailto:agda at lists.chalmers.se>>
Subject: Re: [Agda] Why no impredicative prop?

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<mailto: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<mailto: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<mailto:agda-bounces at lists.chalmers.se>> on behalf of Timothy Carstens <intoverflow at gmail.com<mailto:intoverflow at gmail.com>>
Date: Tuesday, 29 December 2015 17:19
To: "agda at lists.chalmers.se<mailto:agda at lists.chalmers.se>" <agda at lists.chalmers.se<mailto: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.







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/20151230/d0a6ed18/attachment-0001.html