## § Type formers need not be injective

abbrev Powerset (X: Type) := X -> Prop -- the powerset of a type is the collection of all subsets.