Homotopy Type Theory Sandbox (Rev #10, changes)

Showing changes from revision #9 to #10: Added | Removed | Changed

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

Given It doesn’t work! You need types indexed by type families, which we don’t have here.$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}$