<p>Hello,</p>
<p>As some of you know, the following trick is used in homotopy type theory to have reduction rules for higher inductive types:</p>
<p>&gt; private<br>
&gt;   data #I : Set where<br>
&gt;     #0 : #I<br>
&gt;     #1 : #I<br>
&gt;<br>
&gt; I : Set<br>
&gt; I = #I<br>
&gt;<br>
&gt; 0 : I<br>
&gt; 0 = #0<br>
&gt;<br>
&gt; 1 : I<br>
&gt; 1 = #1<br>
&gt;<br>
&gt; postulate<br>
&gt;   seg : Id 0 1<br>
&gt;<br>
&gt; I-rec : (P : I -&gt; Set) (x0 : P 0) (x1 : P 1) (p : Id (transport P seg x0) x1) -&gt; ((x : I) -&gt; P x)<br>
&gt; I-rec P x0 x1 p #0 = x0<br>
&gt; I-rec P x0 x1 p #1 = x1<br>
&gt;<br>
&gt; -- + propositional reduction rules for [seg]</p>
<p>The point is that the reduction<br>
&gt; I-rec P x0 x1 p 0  --&gt;  x0<br>
is definitional.</p>
<p>Now my problem is that when using C-c C-t or even C-c C-a in a goal involving these definitions, &quot;I&quot; is reduced to something ugly (and not even syntactically correct) like &quot;.Interval.#I&quot;, and with more complicated HIT this is sometimes very annoying (and with HIT with parameters there is another problem, but I don&#39;t remember what it is right now)</p>

<p>Is there a workaround for that? Ideally the terms &quot;I&quot;, &quot;0&quot; and &quot;1&quot; should never be reduced.</p>
<p>I tried to declare &quot;I&quot; abstract, but obviously the pattern matching defining I-rec does not work anymore.</p>
<p>Thanks,</p>
<p>Guillaume</p>