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}$ $$x:A.C(x) =^{(A, B, p)} y:B.D(y)$$ [[!redirects Sandbox > history]]