	The remarkable aspect of this is that the latter diagram is one of the various (equivalent) definitions of when two functors are adjoint. Our "F" easily extends to a functor Set → BA, and our definition of "X" generating a free Boolean algebra "FX" is precisely that "U" has a left adjoint "F".