∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : MulOne M] [inst_1 : MulOne N] [inst_2 : MulOne P] (hnp : N →* P)
  (hmn : M →* N), hnp.comp hmn = { toFun := ⇑hnp ∘ ⇑hmn, map_one' := ⋯, map_mul' := ⋯ }