section
variable (A : Type) (B : A → Prop)

def foo := PSigma B

def bar : Type := PSigma B
end