Structure

contravariant power set functor

Notation P∀:Setop→SetP_{\forall}: \Set^{\op} \to \Set Domain dual of the category of setsCodomain category of sets Related P∃P_{\exists} External nLab link
This functor P∀P_{\forall} maps a set XX to its power set P(X)P(X) and a map of sets f:X→Yf : 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 whether it is satisfied.