For CTL I understand the following:
$\square = $ "always"
$\Diamond = $ "eventually"
$ s \models \forall \square \Phi \ $ if for all paths $\pi$ beginning in state $s$ its true that $\Phi$ always holds in $\pi$
$ s \models \exists \square \Phi \ $ if there exists a path $\pi$ beginning in state $s$ such that $\Phi$ always holds in $\pi$
$ s \models \forall \Diamond \Phi \ $ if for all paths $\pi$ beginning in state $s$ its true that $\Phi$ eventually holds in $\pi$
$ s \models \exists \Diamond \Phi \ $ if there exists a path $\pi$ beginning in state $s$ such that $\Phi$ eventually holds in $\pi$
But what happens when you start nesting quantifiers? For example
$s \models \forall \square \forall \Diamond \Phi $
$s \models \exists \square \exists \Diamond \Phi $
$s \models \forall \square \exists \Diamond \Phi $
$s \models \exists \square \forall \Diamond \Phi $
Isn't $s \models \forall \square \forall \Diamond \Phi $ just a superfluous way of writing $ s \models \forall \Diamond \Phi \ $?
Does CTL have any idempotency or absorbtion laws similar to linear temporal logic?
In CTL (or in CTL$^*$) $s \models \forall \Box \forall \Diamond \Phi$ is not equivalent to $s \models \forall \Diamond \Phi$. Consider a structure with exactly one infinite path emanating from $s$ such that the second state along the path is the only one labeled $\Phi$.
Then this structure satisfies $s \models \forall \Diamond \Phi$, but it does not satisfy $s \models \forall \Box \forall \Diamond \Phi$ because the third state of the path fails $\forall \Diamond \Phi$.
It is true that $\forall \Box \forall \Box \Phi$ is equivalent to $\forall \Box \Phi$ (just like in LTL $\Box\Box \Phi$ is equivalent to $\Box \Phi$) but the four formulae you gave have no simpler equivalent formulae.