<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class="">
Dear Jeehon,
<div class=""><br class="">
</div>
<div class="">The fixed point is unique, see 5.10 in the tutorial notes:</div>
<div class="">   <a href="http://cs.au.dk/~abizjak/documents/publications/categorical-logic-tutorial-notes.pdf" class="">http://cs.au.dk/~abizjak/documents/publications/categorical-logic-tutorial-notes.pdf</a></div>
<div class=""><br class="">
</div>
<div class="">
<div class="">Best,</div>
<div class="">Lars.</div>
<div class=""><br class="">
<div>
<blockquote type="cite" class="">
<div class="">On 20 Aug 2016, at 16:22, Jeehoon Kang <<a href="mailto:jeehoon.kang@sf.snu.ac.kr" class="">jeehoon.kang@sf.snu.ac.kr</a>> wrote:</div>
<br class="Apple-interchange-newline">
<div class="">
<div dir="ltr" style="font-family: Helvetica; font-size: 14px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">
Another point is that, "wp is defined as the fixed-point of a contractive function," but I am not sure there is "the" fixed-point.  Previously in the documentation it is only said that a contractive function has "a" fixed-point.
<div class=""><br class="">
</div>
<div class="">- Is it indeed "the" fixed-point"?</div>
<div class="">- If not, in what sense a chosen fixed-point is canonical?<br class="">
<div class=""><br class="">
</div>
<div class="">Thank you,</div>
<div class="">Jeehoon</div>
</div>
</div>
<div class="gmail_extra" style="font-family: Helvetica; font-size: 14px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;">
<br class="">
<div class="gmail_quote">2016-08-20 23:02 GMT+09:00 Jeehoon Kang<span class="Apple-converted-space"> </span><span dir="ltr" class=""><<a href="mailto:jeehoon.kang@sf.snu.ac.kr" target="_blank" class="">jeehoon.kang@sf.snu.ac.kr</a>></span>:<br class="">
<blockquote class="gmail_quote" style="margin: 0px 0px 0px 0.8ex; border-left-width: 1px; border-left-color: rgb(204, 204, 204); border-left-style: solid; padding-left: 1ex;">
<div dir="ltr" class="">I think I almost understand `pre-wp` ;-)  But I still cannot understand the use of step-index: may I ask what is the intuition behind requiring `m+1 \in ...` for the value case?  I think I understand why you required `m in ...` in the
 reduction case, since there is actually a step.  But for the value case, I am not sure why it is necessary to demand `m+1 \in ...`.  Why `m \in ...` is not enough?
<div class=""><br class="">
</div>
<div class="">Thank you,</div>
<div class="">Jeehoon</div>
</div>
<div class="gmail_extra">
<div class="">
<div class="h5"><br class="">
<div class="gmail_quote">2016-08-19 21:14 GMT+09:00 Ralf Jung<span class="Apple-converted-space"> </span><span dir="ltr" class=""><<a href="mailto:jung@mpi-sws.org" target="_blank" class="">jung@mpi-sws.org</a>></span>:<br class="">
<blockquote class="gmail_quote" style="margin: 0px 0px 0px 0.8ex; border-left-width: 1px; border-left-color: rgb(204, 204, 204); border-left-style: solid; padding-left: 1ex;">
Hi,<br class="">
<span class=""><br class="">
> But I am still confused of the definition of `pre-wp`..  In the 2nd<br class="">
> line, `s` should have the type ∆(Val), mandated by `ϕ(s)`; and yet at<br class="">
> the same time `s` should have the type Res, from `s · rf`.  May I ask if<br class="">
> what am I missing here?<br class="">
<br class="">
</span>Right, that should have been ϕ(v)(s). Then things hopefully make sense...<br class="">
<div class="">
<div class=""><br class="">
Kind regards,<br class="">
Ralf<br class="">
<br class="">
--<br class="">
<a href="mailto:iris-club@lists.mpi-sws.org" target="_blank" class="">iris-club@lists.mpi-sws.org</a><span class="Apple-converted-space"> </span>- Mailing List for the Iris Logic<br class="">
Management:<span class="Apple-converted-space"> </span><a href="https://lists.mpi-sws.org/listinfo/iris-club" rel="noreferrer" target="_blank" class="">https://lists.mpi-sws.org/list<wbr class="">info/iris-club</a><br class="">
Unsubscribe:<span class="Apple-converted-space"> </span><a href="mailto:iris-club-unsubscribe@lists.mpi-sws.org" target="_blank" class="">iris-club-unsubscribe@lists.mp<wbr class="">i-sws.org</a><br class="">
</div>
</div>
</blockquote>
</div>
<br class="">
<br clear="all" class="">
<div class=""><br class="">
</div>
</div>
</div>
<span class="">--<span class="Apple-converted-space"> </span><br class="">
<div data-smartmail="gmail_signature" class="">
<div dir="ltr" class=""><a href="http://sf.snu.ac.kr/jeehoon.kang" target="_blank" class="">Jeehoon Kang (Ph.D. student)</a>
<div class=""><a href="http://sf.snu.ac.kr/" target="_blank" class="">Software Foundations Laboratory</a>
<div class=""><a href="http://www.snu.ac.kr/" target="_blank" class="">Seoul National University</a></div>
</div>
</div>
</div>
</span></div>
</blockquote>
</div>
<br class="">
<br clear="all" class="">
<div class=""><br class="">
</div>
--<span class="Apple-converted-space"> </span><br class="">
<div class="gmail_signature" data-smartmail="gmail_signature">
<div dir="ltr" class=""><a href="http://sf.snu.ac.kr/jeehoon.kang" target="_blank" class="">Jeehoon Kang (Ph.D. student)</a>
<div class=""><a href="http://sf.snu.ac.kr/" target="_blank" class="">Software Foundations Laboratory</a>
<div class=""><a href="http://www.snu.ac.kr/" target="_blank" class="">Seoul National University</a></div>
</div>
</div>
</div>
</div>
<span style="font-family: Helvetica; font-size: 14px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px; float: none; display: inline !important;" class="">--<span class="Apple-converted-space"> </span></span><br style="font-family: Helvetica; font-size: 14px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">
<a href="mailto:iris-club@lists.mpi-sws.org" style="font-family: Helvetica; font-size: 14px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">iris-club@lists.mpi-sws.org</a><span style="font-family: Helvetica; font-size: 14px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px; float: none; display: inline !important;" class=""><span class="Apple-converted-space"> </span>-
 Mailing List for the Iris Logic</span><br style="font-family: Helvetica; font-size: 14px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">
<span style="font-family: Helvetica; font-size: 14px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px; float: none; display: inline !important;" class="">Management:<span class="Apple-converted-space"> </span></span><a href="https://lists.mpi-sws.org/listinfo/iris-club" style="font-family: Helvetica; font-size: 14px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">https://lists.mpi-sws.org/listinfo/iris-club</a><br style="font-family: Helvetica; font-size: 14px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">
<span style="font-family: Helvetica; font-size: 14px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px; float: none; display: inline !important;" class="">Unsubscribe:<span class="Apple-converted-space"> </span></span><a href="mailto:iris-club-unsubscribe@lists.mpi-sws.org" style="font-family: Helvetica; font-size: 14px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">iris-club-unsubscribe@lists.mpi-sws.org</a></div>
</blockquote>
</div>
<br class="">
</div>
</div>
</body>
</html>