CatDat

covariant power set functor

This functor maps a set XX to its power set P(X)P(X) and a map of sets f:XYf : X \to Y to the induced image operator f:P(X)P(Y)f_* : P(X) \to P(Y).

Satisfied Properties

Assigned properties

Deduced properties

Unsatisfied Properties

Assigned properties

Deduced properties*

*This also uses the deduced satisfied properties.

Unknown properties

Undecidable properties

There is 1 property for which it cannot be decided if it is satisfied or not.