[Agda] Propositional equality for coinductive records

[Andrea Vezzosi]

So far there are only the examples at

https://github.com/Saizan/cubical-demo

Documentation should be coming soon, also because it's now in the master branch.

Best,
Andrea

On Fri, Feb 24, 2017 at 11:11 AM, Thorsten Altenkirch
<Thorsten.Altenkirch at nottingham.ac.uk> wrote:
> Interesting. Are there any more details about the cubical development
> anywhere?
>
> Cheers,
> Thorsten
>
> From: Agda <agda-bounces at lists.chalmers.se> on behalf of Apostolis
> Xekoukoulotakis <apostolis.xekoukoulotakis at gmail.com>
> Date: Thursday, 23 February 2017 at 15:42
> To: Jannis Limperg <jannis at limperg.de>
> Cc: agda list <Agda at lists.chalmers.se>
> Subject: Re: [Agda] Propositional equality for coinductive records
>
> You can look at the cubical branch and the cubical demos.
>
> https://github.com/Saizan/cubical-demo/blob/master/Stream.agda#L45
>
> You can turn a bisimulation into an equality.
>
> On Thu, Feb 23, 2017 at 5:32 PM, Jannis Limperg <jannis at limperg.de> wrote:
>>
>> Dear all,
>>
>> propositional equality for coinductive records is currently extremely
>> restricted since it is not possible (as far as I can tell) to go from
>> propositional equality of all fields to equality of the records. For
>> example, it is impossible to define `R-ext` in the following example due
>> to the inability to destruct `r` and `s`.
>>
>>
>>     data ? : Set where tt : ?
>>
>>
>>     data _≡_ {a} {A : Set a} (x : A) : A → Set a where
>>       refl : x ≡ x
>>
>>     record R : Set where
>>       coinductive
>>       field force : R
>>
>>     open R
>>
>>     R-ext : {r s : R} → force r ≡ force s → r ≡ s
>>     R-ext = ?
>>
>> This contrasts with Coq (and probably Agda's old coinduction) which
>> would allow similar equalities to be exploited.
>>
>> Now, propositional equality on coinductive data is not often useful
>> anyway since it is too restrictive for most purposes. However, I have a
>> corecursive function, say `f`, for which I can prove `force (f x) ≡
>> force (g x)` for some simpler `g`, and being able to turn this into
>> `f x ≡ g x` would make it much easier to apply the equation in other
>> proofs. Reformulating it in terms of a bisimulation (`force r ≡ force s
>> → Bisim r s`) would be possible, but much less convenient for users of
>> `f`.
>>
>> So,
>>
>> - Has anyone else experienced this problem (and perhaps found a good
>> workaround)?
>> - Would it be desirable to recover this form of 'extensionality' for
>> coinductive records, and if so how could this be done?
>> - Is adding `R-ext` as an axiom dangerous?
>>
>> Thanks for your consideration,
>> Jannis
>> _______________________________________________
>> 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 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.
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>