[Agda] Prop in Agda 2.6 - again

[Jesper Cockx]

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.

-- 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190605/e9f551be/attachment.html>