-- Type is universe, the type of types.
-- 1 is the "one" type (a.k.a unit type), which has one instance.
let f1 : Type = 1;

-- .. and 0 is the instance of 1.
let f2 : 1 = 0;