I read https://en.wikipedia.org/wiki/Lambda_cube#Formal_definition and got confused with the relation between CiC and lambda cube. As far as I understand, CiC extends CoC which is a corner of lambda cube, so rules of lambda cube should be satisfied also in Coq.
For instance, it seems coq accepts (＊,＊). Because the type of nat -> nat is Set which is the type of the nat(the right side one).
But it seems Coq does not accept (□,＊). If it does, then the type of Set -> nat has to be Set, not Type. But Coq's answer to Check (Set -> nat) is Type.
Have I misunderstood the description on the wiki page?
Coq does not have a single untypable □, but a hierarchy of typeable ones. (In particular, □:□ is a rough approximation of one of the typing rules.) So, because of these "universes", Coq does not quite fit the setting of the lambda cube.
As for Set -> nat being of type Set, it depends on whether Set is impredicative. By default, it is predicative, so Set -> nat needs to have a type strictly larger than Set itself, i.e., Type. But you can change Set to be impredicative:
$ coqtop -impredicative-set
Welcome to Coq 8.11.1 (April 2020)
Coq < Check (Set -> nat).
Set -> nat
: Set