What is the role of the Bicolored Calculus of Constructions?
In The Implicit Calculus of Constructions
Extending Pure Type Systems with
an Intersection Type Binder and Subtyping, Alexandre Miquel introduces the basic concepts for the Implicit Calculus of Constructions, which I believe is synonymous with the Bicolored Calculus of Constructions.

The point is (among other things) to have a calculus without the clutter of explicit type annotations everywhere. Type inference is (very likely to be) undecidable though.

In this calculus, if we take $id=\lambda x. x$, then you can derive
$$ \vdash id\colon \forall X\colon Type. X\rightarrow X$$ 
by simply using the explicit product and the implicit product rules in succession. Then the instantiation rule for the implicit product allows
$$ \vdash id\colon Nat\rightarrow Nat $$
and so
$$ \vdash id\ 0 \colon Nat$$
The system admits subject reduction and confluence, even on untyped terms (which in fact fails for calculi with abstraction annotations). All this can be found in Alexandre's thesis, which is sadly in French. Not sure I have a better reference for these results though I'm afraid.