<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>> private<br>
> data #I : Set where<br>
> #0 : #I<br>
> #1 : #I<br>
><br>
> I : Set<br>
> I = #I<br>
><br>
> 0 : I<br>
> 0 = #0<br>
><br>
> 1 : I<br>
> 1 = #1<br>
><br>
> postulate<br>
> seg : Id 0 1<br>
><br>
> I-rec : (P : I -> Set) (x0 : P 0) (x1 : P 1) (p : Id (transport P seg x0) x1) -> ((x : I) -> P x)<br>
> I-rec P x0 x1 p #0 = x0<br>
> I-rec P x0 x1 p #1 = x1<br>
><br>
> -- + propositional reduction rules for [seg]</p>
<p>The point is that the reduction<br>
> I-rec P x0 x1 p 0 --> 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, "I" is reduced to something ugly (and not even syntactically correct) like ".Interval.#I", and with more complicated HIT this is sometimes very annoying (and with HIT with parameters there is another problem, but I don't remember what it is right now)</p>
<p>Is there a workaround for that? Ideally the terms "I", "0" and "1" should never be reduced.</p>
<p>I tried to declare "I" abstract, but obviously the pattern matching defining I-rec does not work anymore.</p>
<p>Thanks,</p>
<p>Guillaume</p>