Nice! I will be happy to remove my NonEmpty types from everywhere. 😁

The only functions I commonly use that are missing are the two constructors:

let make
    : ∀(a : Type) → ∀(head : a) → ∀(tail : List a) → NonEmpty a
    = λ(a : Type) → λ(head : a) → λ(tail : List a) → { head, tail }

let singleton
    : ∀(a : Type) → ∀(head : a) → NonEmpty a
    = λ(a : Type) → λ(head : a) → { head, tail = [] : List a }

which I prefer to use since there is no "sugared" way to construct a NonEmpty list and those functions make one's use of them agnostic to the underlying implementation (e.g. you don't care if it's implemented as { head : a, tail : List a } or { first : a, rest: List a } or { _1 : a, _2 : List a } or something else entirely). Would those make good additions as well or do people prefer just constructing them manually?