[Agda] Using instance arguments for pointed types

[Guillaume Brunerie]

Hi Matteo,

I’m trying to get rid of the [Ptd] type, in particular I want to be
able to write [Ω^ n Unit] with [Unit] being the actual Unit type (not
a pointed version of it). In your code (and in the current HoTT-Agda
code) it seems that you still cannot apply [Ω^ n] directly to [Unit].

Guillaume

2013/10/2 Matteo Acerbi <matteo.acerbi at gmail.com>:
> Hello Agda list,
>
> maybe this ended up in Guillaume's spam folder, so I'll take the risk
> of posting it here.
>
> Cheers,
> Matteo
>
> ---------- Forwarded message ----------
> From: Matteo Acerbi <matteo.acerbi at gmail.com>
> Date: Wed, Oct 2, 2013 at 12:56 AM
> Subject: Re: [Agda] Using instance arguments for pointed types
> To: Guillaume Brunerie <guillaume.brunerie at gmail.com>
>
> Hello,
>
> your question made me curious and I played a bit with HoTT-Agda:
>
> https://gist.github.com/ma82/66efe89e918820f7f643
>
> If that is not what you were after, just ignore. :-)
>
> Cheers,
> Matteo
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda