{P : Sort u_1} →
  {α : Type u} →
    {β : Type v} →
      {t : Singleton α β} →
        {α' : Type u} →
          {β' : Type v} → {t' : Singleton α' β'} → α = α' → β = β' → t ≍ t' → Singleton.noConfusionType P t t'