§ Type formers need not be injective

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

• This shows that we can create type formers which are not injective.
• This means that inductives are indeed special, for us to be able to have that, eg, cons a as = cons b bs implies that a = b /\ b = bs.