J is singleton contractibility plus transport, definitionally
A somewhat technical result known in the homotopy type theory community is that the identity elimination rule (“J”) is interprovable with the following pair of facts:
- The based path space, \(\Sigma x:A.a=x\), is contractible; and
- Dependent families admit transport, \((x=y) \to C(x) \to C(y)\).
I learned this fact from Steve Awodey, who noticed it in 2009. (It appears as though it may have been independently discovered by several people, including at least Thierry Coquand. Does anyone else have more information?) The HoTT Book proves these facts using J in Lemmas 3.11.8 and 2.3.1, respectively.
I attach a short note proving not only that (1) + (2) implies J, but that definitional computation rules for (1) and (2) allow one to derive the definitional computation rule for J. My note is several months old, but this result has come up several times recently, so I thought I’d post it online: