在独立类型理论中有一个相等类型。通常在定义此类型时，会引入一些实用程序，即long和subst。他们的表达能力如何?是否有可能用消除器来表达我们所能表达的与它们平等的一切?
不能，不能只用长、代、消来证明身份证明的唯一性。
uip : {α : Level} {A : Set α} {x y : A} -> (p q : x ≡ y) -> p ≡ q
解释如下:http://homotopytypetheory.org/2011/04/10/just-kidding-understanding-identity-elimination-in-homotopy-type-theory/