{M : Type u_1} →
  [inst : Monoid M] →
    {σ : M →* M} →
      {motive : MonoidHom.CompTriple.IsId σ → Sort u} →
        (t : MonoidHom.CompTriple.IsId σ) → ((eq_id : σ = MonoidHom.id M) → motive ⋯) → motive t