instance instDecidableEqULift : {α : Type u_1} → [inst : DecidableEq α] → DecidableEq (ULift α)

Equations

• instDecidableEqULift = decEqULift✝

instance instSubsingletonULift {α : Type u_1} [Subsingleton α] : Subsingleton (ULift α)

Equations

• ⋯ = ⋯