[Iris-Club] Two Monoid Questions

[Gregory Malecha]

Perhaps "squashed" since it is essentially the squash from HOTT, i.e. the
inhabitants of the type are all equivalent.

On Fri, Aug 16, 2019 at 12:49 PM Ralf Jung <jung at mpi-sws.org> wrote:

> Ah, sorry.  Yes that is a rather unfortunate clash of terminology. ;)
> Our S is for "step-indexed".  I don't even know what the "s" in Coq's
> sprop is
> for, do you?
>
> ; Ralf
>
> On 16.08.19 18:10, Gregory Malecha wrote:
> > Ah, that makes more sense. When you said SProp, I thought you meant the
> new
> > sprop Coq feature, not step-indexed propositions.
> >
> > On Fri, Aug 16, 2019 at 9:58 AM Robbert Krebbers
> > <mailinglists at robbertkrebbers.nl <mailto:mailinglists at robbertkrebbers.nl>>
> wrote:
> >
> >     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
> >     >
> >
> >
> >
> > --
> > gregory malecha
> > gregory at bedrocksystems.com <mailto:gregory at bedrocksystems.com>
> > director of formal methods
>
> --
> Website: https://people.mpi-sws.org/~jung/
>


-- 
gregory malecha
gregory at bedrocksystems.com
director of formal methods
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mpi-sws.org/pipermail/iris-club/attachments/20190816/bbfe4c0b/attachment-0001.html>