[Agda] Display of private things (for higher inductive types)
Guillaume Brunerie
guillaume.brunerie at gmail.com
Thu Jul 26 16:07:11 CEST 2012
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
More information about the Agda
mailing list