Paths with an interval
Cubical type theories make paths and composition operations explicit using an interval and additional structure. The design of interval operations and Kan composition varies among systems.
Computational accounts of univalence seek rules whose behavior supports normalization or canonicity in the particular calculus. An implementation claim should identify the calculus and the exact metatheorem it relies on.
What to submit
An executable account should include a versioned implementation, the primitive composition operations it uses, and a minimal example illustrating transport along a nontrivial path.
Our scope includes higher inductive types, constructive Kan operations, and categorical models of these rules.
This original editorial primer is not a peer-reviewed manuscript.