(Co)condition hits the Path

TL;DR

The paper introduces (co)conditions as an enhancement to inductive types and records in dependent type theory, generalizing cubical syntax and dualizing conditions with coconditions, focusing on type checking without developing full metatheory.

Contribution

It proposes (co)conditions to extend inductive types and records, providing a duality framework and generalizations of cubical syntax in dependent type theory.

Findings

Conditions generalize cubical syntax of higher inductive types

Coconditions generalize cubical path types

Type checking for (co)conditions is presented

Abstract

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 of higher inductive types in homotopy type theory, while coconditions generalize the cubical path type. (Co)conditions are also useful without an interval type. The duality between conditions and coconditions is presented in an interesting way: The elimination principles of inductive types with conditions can be internalized with records with coconditions and vice versa. However, we do not develop the metatheory of conditions and coconditions in this paper. Instead, we only present the type checking.