(Co)condition hits the Path

Tesla Zhang, Valery Isaev

We propose an enhancement to inductive types and records in a dependent type theory, namely (co)conditions. With a primitive interval type, conditions generalize the cubical syntax…