transpose and identity of vector-matrices in Agda

Transpose.agda

open import Data.Nat

data Vec : ℕ → Set → Set where
  nil : ∀ {A} → Vec 0 A
  cons : ∀ {A n} → A → Vec n A → Vec (suc n) A

record Traversable (F : Set → Set) : Set1 where
  field
    traverse : ∀ {S T : Set} {G : Set → Set} → (S → G T) → F S → G (F T)

open Traversable

postulate
  TraversableVec : ∀ {n} → Traversable (Vec n)
  TraversableId : Traversable (λ x → x)
  TraversableComp : ∀ {F G} → Traversable F → Traversable G → Traversable λ x → F (G x)

idm : ∀ {T m n} → Vec n (Vec m T) → Vec n (Vec m T)
idm {T} {m} {n} v =
  traverse
    (TraversableComp
      -- {λ T → T} {λ T → Vec n (Vec m T)}
      TraversableId
      (TraversableComp TraversableVec TraversableVec))
    {T} {T} {λ x → x}
    (λ x → x) v

trans : ∀ {T m n} → Vec n (Vec m T) → Vec m (Vec n T)
trans {T} {m} {n} v = traverse TraversableVec {Vec _ T} {_} {G = λ T → Vec m T} (λ x → x) v