1 2 3 4 5 6
-- 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;