A major difference between cubical path types and Martin-Löf identity types is the behaviour of the J rule. In Martin-Löf identity types the J rule holds up to definitional equality, but for cubical path types, the J rule only holds up to a path. Another difference is that transport generally behaves better with cubical path types. Certain rules for the computation of transports in concrete type families hold up to definitional equality for cubical path types, but only up to an identification for Martin-Löf identity types. Rules The rules for (dependent) cubical path types are as follows Formation Introduction Elimination Computation Uniqueness (optional) In addition, there are coercion and composition operations which make the path type behave like an identity type: Coercion: Composition: … Regularity In general, cubical path types in cubical type theory do not satisfy the J rule definitionally. However one could force the J rule to hold definitionally by appending a coercion regularity rule: