∀ (I : Type u_1) (J : Type u_2) (K : Type u_3) (L : Type u_4) (R : Type u_5),
  Matrix.comp I J K L R =
    { toFun := fun m ik jl => m ik.1 jl.1 ik.2 jl.2, invFun := fun n i j k l => n (i, k) (j, l), left_inv := ⋯,
      right_inv := ⋯ }