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

Equations

• instDecidableEqPLift = decEqPLift✝

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

Equations

• ⋯ = ⋯