[Iris-Club] Two Monoid Questions
Gregory Malecha
gregory at bedrocksystems.com
Fri Aug 16 20:16:43 CEST 2019
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>
More information about the Iris-Club
mailing list