等号の基本性質

任意の $a,b,c:A$ について、次の型の項が J 規則から構成できる。

1. （対称性）$\mathrm{Id}_A(a,b)\to\mathrm{Id}_A(b,a)$。
2. （推移性）$\mathrm{Id}_A(a,b)\to\mathrm{Id}_A(b,c)\to\mathrm{Id}_A(a,c)$。
3. （輸送）型族 $P(x)$（$x:A$）について $\mathrm{Id}_A(a,b)\to P(a)\to P(b)$。
4. （合同）関数 $f:A\to B$ について $\mathrm{Id}_A(a,b)\to\mathrm{Id}_B(f\,a,f\,b)$。