CatDat

contravariant power set functor

This functor PP_{\forall} 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

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.