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

Properties from the database

Deduced properties

Unsatisfied Properties

Properties from the database

Deduced properties*

*This also uses the deduced satisfied properties.

Unknown properties

For these properties the database currently doesn't have an answer if they are satisfied or not. Please help to contribute the data!