instance instDecidableEqPLift {α✝ : Sort u_1} [DecidableEq α✝] : DecidableEq (PLift α✝)

Equations

• instDecidableEqPLift = decEqPLift✝

instance instSubsingletonPLift {α : Sort u_1} [Subsingleton α] : Subsingleton (PLift α)