{κ : Type w} →
  (A : Type u) →
    {B : Type v} →
      (C : Type z) →
        [inst : CommRing A] →
          [inst_1 : CommRing B] →
            [inst_2 : Algebra A B] → [inst_3 : CommRing C] → [inst_4 : Algebra A C] → (κ → B) → Matrix κ (B →ₐ[A] C) C