[Agda] Display of private things (for higher inductive types)

[Guillaume Brunerie]

Hello,

As some of you know, the following trick is used in homotopy type theory to
have reduction rules for higher inductive types:

> private
>   data #I : Set where
>     #0 : #I
>     #1 : #I
>
> I : Set
> I = #I
>
> 0 : I
> 0 = #0
>
> 1 : I
> 1 = #1
>
> postulate
>   seg : Id 0 1
>
> I-rec : (P : I -> Set) (x0 : P 0) (x1 : P 1) (p : Id (transport P seg x0)
x1) -> ((x : I) -> P x)
> I-rec P x0 x1 p #0 = x0
> I-rec P x0 x1 p #1 = x1
>
> -- + propositional reduction rules for [seg]

The point is that the reduction
> I-rec P x0 x1 p 0  -->  x0
is definitional.

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)

Is there a workaround for that? Ideally the terms "I", "0" and "1" should
never be reduced.

I tried to declare "I" abstract, but obviously the pattern matching
defining I-rec does not work anymore.

Thanks,

Guillaume
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120726/e91207f2/attachment.html