述語論理において、$B$を一変数の述語とすると、$x_{1}=x_{2}\to B(x_{1})\to B(x_{2})$が成り立つ。これは等しい対象は述語によって区別できないことを表す。[001C]はこの類似で、型理論においては同一視される要素を型の族では区別できないことを表す。