<html>

<head>

<meta http-equiv="Content-Type" content="text/html; charset=euc-kr">

</head>

<body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; color: rgb(0, 0, 0); font-size: 14px; font-family: Calibri, sans-serif;">

<div>Interesting. Are there any more details about the cubical development anywhere?</div>

<div><br>

</div>

<div>Cheers,</div>

<div>Thorsten</div>

<div><br>

</div>

<span id="OLK_SRC_BODY_SECTION">

<div style="font-family:Calibri; font-size:11pt; text-align:left; color:black; BORDER-BOTTOM: medium none; BORDER-LEFT: medium none; PADDING-BOTTOM: 0in; PADDING-LEFT: 0in; PADDING-RIGHT: 0in; BORDER-TOP: #b5c4df 1pt solid; BORDER-RIGHT: medium none; PADDING-TOP: 3pt">

<span style="font-weight:bold">From: </span>Agda <<a href="mailto:agda-bounces@lists.chalmers.se">agda-bounces@lists.chalmers.se</a>> on behalf of Apostolis Xekoukoulotakis <<a href="mailto:apostolis.xekoukoulotakis@gmail.com">apostolis.xekoukoulotakis@gmail.com</a>><br>

<span style="font-weight:bold">Date: </span>Thursday, 23 February 2017 at 15:42<br>

<span style="font-weight:bold">To: </span>Jannis Limperg <<a href="mailto:jannis@limperg.de">jannis@limperg.de</a>><br>

<span style="font-weight:bold">Cc: </span>agda list <<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>><br>

<span style="font-weight:bold">Subject: </span>Re: [Agda] Propositional equality for coinductive records<br>

</div>

<div><br>

</div>

<div>

<div>

<div dir="ltr">

<div>You can look at the cubical branch and the cubical demos.<br>

<br>

<a href="https://github.com/Saizan/cubical-demo/blob/master/Stream.agda#L45">https://github.com/Saizan/cubical-demo/blob/master/Stream.agda#L45</a><br>

<br>

</div>

You can turn a bisimulation into an equality.<br>

</div>

<div class="gmail_extra"><br>

<div class="gmail_quote">On Thu, Feb 23, 2017 at 5:32 PM, Jannis Limperg <span dir="ltr">

<<a href="mailto:jannis@limperg.de" target="_blank">jannis@limperg.de</a>></span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">

Dear all,<br>

<br>

propositional equality for coinductive records is currently extremely<br>

restricted since it is not possible (as far as I can tell) to go from<br>

propositional equality of all fields to equality of the records. For<br>

example, it is impossible to define `R-ext` in the following example due<br>

to the inability to destruct `r` and `s`.<br>

<br>

<br>

    data ? : Set where tt : ?<br>

<br>

    data _Ёе_ {a} {A : Set a} (x : A) : A Ёц Set a where<br>

      refl : x Ёе x<br>

<br>

    record R : Set where<br>

      coinductive<br>

      field force : R<br>

<br>

    open R<br>

<br>

    R-ext : {r s : R} Ёц force r Ёе force s Ёц r Ёе s<br>

    R-ext = ?<br>

<br>

This contrasts with Coq (and probably Agda's old coinduction) which<br>

would allow similar equalities to be exploited.<br>

<br>

Now, propositional equality on coinductive data is not often useful<br>

anyway since it is too restrictive for most purposes. However, I have a<br>

corecursive function, say `f`, for which I can prove `force (f x) Ёе<br>

force (g x)` for some simpler `g`, and being able to turn this into<br>

`f x Ёе g x` would make it much easier to apply the equation in other<br>

proofs. Reformulating it in terms of a bisimulation (`force r Ёе force s<br>

Ёц Bisim r s`) would be possible, but much less convenient for users of `f`.<br>

<br>

So,<br>

<br>

- Has anyone else experienced this problem (and perhaps found a good<br>

workaround)?<br>

- Would it be desirable to recover this form of 'extensionality' for<br>

coinductive records, and if so how could this be done?<br>

- Is adding `R-ext` as an axiom dangerous?<br>

<br>

Thanks for your consideration,<br>

Jannis<br>

______________________________<wbr>_________________<br>

Agda mailing list<br>

<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>

<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>

</blockquote>

</div>

<br>

</div>

</div>

</div>

</span>

<PRE>

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.

</PRE></body>

</html>