Example of a preorder that is not a partial order

Length.agda

module Length where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; trans)
open import Data.List using (List; _∷_; []; length)
open import Data.Nat using (ℕ; _≤_; s≤s; z≤n)
open import Data.Product using (∃-syntax; _,_; _×_; -,_)
open import Relation.Nullary using (¬_)

_ℕList≤_ : List ℕ → List ℕ → Set
xs ℕList≤ ys = length xs ≤ length ys

ℕList≤-refl : ∀{xs : List ℕ} → xs ℕList≤ xs
ℕList≤-refl {[]} = z≤n
ℕList≤-refl {x ∷ xs} = s≤s (ℕList≤-refl {xs})

ℕList≤-trans : ∀{xs ys zs : List ℕ} → xs ℕList≤ ys → ys ℕList≤ zs → xs ℕList≤ zs
ℕList≤-trans {x ∷ xs} {x₁ ∷ ys} {x₂ ∷ zs} (s≤s xs≤ys) (s≤s ys≤zs) = s≤s (ℕList≤-trans {xs} {ys} {zs} xs≤ys ys≤zs)
ℕList≤-trans {[]} {[]} {_} _ ys≤zs = ys≤zs
ℕList≤-trans {[]} {_ ∷ _} {_ ∷ _} _ _ = z≤n

not-anti-sym-List≤ : ∃[ m ]( ∃[ n ]( (m ℕList≤ n) × (n ℕList≤ m) × (¬ m ≡ n) ) )
not-anti-sym-List≤ = 1 ∷ [] , (2 ∷ [] , s≤s z≤n , s≤s z≤n , (λ ()))