On 2016-03-04 16:57, wrote: > Agda doesn't permit \lambda as a type constructor! The lambda character, λ, is used for lambda abstractions: λ x → … -- /NAD