[Iris-Club] Two Monoid Questions

[Robbert Krebbers]

I realized I defined the type sProp in Coq a long time ago already, but 
never created a merge request for it. I have done that now:

   https://gitlab.mpi-sws.org/iris/iris/merge_requests/304/diffs

I propose we continue this discussion there.

On 16/08/2019 14.30, Ralf Jung wrote:
>> By defining SProp, I suppose you would also define the logical operators and
>> prove that it's an step-indexed intuitionistic logic?
> 
> No, I'd just define the notion of down-closed predicates, and show that they
> form a COFE.  I'd show that `dist` can be written as one (and maybe validity
> too, for fun's sake).  And that's about all I need to get started.
> 
> Even independent of a proof mode instance this opens all sorts of questions:
> should `dist` be define as one of these? Should `UPred` use this? Should there
> be embeddings to/from the Iris Base Logic?
> For now, I am only interested in what is needed to generalize auth.
> 
> ; Ralf
>