<div dir="ltr">On 14/07/15 14:11, Andrew Pitts wrote:<br><div class="gmail_extra"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">
> On 14 July 2015 at 13:46, Martin Escardo <<a href="mailto:m.escardo@cs.bham.ac.uk">m.escardo@cs.bham.ac.uk</a>> wrote:<br>
>> I am a bit nervous about the computational consistency of this<br>
>> postulate. I think this may imply excluded middle (but I am not sure).<br>
><br>
> If true, that would be annoying, but interesting.<br></span><br>
But here you (1) give up the computation rule for truncation, and (2)<br>
you declare that all elements of the truncation are definitionally<br>
equal. This sounds very strange, but I can't see any contradiction or<br>
taboo. </blockquote><div><br></div><div>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.</div><div><br></div><div>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.<br></div><div><br></div><div>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.</div><div><br></div><div>–p.</div><div><br></div></div></div></div>