[Iris-Club] Two Monoid Questions
jung at mpi-sws.org
Fri Aug 16 14:30:28 CEST 2019
> 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.
More information about the Iris-Club