[Agda] Re: eta expansion

Francesco Mazzoli f at mazzo.li
Tue Mar 19 21:44:10 CET 2013


Francesco Mazzoli <f <at> mazzo.li> writes:
> ...nothing prevents you from forming types of type...

Here I obviously meant ‘terms of types’.

Francesco



More information about the Agda mailing list