On Fri, Feb 11, 2011 at 11:15 AM, Permjacov Evgeniy <permeakra at gmail.com> wrote: > When I give Agda _→_ as value (for example, as parameter for type > family) I get an error. So, is → a special synthax form Yes, it's an alias for -> and is there any > 'standart' type constructor to be used as replacement ? Not as far as I know. Cheers, -- JP