And in this definition lies the reason of why having a denotational approach in terms of fixed point, be them either least fixed points or greatest fixed points is mathematically very rewarding. We have immediately from this very definition we can extract two reasoning principles: induction and definition by recursion from the least fixed point and co-induction and definition by co-recursion from the greatest fixed point.
And when we instantiate Tarski's fixed-point theorem to the case of sets, here I write hyper-sets, well then in this case we define inductive and co-inductive types. When we restrict attention to the class of binary relations intended as graphs then we define functions by recursion and co-recursion. And when we restrict attention to sets P of x for some set x well what we are doing is that we are essentially focusing on induction and co-induction.
