bifunctor and End homs

Stream: maths

[Yury G. Kudryashov]

Hi, what of the following do we already have in mathlib (no universes for simplicity)?

variables {C D : Type} [category C] [category D] (X : C) (Y : D)
definition n1 : End X × End Y → End (X, Y) := sorry
definition n2 : (End X)ᵒᵖ ≃* End (op X) := sorry
definition n3 : (End (op X) × End Y) →* End (X ⟶ Y) := sorry
definition n4 : ((End X)ᵒᵖ × End Y) →* End (X ⟶ Y) := sorry
definition n5 {M : Type} [monoid M] : (Mᵒᵖ →* End X) → (M →* End Y) → (M → End (X ⟶ Y)) := sorry

Of course, most of these definitions are trivial but I'd prefer to avoid code duplication.