[Agda] Prop in Agda 2.6 - again

[Jesper Cockx]

Hi Thorsten,

That's what I thought at first, but then I realized it would be unsound to
have the projections even *without* eta equality, since you would still be
able to get something relevant out of a Prop. So it is the existence of the
projections itself rather than eta which is problematic for such a type.

-- Jesper

On Wed, Jun 5, 2019 at 4:23 PM Thorsten Altenkirch <
Thorsten.Altenkirch at nottingham.ac.uk> wrote:

> I would paraphrase tis differently: the eta rule for record times makes
> the projections strictly injective and this is obviously false in this
> example. Or do I miss something here?
>
>
>
> Thorsten
>
>
>
> *From: *Agda <agda-bounces at lists.chalmers.se> on behalf of Andrew Pitts <
> andrew.pitts at cl.cam.ac.uk>
> *Date: *Wednesday, 5 June 2019 at 14:45
> *To: *Jesper Cockx <Jesper at sikanda.be>, agda list <agda at lists.chalmers.se>
> *Subject: *Re: [Agda] Prop in Agda 2.6 - again
>
>
>
> Dear Jesper,
>
>
>
> On 5 Jun 2019, at 13:34, Jesper Cockx <Jesper at sikanda.be> wrote:
>
>
>
> Hi Andy,
>
>
>
> When you define a datatype in Prop, the resulting type is automatically
> 'squashed', i.e. any two elements are equal. In contrast, for record types
> this is not possible because then it is impossible to define the
> projections. For your definition of ∃ in Prop, (true , _) is equal to
> (false , _) of type `∃ Bool (λ _ → ⊤)`, but their first projections are
> not equal. It would theoretically be possible to have such a record type
> but not give access to the projections and disabling eta-equality, but then
> you could've equally defined it as a single-constructor datatype.
>
>
>
> I see. So to paraphrase your explanation, Agda imposes a simple syntactic
> restriction on what record types can be declared to have type Prop in order
> to maintain the soundness of forcing all elements of an element of a Prop
> to be definitionally equal.
>
>
>
> I can think of a simple syntactic restriction that is less liberal than
> the current one: don’t allow record types in Prop! Is there an example of
> why my restriction is too restrictive? —- in other words a case where using
> a record of Prop type is really better than using a corresponding
> single-constructor datatype of type Prop?
>
>
>
> (I am thinking that one often uses a record type in Set instead of a
> single-constructor-datatype in Set, in order to get definitional eta
> expansion; but that’s automatic for elements of Prop, due to the
> definitional proof irrelevance.)
>
>
>
> Andy
>
>
>
>
>
>
>
> -- Jesper
>
>
>
> On Wed, Jun 5, 2019 at 1:09 PM Andrew Pitts <andrew.pitts at cl.cam.ac.uk>
> wrote:
>
> Here is another question about Prop in Agda 2.6. Can anyone enlighten me?
>
> The documentation says
>
> "Just as for Set, we can define new types in Prop’s as data or record
> types”
>
> However, although Agda 2.6 allows the declaration of the following
> one-constructor datatype
>
> data ∃ {l m}(A : Set l)(P : A → Prop m) : Prop (l ⊔ m) where
>   _,_ : (x : A)(p : P x) → ∃ A P
>
> if instead I try to define a record type
>
> record ∃ {l m : Level}(A : Set l)(B : A → Prop m) : Prop (l ⊔ m) where
>   constructor _,_
>   field
>     fst : A
>     snd : B fst
>
> Agda complains (somewhat ungrammatically) that
>
> "Set l is not less or equal than Prop (l ⊔ m) when checking the
> definition of ∃”
>
> So it doesn’t mind the parameter (A : Set l) when defining a datatype in
> Prop (l ⊔ m), but does mind it when defining a record type.
>
> Why is that?
>
> Andy
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
>
> 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 contact the sender and delete the email and
> attachment.
>
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored
> where permitted by law.
>
>
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190605/7ca58a0c/attachment.html>