[Agda] question about a form of irrelevance elimination

[Peter LeFanu Lumsdaine]

On 14/07/15 14:11, Andrew Pitts wrote:

> > On 14 July 2015 at 13:46, Martin Escardo <m.escardo at cs.bham.ac.uk>
> wrote:
> >> I am a bit nervous about the computational consistency of this
> >> postulate. I think this may imply excluded middle (but I am not sure).
> >
> > If true, that would be annoying, but interesting.
>
> But here you (1) give up the computation rule for truncation, and (2)
> you declare that all elements of the truncation are definitionally
> equal. This sounds very strange, but I can't see any contradiction or
> taboo.


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.

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