[Agda] Irrelevance and propositional equality

Andrea Vezzosi sanzhiyan at gmail.com
Wed Aug 3 17:23:54 CEST 2011


On Fri, Jul 29, 2011 at 9:11 PM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> [...]
> So, I think your foot is safe. ;-)
>
> Actually, this looks like a nice combination of experimental features...

On this line of thought, could we have a universe polymorphic trustMe?


-- Andrea


More information about the Agda mailing list