Agda.Utils.Permutation

data Permutation

class InversePermute a b

Drop (apply) and undrop (abstract)

data Drop a

class DoDrop a

Test data generator

Properties, see Agda.Utils.Permutation.Tests.