Kata

Prove that the (contravariant) double powerset functor PP is a monad.

Preloaded contains the following:

import category_theory.functor
import category_theory.types
import tactic

universe u

@[simps]
def PP : Type u ⥤ Type u :=
{ obj := λ X, set (set X),
  map := λ X Y f, set.preimage (set.preimage f) }