CatDat

contravariant 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 preimage operator f:P(Y)P(X)f^* : P(Y) \to P(X).

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