述語論理において、\(f\)を一変数の関数とすると、\(x_{1}=x_{2}\to f(x_{1})=f(x_{2})\)が成り立つ。これは関数が等しさを保つことを表す。[001F]はこの類似で、型理論において関数は同一視を保つことを表す。