<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote"><div>Hello Ralf,</div><div><br></div><div>Thank you for all the answers!  It really helped me.  Now I understand more of the documentation, and yet I still have some remaining questions:</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><span class="">> - Page 2: "if its action F1 on arrows": I think "F1" here is a little<br>
> bit confusing.  What exactly does it mean?<br>
<br>
</span>As far as I know, this is standard terminology/notation in category<br>
theory. Given a functor F : C1 -> C2, it is really two functions: F_0,<br>
the action on objects (mapping objects of C0 to objects of C1), and F_1,<br>
the action on arrows (mapping arrows of C0 to arrows of C1, and suitably<br>
compatible with F_0).<br>
So, in this case, we are saying that the function "\lambda f. F(f)",<br>
i.e. calling the functor F on arrows f of the category COFE, must be<br>
non-expansive.<br>
<br>
The idea behind these category-theoretic remarks is that if you know<br>
category theory, they should be helfpul; if not, just ignore them. :)<br>
Understanding them is certainly not required to just use Iris as a logic.<span class=""><br></span></blockquote><div><br></div><div>Ah I see :-)  May I ask which reference/textbook you are consulting to?  Because it is different from the convention in the textbook I learned from (Mac Lane. Categories for the Working Mathematician. Springer GTM 5)..</div><div><br></div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><span class="">
> - Page 9: in what sense "↑(S, T)" is the closure?  I mean, is it minimal<br>
> w.r.t. the closedness?  If so, is it obvious?<br>
<br>
</span>It is adding exactly those elements that successors of elements in S.<br>
So I would say it is pretty obvious that this makes it the smallest set<br>
containing S that is closed under successors.</blockquote></div><div class="gmail_extra"><br></div><div class="gmail_extra">I am concerned with the condition of the closedness that \mathcal{L}(s) # T..  Due to this restriction I believe the closure is in general not minimal w.r.t. the closedness.</div><div><br></div><div>Another remark on the closedness is: the definition of s \stackrel{T}{\rightarrow} s' involves the existential quantification of T1 and T2, and I think there exists an alternative definition that does not involve that quantification:</div><div>    [(\mathcal{L}(s') # T) /\ s \rightarrow s' .]<br></div><div>This is obtained by letting T1 and T2 be (\mathcal{L}(s') \setminus \mathcal{L}(s)) and (\mathcal{L}(s) \setminus \mathcal{L}(s')).  I guess the definition in the documentation is more amenable to the proof, and for this reason you choose to define in that way.  May I ask what is the reason?<br></div><div><br></div><div><br></div><div>Thank you,</div><div>Jeehoon</div><div><br></div>-- <br><div class="gmail_signature" data-smartmail="gmail_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>