<p dir="ltr">Do you also want the same elimination and computation rules as before?<br>
Again, that may be problematic when combined with univalence.</p>
<p dir="ltr">Assuming univalence, the type Contr of small contractible types is a proposition. Hence you can define a map f from the truncation of Bool to Contr sending true to Unit and false to Unit -&gt; Unit.</p>
<p dir="ltr">Then, by the usual computation rule for truncation, you get f | true | = Unit.<br>
But | true | = | false |, hence</p>
<p dir="ltr">  Unit = f | true | = f | false | = Unit -&gt; Unit</p>
<p dir="ltr">(all equalities are definitional here).</p>
<p dir="ltr">It&#39;s not a contradiction yet, but having Unit and Unit -&gt; Unit definitionally equal is already quite strange.</p>
<p dir="ltr">Guillaume</p>
<div class="gmail_quote">On Jun 7, 2013 4:13 PM, &quot;Martin Escardo&quot; &lt;<a href="mailto:m.escardo@cs.bham.ac.uk">m.escardo@cs.bham.ac.uk</a>&gt; wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Summary of discussion:<br>
---------------------<br>
<br>
* primTrustMe doesn&#39;t do what I wanted.<br>
<br>
I wanted to identify all elements of any given type, definitionally, so as to get an Agda implementation of hpropositional truncation that fully computes, by replacing a postulate in Dan&#39;s trick with primTrustMe.<br>

