Reverse function

ReverseFunction.agda

open import Data.List
open import Data.List.Properties
open import Relation.Binary.PropositionalEquality

record ReverseFunction : Set₁ where
  field
    f : ∀ {A} → List A → List A
    rev : ∀ {A} (xs ys : List A) → f (xs ++ ys) ≡ f ys ++ f xs
    sing : ∀ {A} (x : A) → f (x ∷ []) ≡ x ∷ []

reverseF : ReverseFunction
reverseF = record
  { f = reverse
  ; rev = reverse-++-commute
  ; sing = λ x → refl
  }