[Iris-Club] Typos (, I think,) in the Iris 2.0 documentation

[Ralf Jung]

Hi,

>     As far as I know, this is standard terminology/notation in category
>     theory. Given a functor F : C1 -> C2, it is really two functions: F_0,
>     the action on objects (mapping objects of C0 to objects of C1), and F_1,
>     the action on arrows (mapping arrows of C0 to arrows of C1, and suitably
>     compatible with F_0).
>     So, in this case, we are saying that the function "\lambda f. F(f)",
>     i.e. calling the functor F on arrows f of the category COFE, must be
>     non-expansive.
> 
>     The idea behind these category-theoretic remarks is that if you know
>     category theory, they should be helfpul; if not, just ignore them. :)
>     Understanding them is certainly not required to just use Iris as a
>     logic.
> 
> 
> 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)..

I have no idea, I just know I saw this notation a few times while we did
our Category Theory seminar... Derek, do you remember?

>     > - Page 9: in what sense "↑(S, T)" is the closure?  I mean, is it minimal
>     > w.r.t. the closedness?  If so, is it obvious?
> 
>     It is adding exactly those elements that successors of elements in S.
>     So I would say it is pretty obvious that this makes it the smallest set
>     containing S that is closed under successors.
> 
> 
> 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.

Oh, right, we also added this well-formedness condition here because we
are lazy. However, considering T to be fixed, this condition is
monotone, i.e., if it rules out a set then it also rules out all larger
sets. How should this violate minimality?

> Another remark on the closedness is: the definition of s
> \stackrel{T}{\rightarrow} s' involves the existential quantification of
> T1 and T2,

Right, this matches exactly the definition in Coq.

> and I think there exists an alternative definition that does
> not involve that quantification:
>     [(\mathcal{L}(s') # T) /\ s \rightarrow s' .]
> 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?

Yeah, this looks equivalent.  I honestly do not know any more why this
is defined the way it is; it is also possible that the definition
changed over time.

Kind regards,
Ralf