<div dir="ltr"><span class="gmail-m_-9204929174622241972gmail-"></span>Thank you for answering all the questions I have asked.  Always your answers enlightened me a lot :)  Here are the remaining questions to the answers.<br><br><br><br>On <span class="gmail-m_-9204929174622241972gmail-">ξ and ξ^{−1}: I agree that it is not worth an issue to examine further.  I realized that what I wanted to ask is: how it is done in Coq?<br></span><br><br><br><div><div class="gmail_extra"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
Indeed, if you do that in Coq, you get a universe conflict.  And I think<br>
that's not just superficial; if you do the same in set theory, you would<br>
get the same problem -- the "CMRA of all CMRAs" can't contain itself, or<br>
else Russel comes and hits you with his paradox.<br></blockquote><div><br></div><div>But you anyway need to provide the list of CMRAs, right?  Then the list of CMRAs can also be interpreted as a CMRA, while it does not incur universe size problem.  I would like to ask if we could do the same technique here: just define the logic with the product of all CMRAs (whose size is less than something), and let users to use only those CMRAs that are small enough.<br><br></div><div>I am quite sure my explanation is bad :-\  maybe it would be better for me to contribute to Iris in this respect (or learn why it is difficult to do that by actually doing some proofs in Coq).  I will return to this subject as soon as I am used to iris-coq.<br></div><div><br><br><br></div><div>On composability: what about "compositionality" as said in the parametric (bi)simulation works?<br clear="all"></div></div><br><br><br></div><div class="gmail_extra">Best regards,<br></div><div class="gmail_extra">Jeehoon<br></div><div class="gmail_extra"><br><br>-- <br><div class="gmail-m_-9204929174622241972gmail_signature"><div dir="ltr"><a href="http://sf.snu.ac.kr/jeehoon.kang" target="_blank">Jeehoon Kang (Ph.D. student)</a><div><a href="http://sf.snu.ac.kr" target="_blank">Software Foundations Laboratory</a><div><a href="http://www.snu.ac.kr" target="_blank">Seoul National University</a></div></div></div></div>
</div></div></div>