[Iris-Club] Two Monoid Questions

Ralf Jung jung at mpi-sws.org
Fri Aug 16 14:24:53 CEST 2019


My thinking is I would define a new "view" CMRA, and make "auth" an instance of
it.  So it would (have to) support step-indexing.  I would define SProp, but not
need a proof-mode instance or so.

But if that's too annoying, a discrete variant would also be a start.  Should be
enough for the bijection.

; Ralf

On 16.08.19 14:22, Robbert Krebbers wrote:
> On 8/16/19 2:21 PM, Ralf Jung wrote:
>> and I think we could get a decent generalization of auth
>> without a lot of SProp infrastructure.
> 
> In that case I presume you would keep the old auth, and make the new version
> just for the discrete case?

-- 
Website: https://people.mpi-sws.org/~jung/



More information about the Iris-Club mailing list