∀ {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {inst : Semiring R₁} {inst_1 : Semiring R₂} {inst_2 : Semiring R₃}
  {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : outParam (R₁ →+* R₃)} [self : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃],
  σ₂₃.comp σ₁₂ = σ₁₃