<div dir="ltr">Perhaps "squashed" since it is essentially the squash from HOTT, i.e. the inhabitants of the type are all equivalent.<br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Aug 16, 2019 at 12:49 PM Ralf Jung <<a href="mailto:jung@mpi-sws.org">jung@mpi-sws.org</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Ah, sorry.  Yes that is a rather unfortunate clash of terminology. ;)<br>
Our S is for "step-indexed".  I don't even know what the "s" in Coq's sprop is<br>
for, do you?<br>
<br>
; Ralf<br>
<br>
On 16.08.19 18:10, Gregory Malecha wrote:<br>
> Ah, that makes more sense. When you said SProp, I thought you meant the new<br>
> sprop Coq feature, not step-indexed propositions.<br>
> <br>
> On Fri, Aug 16, 2019 at 9:58 AM Robbert Krebbers<br>
> <<a href="mailto:mailinglists@robbertkrebbers.nl" target="_blank">mailinglists@robbertkrebbers.nl</a> <mailto:<a href="mailto:mailinglists@robbertkrebbers.nl" target="_blank">mailinglists@robbertkrebbers.nl</a>>> wrote:<br>
> <br>
>     I realized I defined the type sProp in Coq a long time ago already, but<br>
>     never created a merge request for it. I have done that now:<br>
> <br>
>        <a href="https://gitlab.mpi-sws.org/iris/iris/merge_requests/304/diffs" rel="noreferrer" target="_blank">https://gitlab.mpi-sws.org/iris/iris/merge_requests/304/diffs</a><br>
> <br>
>     I propose we continue this discussion there.<br>
> <br>
>     On 16/08/2019 14.30, Ralf Jung wrote:<br>
>     >> By defining SProp, I suppose you would also define the logical operators and<br>
>     >> prove that it's an step-indexed intuitionistic logic?<br>
>     ><br>
>     > No, I'd just define the notion of down-closed predicates, and show that they<br>
>     > form a COFE.  I'd show that `dist` can be written as one (and maybe validity<br>
>     > too, for fun's sake).  And that's about all I need to get started.<br>
>     ><br>
>     > Even independent of a proof mode instance this opens all sorts of questions:<br>
>     > should `dist` be define as one of these? Should `UPred` use this? Should there<br>
>     > be embeddings to/from the Iris Base Logic?<br>
>     > For now, I am only interested in what is needed to generalize auth.<br>
>     ><br>
>     > ; Ralf<br>
>     ><br>
> <br>
> <br>
> <br>
> -- <br>
> gregory malecha<br>
> <a href="mailto:gregory@bedrocksystems.com" target="_blank">gregory@bedrocksystems.com</a> <mailto:<a href="mailto:gregory@bedrocksystems.com" target="_blank">gregory@bedrocksystems.com</a>><br>
> director of formal methods<br>
<br>
-- <br>
Website: <a href="https://people.mpi-sws.org/~jung/" rel="noreferrer" target="_blank">https://people.mpi-sws.org/~jung/</a><br>
</blockquote></div><br clear="all"><br>-- <br><div dir="ltr" class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div>gregory malecha</div><div><a href="mailto:gregory@bedrocksystems.com" target="_blank">gregory@bedrocksystems.com</a></div><div><span>director of formal methods</span></div></div></div></div></div>