Homotopy Type Theory Sandbox (Rev #9)

All right, let us get the identity types of type families working…

Given types $A$ and $B$ and an identification $p:A = B$, one can define the heterogeneous identity type between type families $x:A \; \mathrm{type} \vdash C(x) \; \mathrm{type}$ and $y:B \; \mathrm{type} \vdash D(y) \; \mathrm{type}$