  The function id takes as argument a “small” type \(A:U\) and an element \(x\) of type \(A\), and outputs an element of type \(A\). More generally if \(T(A)\) is a type under the assumption \(A:U\), one can form the dependent type