[Agda] question about a form of irrelevance elimination

[Andrew Pitts]

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.
>
> Precisely: given any fibration of simplicial sets, the inclusion of its
> image (in the old-fashioned 1-categorical sense) is also a fibration; and
> since it’s a monomorphism, any two sections of it are (judgementally) equal.
> Moreover, all this is pseudo-stable under pullback in the base (i.e. stable
> up to iso), so lifts to strictly stable structure in any of the standard
> strictifications, and hence models this type theory.
>
> In SSets, this also admits an elimination principle, with a “propositional
> computation rule”; this is not pseudo-stable, so will not (afaik) lift to
> the Hofmann (right adjoint) strictification, but should lift to the
> universes and local universes strictifications; so this should show that
> this elimination principle for this “judgemental truncation” is also
> consistent.

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

Andy