<div dir="ltr"><div class="gmail_extra">On 15 July 2015 at 21:38, Peter LeFanu Lumsdaine<br><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
<span class=""><<a href="mailto:p.l.lumsdaine@gmail.com">p.l.lumsdaine@gmail.com</a>> wrote:<br>
> I think this sort of truncation should be consistent, at least with<br>
> Martin-Löf type theory (…I can’t speak to the rest of Agda’s type system…<br>
> ^_^ ) since it holds in the simplicial model, if I’m not mistaken.<br></span></blockquote><div> </div>On Wed, Jul 15, 2015 at 10:51 PM, Andrew Pitts <span dir="ltr"><<a href="mailto:Andrew.Pitts@cl.cam.ac.uk" target="_blank">Andrew.Pitts@cl.cam.ac.uk</a>></span> wrote:<br><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><span class="">
</span>Is there a reference for a semantics for the kind of irrelevance<br>
annotations that Agda provides, do you know?<br></blockquote><div><br></div>Not that I know of — my argument above was just for the “judgemental truncation” discussed in this thread.</div><div class="gmail_quote"><br></div><div class="gmail_quote">–p.<br><div><br></div><div> </div></div></div></div>