{α : Type u_3} →
  {β : Type u_5} →
    {γ : Type u_7} →
      {l : Type u_9} →
        {m : Type u_10} →
          {n : Type u_11} → {p : Type u_12} → (α → β → γ) → Matrix l m α → Matrix n p β → Matrix (l × n) (m × p) γ