[Agda] question about a form of irrelevance elimination

[Peter LeFanu Lumsdaine]

On 15 July 2015 at 21:38, Peter LeFanu Lumsdaine

> <p.l.lumsdaine at gmail.com> wrote:
> > I think this sort of truncation should be consistent, at least with
> > Martin-Löf type theory (…I can’t speak to the rest of Agda’s type system…
> > ^_^ ) since it holds in the simplicial model, if I’m not mistaken.
>

On Wed, Jul 15, 2015 at 10:51 PM, Andrew Pitts <Andrew.Pitts at cl.cam.ac.uk>
 wrote:


> Is there a reference for a semantics for the kind of irrelevance
> annotations that Agda provides, do you know?
>

Not that I know of — my argument above was just for the “judgemental
truncation” discussed in this thread.

–p.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150715/554f6d39/attachment.html