[Agda] Irrelevance and propositional equality

Andrea Vezzosi sanzhiyan at gmail.com
Tue Aug 9 19:35:20 CEST 2011


On Tue, Aug 9, 2011 at 2:35 PM, Nils Anders Danielsson <nad at chalmers.se> wrote:
> On 2011-08-03 17:23, Andrea Vezzosi wrote:
>>
>> On this line of thought, could we have a universe polymorphic trustMe?
>
> Yes.

Great!

-- Andrea

> --
> /NAD
>


More information about the Agda mailing list