<br>
For my purposes, I will use Dan&#39;s trick, as originally stated by him, with a postulate for identifying all points of || X ||.<br>
<br>
* Advantage (Dan&#39;s original point in <a href="http://homotopytypetheory.org/2011/04/23/running-circles-around-in-your-proof-assistant/" target="_blank">http://homotopytypetheory.org/<u></u>2011/04/23/running-circles-<u></u>around-in-your-proof-<u></u>assistant/</a>): <br>

<br>
    The elimination-rule equation for hpropositional truncation holds<br>
    definitionally rather than just propositionally.<br>
<br>
This is precisely what I need to get my proofs accepted. (And what he and other people needed to get their proofs accepted in the presence of higher-inductive types (HIT&#39;s) for lines, circles, spheres etc.)<br>
<br>
* Disadvantage (again in Dan&#39;s original post):<br>
<br>
     We lose canonicity if we use || - ||, because there is a<br>
     postulate. (And we may gain SegFault if we attempt to fix this by<br>
     using primTrustMe).<br>
<br>
I can live with that, using a postulate as Dan originally did, rather than my failed attempt with primTrustMe, waiting for the computational open problems in univalent foundations to be sorted out. primTrustMe can&#39;t solve them in this particular case, it seems.<br>

<br>
But I have the feeling that it should be trivial to extend Agda with a type constructor for hpropositional truncation so that canonicity is preserved (but primTrustMe doesn&#39;t seem to be the answer).<br>
<br>
Best,<br>
Martin<br>
<br>
<br>
On 07/06/13 13:00, Guillaume Brunerie wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
On Jun 7, 2013 5:40 AM, &quot;Martin Escardo&quot; &lt;<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a><br>
&lt;mailto:<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.<u></u>uk</a>&gt;&gt; wrote:<br>
 &gt;<br>
 &gt;<br>
 &gt;<br>
 &gt; On 06/06/13 19:57, Guillaume Brunerie wrote:<br>
 &gt;&gt;<br>
 &gt;&gt; This is a natural number which should normalise to 0 if you have<br>
 &gt;&gt; canonicity, but it doesn&#39;t, even if you use primTrustMe.<br>
 &gt;&gt; (on the other hand if you *compile* it, then it will compute to 0,<br>
 &gt;<br>
 &gt;<br>
 &gt; It is a bit disturbing that the normalization for type checking is<br>
different from the normalization given by compilation for running terms.<br>
<br>
One difference between normalization and compilation is that when you<br>
run a program you are guaranteed to be in the empty context whereas<br>
normalization also happens in non empty contexts.<br>
<br>
 &gt;&gt; but<br>
 &gt;&gt; combining that with univalence you can easily get a segfault)<br>
 &gt;<br>
 &gt;<br>
 &gt; I want to understand this more precisely, because univalence is<br>
compatible with hpropositional truncation. Perhaps you are just saying<br>
that we cannot have all points of the truncation to be definitionally<br>
equal under univalence: the type checking is right (because it doesn&#39;t<br>
believe me when I ask to be trusted), but the compilation is wrong (for<br>
univalent foundations).<br>
<br>
Univalence is compatible with truncation but not with primTrustMe.<br>
PrimTrustMe is based on the fact that in the empty context the only<br>
proof of equality should be refl, which is not compatible with univalence.<br>
<br>
Here is how I think you can get a segfault using the interval (I haven&#39;t<br>
managed to actually get the segfault because I don&#39;t understand how to<br>
compile an Agda program yet). You can probably adapt it to truncations<br>
if you want.<br>
<br>
Assuming univalence, the types Unit and Unit -&gt; Unit are equivalent.<br>
Hence there is a dependent type over I whose fiber over 0 is Unit and<br>
whose fiber over 1 is Unit -&gt; Unit.<br>
Then you can take the canonical element tt of Unit, transport it along<br>
the path of the interval (so that you get a function of type Unit -&gt;<br>
Unit) and apply it to tt.<br>
What I think will happen if you try to compile it is that the path of<br>
the interval will be compiled to refl, hence the transport is just the<br>
identity so the program will try to apply the &quot;function&quot; tt to the<br>
argument tt, which is obviously problematic.<br>
<br>
 &gt; Anyway, if trustMe does work as a postulate as claimed earlier, why<br>
is it needed/useful at all?<br>
<br>
My impression is that it can be used to get some unsafe coercion between<br>
arbitrary types, like Obj.magic in OCaml.<br>
<br>
Guillaume<br>
<br>
 &gt;&gt; On Jun 6, 2013 3:20 PM, &quot;Martin Escardo&quot; &lt;<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a><br>
&lt;mailto:<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.<u></u>uk</a>&gt;<br>
 &gt;&gt; &lt;mailto:<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.<u></u>uk</a> &lt;mailto:<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.<u></u>uk</a>&gt;&gt;&gt;<br>

wrote:<br>
 &gt;&gt;<br>
 &gt;&gt;<br>
 &gt;&gt;<br>
 &gt;&gt;     On 06/06/13 16:16, Guillaume Brunerie wrote:<br>
 &gt;&gt;<br>
 &gt;&gt;         Are you planning to compile such code?<br>
 &gt;&gt;<br>
 &gt;&gt;<br>
 &gt;&gt;     Not necessarily, but I want to normalize closed terms of e.g.<br>
 &gt;&gt;     natural number type.<br>
 &gt;&gt;<br>
 &gt;&gt;     When I say that I want a definition that computes, I mean that the<br>
 &gt;&gt;     addition of this construction should preserve canonicity (say for<br>
 &gt;&gt;     closed terms of natural number type).<br>
 &gt;&gt;<br>
 &gt;&gt;         It doesn&#39;t really seem safe to me to compile all<br>
 &gt;&gt;         truncation-is-hprop to<br>
 &gt;&gt;         refl, especially when combined with univalence.<br>
 &gt;&gt;         As far as I understand, it only affects the compiler (not the<br>
 &gt;&gt;         normalisation procedure in the type checker), so maybe it&#39;s safe<br>
 &gt;&gt;         if you<br>
 &gt;&gt;         just want to type-check code.<br>
 &gt;&gt;<br>
 &gt;&gt;<br>
 &gt;&gt;     If I wanted to just type check, then postulates would be enough.<br>
 &gt;&gt;<br>
 &gt;&gt;         For the interval, given that the two endpoints are not<br>
 &gt;&gt;         definitionally<br>
 &gt;&gt;         equal, I don&#39;t think there is any difference with the version<br>
 &gt;&gt;         using a<br>
 &gt;&gt;         postulate (unless you compile the code, in which case<br>
strange things<br>
 &gt;&gt;         might happen)<br>
 &gt;&gt;<br>
 &gt;&gt;<br>
 &gt;&gt;     Well, I would be very surprised if it works, because the interval<br>
 &gt;&gt;     gives you functional extensionality, and it would be too easy to get<br>
 &gt;&gt;     that from data abstraction + primTrustMe in such a way that<br>
 &gt;&gt;     canonicity is preserved.<br>
 &gt;&gt;<br>
 &gt;&gt;     Best,<br>
 &gt;&gt;     Martin<br>
 &gt;&gt;<br>
 &gt;&gt;<br>
 &gt;&gt;<br>
 &gt;&gt;         On Jun 6, 2013 8:35 AM, &quot;Martin Escardo&quot;<br>
 &gt;&gt;         &lt;<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a> &lt;mailto:<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.<u></u>uk</a>&gt;<br>
&lt;mailto:<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.<u></u>uk</a> &lt;mailto:<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.<u></u>uk</a>&gt;&gt;<br>
 &gt;&gt;         &lt;mailto:<a href="mailto:m.escardo@cs.bham.ac" target="_blank">m.escardo@cs.bham.ac</a>. &lt;mailto:<a href="mailto:m.escardo@cs.bham.ac" target="_blank">m.escardo@cs.bham.ac</a>.&gt;<u></u>__uk<br>
 &gt;&gt;<br>
 &gt;&gt;         &lt;mailto:<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.<u></u>uk</a><br>
&lt;mailto:<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.<u></u>uk</a>&gt;&gt;&gt;&gt; wrote:<br>
 &gt;&gt;<br>
 &gt;&gt;              Hi Dan,<br>
 &gt;&gt;<br>
 &gt;&gt;              On 05/06/13 17:41, Dan Licata wrote:<br>
 &gt;&gt;<br>
 &gt;&gt;                  As far as I understand it,<br>
 &gt;&gt;                  primTrustMe is a way of asserting an equality, which is<br>
 &gt;&gt;         slightly<br>
 &gt;&gt;                  better<br>
 &gt;&gt;                  than a postulate because when it has type x = x , it<br>
 &gt;&gt;         reduces to<br>
 &gt;&gt;                  refl.<br>
 &gt;&gt;<br>
 &gt;&gt;               &gt; [...]<br>
 &gt;&gt;<br>
 &gt;&gt;                  I would guess that what you&#39;re doing below is OK:  For<br>
 &gt;&gt;         the usual<br>
 &gt;&gt;                  definition of ∥ X ∥ as a higher inductive type,<br>
 &gt;&gt;<br>
 &gt;&gt;                  (x : ∥ X ∥) (p : Id x x) -&gt; Id p refl<br>
 &gt;&gt;<br>
 &gt;&gt;                  will be propositionally true, (∥ X ∥ is an hprop, and<br>
 &gt;&gt;         therefore an<br>
 &gt;&gt;                  hset).<br>
 &gt;&gt;<br>
 &gt;&gt;<br>
 &gt;&gt;              Yes, that&#39;s precisely my intuition. But this intuition<br>
 &gt;&gt;         would work<br>
 &gt;&gt;              for the interval too, because it is an hprop and hence an<br>
 &gt;&gt;         hset, but<br>
 &gt;&gt;              I don&#39;t think this trick would work for the interval. Or<br>
 &gt;&gt;         would it?<br>
 &gt;&gt;<br>
 &gt;&gt;                  Using primTrustMe will strictify certain instances of<br>
 &gt;&gt;         this (the<br>
 &gt;&gt;                  ones where p is constructed by applying<br>
 &gt;&gt;         truncation-is-hprop to<br>
 &gt;&gt;                  definitionally equal arguments) to definitional<br>
 &gt;&gt;         equalities.  Off the<br>
 &gt;&gt;                  top of my head, I don&#39;t see why that would go wrong.<br>
 &gt;&gt;<br>
 &gt;&gt;<br>
 &gt;&gt;              I agree. But it would be nice to hear from those who<br>
 &gt;&gt;         designed and<br>
 &gt;&gt;              implemented the feature.<br>
 &gt;&gt;<br>
 &gt;&gt;                  On the other hand, using primTrustMe to implement the<br>
 &gt;&gt;         circle or<br>
 &gt;&gt;                  something like that would be bad: if loop : Id{S1} base<br>
 &gt;&gt;         base<br>
 &gt;&gt;                  is defined to be primTrustMe, it will reduce to refl.<br>
 &gt;&gt;<br>
 &gt;&gt;<br>
 &gt;&gt;              I agree too.<br>
 &gt;&gt;<br>
 &gt;&gt;              Best,<br>
 &gt;&gt;              Martin<br>
 &gt;&gt;<br>
 &gt;&gt;<br>
 &gt;&gt;                  -Dan<br>
 &gt;&gt;<br>
 &gt;&gt;                  On Jun05, Martin Escardo wrote:<br>
 &gt;&gt;<br>
 &gt;&gt;<br>
 &gt;&gt;                      On 05/06/13 03:12, Guillaume Brunerie wrote:<br>
 &gt;&gt;<br>
 &gt;&gt;                          I’m not sure I understand what you are trying<br>
 &gt;&gt;         to do.<br>
 &gt;&gt;<br>
 &gt;&gt;<br>
 &gt;&gt;                      I am trying to use an unsound Agda feature to<br>
 &gt;&gt;         implement a sound<br>
 &gt;&gt;                      construction (hpropositional reflection or<br>
truncation).<br>
 &gt;&gt;<br>
 &gt;&gt;                          I don’t really know what primTrustMe is,<br>
 &gt;&gt;<br>
 &gt;&gt;<br>
 &gt;&gt;                      Me neither, and this is why I asked the question<br>
 &gt;&gt;         here. The<br>
 &gt;&gt;                      documentation<br>
 &gt;&gt; <a href="http://code.haskell.org/Agda/____doc/release-notes/2-2-6.txt" target="_blank">http://code.haskell.org/Agda/_<u></u>___doc/release-notes/2-2-6.txt</a><br>
 &gt;&gt;         &lt;<a href="http://code.haskell.org/Agda/__doc/release-notes/2-2-6.txt" target="_blank">http://code.haskell.org/Agda/<u></u>__doc/release-notes/2-2-6.txt</a>&gt;<br>
 &gt;&gt;<br>
 &gt;&gt;<br>
 &gt;&gt;         &lt;<a href="http://code.haskell.org/Agda/__doc/release-notes/2-2-6.txt" target="_blank">http://code.haskell.org/Agda/<u></u>__doc/release-notes/2-2-6.txt</a><br>
 &gt;&gt;         &lt;<a href="http://code.haskell.org/Agda/doc/release-notes/2-2-6.txt" target="_blank">http://code.haskell.org/Agda/<u></u>doc/release-notes/2-2-6.txt</a>&gt;&gt;<br>
 &gt;&gt;                      says:<br>
 &gt;&gt;<br>
 &gt;&gt;                          &quot;Note that the compiler replaces all uses of<br>
 &gt;&gt;         primTrustMe<br>
 &gt;&gt;                      with the<br>
 &gt;&gt;                          REFL builtin, without any check for<br>
definitional<br>
 &gt;&gt;                      equality. Incorrect<br>
 &gt;&gt;                          uses of primTrustMe can potentially lead to<br>
 &gt;&gt;         segfaults or<br>
 &gt;&gt;                      similar<br>
 &gt;&gt;                          problems.&quot;<br>
 &gt;&gt;<br>
 &gt;&gt;                      However, It Doesn&#39;t say what the correct uses are<br>
 &gt;&gt;         meant to be.<br>
 &gt;&gt;<br>
 &gt;&gt;                          but it seems to be some kind of postulate that<br>
 &gt;&gt;         every<br>
 &gt;&gt;                          type is an<br>
 &gt;&gt;                          hprop, which seems much worse than just<br>
 &gt;&gt;         postulating that<br>
 &gt;&gt;                          a single<br>
 &gt;&gt;                          type is an hprop.<br>
 &gt;&gt;<br>
 &gt;&gt;<br>
 &gt;&gt;                      Yes, but notice that I use it privately,<br>
hopefully in a<br>
 &gt;&gt;                      sound way.<br>
 &gt;&gt;<br>
 &gt;&gt;                          What are you trying to achieve exactly?<br>
 &gt;&gt;<br>
 &gt;&gt;<br>
 &gt;&gt;                      I am trying to (soundly) implement hpropositional<br>
 &gt;&gt;         truncation<br>
 &gt;&gt;                      that<br>
 &gt;&gt;                      computes, without *any* postulate at all.<br>
 &gt;&gt;<br>
 &gt;&gt;                      Voevodsky&#39;s Coq implementation uses<br>
type-in-type (also<br>
 &gt;&gt;                      unsound in<br>
 &gt;&gt;                      general, but backed by sound resizing axioms in<br>
 &gt;&gt;         this case) and<br>
 &gt;&gt;                      additionally postulates the axiom of function<br>
 &gt;&gt;         extensionality<br>
 &gt;&gt;                      to show<br>
 &gt;&gt;                      that the truncation really is an hproposition.<br>
 &gt;&gt;<br>
 &gt;&gt;                      Here is an improved version of what I sent<br>
 &gt;&gt;         yesterday, with more<br>
 &gt;&gt;                      explanations, and the main question repeated.<br>
 &gt;&gt;<br>
 &gt;&gt;                      Best,<br>
 &gt;&gt;                      Martin<br>
 &gt;&gt;<br>
 &gt;&gt;<br>
------------------------------<u></u>____--------------------------<u></u>--__--__-------<br>
 &gt;&gt;<br>
 &gt;&gt;                      Here is what we want to achieve:<br>
 &gt;&gt;<br>
 &gt;&gt;                      Given a type X, we want to construct a type ∥ X ∥:<br>
 &gt;&gt;<br>
 &gt;&gt;                                   X type<br>
 &gt;&gt;                                 ----------<br>
 &gt;&gt;                                  ∥ X ∥ type<br>
 &gt;&gt;<br>
 &gt;&gt;                      We want any two elements of ∥ X ∥ to be<br>
propositionally<br>
 &gt;&gt;                      equal, written<br>
 &gt;&gt;                      hprop ∥ X ∥.<br>
 &gt;&gt;<br>
 &gt;&gt;                      We have the introduction rule:<br>
 &gt;&gt;<br>
 &gt;&gt;                                       x : X<br>
 &gt;&gt;                                  ---------------<br>
 &gt;&gt;                                    ∣ x ∣ :  ∥ X ∥<br>
 &gt;&gt;<br>
 &gt;&gt;                      The elimination rule or induction principle, for<br>
 &gt;&gt;         any P : ∥ X<br>
 &gt;&gt;                      ∥ → Set:<br>
 &gt;&gt;<br>
 &gt;&gt;                             g : (h : ∥ X ∥) → hprop(P h)  f : ((x : X) →<br>
 &gt;&gt;         P ∣ x ∣)<br>
 &gt;&gt;<br>
 &gt;&gt;           ------------------------------<u></u>____------------------------<br>
 &gt;&gt;<br>
 &gt;&gt;                                   elim g f : (h : ∥ X ∥) → P h<br>
 &gt;&gt;<br>
 &gt;&gt;                      The computation rule:<br>
 &gt;&gt;<br>
 &gt;&gt;                             elim g f ∣ x ∣ = f x<br>
 &gt;&gt;<br>
 &gt;&gt;                      Thus this is a bracket type that allows us to get<br>
 &gt;&gt;         out of it,<br>
 &gt;&gt;                      provided<br>
 &gt;&gt;                      the target has at most one element (is an<br>
 &gt;&gt;         hproposition).<br>
 &gt;&gt;<br>
 &gt;&gt;                      Here is the tentative implementation:<br>
 &gt;&gt;<br>
 &gt;&gt;                      \begin{code}<br>
 &gt;&gt;<br>
 &gt;&gt;                      module hpropositionalTruncationTentat<u></u>____ive where<br>
 &gt;&gt;<br>
 &gt;&gt;<br>
 &gt;&gt;                      private<br>
 &gt;&gt;                         postulate Level : Set<br>
 &gt;&gt;                         postulate zero : Level<br>
 &gt;&gt;                         postulate suc  : Level → Level<br>
 &gt;&gt;<br>
 &gt;&gt;                      {-# BUILTIN LEVEL     Level #-}<br>
 &gt;&gt;                      {-# BUILTIN LEVELZERO zero  #-}<br>
 &gt;&gt;                      {-# BUILTIN LEVELSUC  suc   #-}<br>
 &gt;&gt;<br>
 &gt;&gt;                      data _≡_ {ℓ} {X : Set ℓ} (x : X) : X → Set ℓ where<br>
 &gt;&gt;                          refl : x ≡ x<br>
 &gt;&gt;<br>
 &gt;&gt;                      {-# BUILTIN EQUALITY _≡_  #-}<br>
 &gt;&gt;                      {-# BUILTIN REFL     refl #-}<br>
 &gt;&gt;<br>
 &gt;&gt;                      \end{code}<br>
 &gt;&gt;<br>
 &gt;&gt;                      This is unsound, but we try to use it to perform a<br>
 &gt;&gt;         sound<br>
 &gt;&gt;                      construction:<br>
 &gt;&gt;<br>
 &gt;&gt;                      \begin{code}<br>
 &gt;&gt;<br>
 &gt;&gt;                      private<br>
 &gt;&gt;                         primitive<br>
 &gt;&gt;                           primTrustMe : ∀{ℓ} {X : Set ℓ} {x y : X} →<br>
x ≡ y<br>
 &gt;&gt;<br>
 &gt;&gt;                      \end{code}<br>
 &gt;&gt;<br>
 &gt;&gt;                      Notice that we keep the above private to the<br>
 &gt;&gt;         module, so that the<br>
 &gt;&gt;                      unsoundness doesn&#39;t leak to modules that use this<br>
 &gt;&gt;         module but no<br>
 &gt;&gt;                      unsound Agda features.<br>
 &gt;&gt;<br>
 &gt;&gt;                      The first part is Dan Licata&#39;s trick. We<br>
implement the<br>
 &gt;&gt;                      hpropositional<br>
 &gt;&gt;                      truncation of ∥ X ∥ as X itself, or rather its<br>
 &gt;&gt;         isomorphic<br>
 &gt;&gt;                      copy ∥ X<br>
 &gt;&gt;                      ∥&#39;,<br>
 &gt;&gt;                      which is kept private to the module:<br>
 &gt;&gt;<br>
 &gt;&gt;                      \begin{code}<br>
 &gt;&gt;<br>
 &gt;&gt;                      private<br>
 &gt;&gt;                          data ∥_∥&#39; (X : Set) : Set where<br>
 &gt;&gt;                            ∣_∣&#39; : X → ∥ X ∥&#39;<br>
 &gt;&gt;<br>
 &gt;&gt;                      ∥_∥ : Set → Set<br>
 &gt;&gt;                      ∥_∥ = ∥_∥&#39;<br>
 &gt;&gt;<br>
 &gt;&gt;                      ∣_∣ : {X : Set} → X → ∥ X ∥<br>
 &gt;&gt;                      ∣_∣ = ∣_∣&#39;<br>
 &gt;&gt;<br>
 &gt;&gt;                      hprop : Set → Set<br>
 &gt;&gt;                      hprop X = (x y : X) → x ≡ y<br>
 &gt;&gt;<br>
 &gt;&gt;                      truncation-rec : {X P : Set} → hprop P → (X → P) →<br>
 &gt;&gt;         ∥ X ∥ → P<br>
 &gt;&gt;                      truncation-rec _ f ∣ x ∣&#39; = f x<br>
 &gt;&gt;<br>
 &gt;&gt;                      truncation-ind : {X : Set} {P : ∥ X ∥ → Set} → ((h<br>
 &gt;&gt;         : ∥ X ∥)<br>
 &gt;&gt;                                       → hprop(P h)) → ((x : X) → P ∣ x<br>
 &gt;&gt;         ∣) → (h : ∥ X<br>
 &gt;&gt;                      ∥) → P h<br>
 &gt;&gt;                      truncation-ind _ f ∣ x ∣&#39; = f x<br>
 &gt;&gt;<br>
 &gt;&gt;                      \end{code}<br>
 &gt;&gt;<br>
 &gt;&gt;                      The above -rec and -ind are the non-dependent and<br>
 &gt;&gt;         dependent<br>
 &gt;&gt;                      elimination rules respectively.<br>
 &gt;&gt;<br>
 &gt;&gt;                      The crucial requirement is that ∥ X ∥ is to be an<br>
 &gt;&gt;                      hproposition. We can<br>
 &gt;&gt;                      achieve this with a postulate, but postulates don&#39;t<br>
 &gt;&gt;         compute.<br>
 &gt;&gt;                      To try to<br>
 &gt;&gt;                      get an implementation that fully computes, we<br>
 &gt;&gt;         privately use<br>
 &gt;&gt;                      the above<br>
 &gt;&gt;                      generally unsound feature:<br>
 &gt;&gt;<br>
 &gt;&gt;                      \begin{code}<br>
 &gt;&gt;<br>
 &gt;&gt;                      truncation-is-hprop : {X : Set} → hprop ∥ X ∥<br>
 &gt;&gt;                      truncation-is-hprop _ _ = primTrustMe<br>
 &gt;&gt;<br>
 &gt;&gt;                      \end{code}<br>
 &gt;&gt;<br>
 &gt;&gt;                      Is that sound? The semantics of primTrustMe is not<br>
 &gt;&gt;         clearly<br>
 &gt;&gt;                      given in<br>
 &gt;&gt;                      the documentation.<br>
 &gt;&gt;<br>
 &gt;&gt;                      NB. Of course, we can make one parameter of the<br>
 &gt;&gt;         elimination rule<br>
 &gt;&gt;                      computationally irrelevant:<br>
 &gt;&gt;<br>
 &gt;&gt;                      \begin{code}<br>
 &gt;&gt;<br>
 &gt;&gt;                      Truncation-elim&#39; : {X P : Set} → .(hprop P) → (X →<br>
 &gt;&gt;         P) → ∥ X ∥<br>
 &gt;&gt;                      → P<br>
 &gt;&gt;                      Truncation-elim&#39; _ f ∣ x ∣&#39; = f x<br>
 &gt;&gt;<br>
 &gt;&gt;                      Truncation-elim : {X : Set} {P : ∥ X ∥ → Set} →<br>
 &gt;&gt;         .((h : ∥ X ∥)<br>
 &gt;&gt;                      → hprop(P h)) → ((x : X) → P ∣ x ∣) → (h : ∥ X<br>
∥) → P h<br>
 &gt;&gt;                      Truncation-elim _ f ∣ x ∣&#39; = f x<br>
 &gt;&gt;<br>
 &gt;&gt;                      \end{code}<br>
 &gt;&gt;                      ______________________________<u></u>_____________________<br>
 &gt;&gt;<br>
 &gt;&gt;                      Agda mailing list<br>
 &gt;&gt; <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a> &lt;mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><u></u>&gt;<br>
&lt;mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a> &lt;mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><u></u>&gt;&gt;<br>
 &gt;&gt;         &lt;mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
&lt;mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><u></u>&gt; &lt;mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
&lt;mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><u></u>&gt;&gt;__&gt;<br>
 &gt;&gt; <a href="https://lists.chalmers.se/____mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/____<u></u>mailman/listinfo/agda</a><br>
 &gt;&gt;         &lt;<a href="https://lists.chalmers.se/__mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/__<u></u>mailman/listinfo/agda</a>&gt;<br>
 &gt;&gt;                      &lt;<a href="https://lists.chalmers.se/__mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/__<u></u>mailman/listinfo/agda</a><br>
 &gt;&gt;         &lt;<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a>&gt;&gt;<br>
 &gt;&gt;<br>
 &gt;&gt;<br>
 &gt;&gt;              ______________________________<u></u>_____________________<br>
 &gt;&gt;<br>
 &gt;&gt;              Agda mailing list<br>
 &gt;&gt; <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a> &lt;mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><u></u>&gt;<br>
&lt;mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a> &lt;mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><u></u>&gt;&gt;<br>
 &gt;&gt;         &lt;mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
&lt;mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><u></u>&gt; &lt;mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
&lt;mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><u></u>&gt;&gt;__&gt;<br>
 &gt;&gt; <a href="https://lists.chalmers.se/____mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/____<u></u>mailman/listinfo/agda</a><br>
 &gt;&gt;         &lt;<a href="https://lists.chalmers.se/__mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/__<u></u>mailman/listinfo/agda</a>&gt;<br>
 &gt;&gt;<br>
 &gt;&gt;              &lt;<a href="https://lists.chalmers.se/__mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/__<u></u>mailman/listinfo/agda</a><br>
 &gt;&gt;         &lt;<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a>&gt;&gt;<br>
 &gt;&gt;<br>
 &gt;&gt;     ______________________________<u></u>___________________<br>
 &gt;&gt;     Agda mailing list<br>
 &gt;&gt; <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a> &lt;mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><u></u>&gt;<br>
&lt;mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a> &lt;mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><u></u>&gt;&gt;<br>
 &gt;&gt; <a href="https://lists.chalmers.se/__mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/__<u></u>mailman/listinfo/agda</a><br>
 &gt;&gt;     &lt;<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a>&gt;<br>
 &gt;&gt;<br>
 &gt; ______________________________<u></u>_________________<br>
 &gt; Agda mailing list<br>
 &gt; <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a> &lt;mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><u></u>&gt;<br>
 &gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
<br>
</blockquote>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
</blockquote></div>