[Agda] collections/containers/finite sets

[Dominique Devriese]

> str< : Rel String _
> str< s₁ s₂ = Lex-< _≡_ (λ c₁ c₂ → Data.Char.toNat c₁ < Data.Char.toNat
> c₂) (Data.String.toList s₁) (Data.String.toList s₂)
>
> Is there a slicker way to do it?
> In particular, are there notions of inverse image or relation
> composition in the standard library somewhere?

One immediate improvement is to use the Data.Function._on_ function,
which may count as a notion of relation composition:

str< : Rel String _
str< = Lex-< _≡_ (_<_ on toNat) on toList

Dominique