Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

(Co)condition hits the Path

Tesla Zhang, Valery Isaev

TL;DR

This paper introduces (co)conditions as an extension to inductive types and records in a dependent type theory, enabling definitional equalities via pattern-based reductions and dual coconditions for records. It leverages a primitive interval type to connect cubical higher inductive types with path types, and demonstrates a type-checking-centric development rather than full metatheory. Key contributions include internalizing elimination principles with coconditions, formalizing core syntax, typing rules, and a confluence-checking algorithm, and illustrating practical constructs such as naturals with infinity and quotients-like identifications. The work offers a bridge between quotients, HITs, and cubical technology, with implementations in Arend and Aya and clear directions for future extensions and metatheory refinement.

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.

(Co)condition hits the Path

TL;DR

This paper introduces (co)conditions as an extension to inductive types and records in a dependent type theory, enabling definitional equalities via pattern-based reductions and dual coconditions for records. It leverages a primitive interval type to connect cubical higher inductive types with path types, and demonstrates a type-checking-centric development rather than full metatheory. Key contributions include internalizing elimination principles with coconditions, formalizing core syntax, typing rules, and a confluence-checking algorithm, and illustrating practical constructs such as naturals with infinity and quotients-like identifications. The work offers a bridge between quotients, HITs, and cubical technology, with implementations in Arend and Aya and clear directions for future extensions and metatheory refinement.

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.
Paper Structure (23 sections, 5 theorems, 19 equations, 6 figures)

This paper contains 23 sections, 5 theorems, 19 equations, 6 figures.

Table of Contents

  1. Introduction
  2. Quotients with definitional equality
  3. Higher inductive types
  4. Programming with conditions
  5. Naturals with infinity
  6. Preservation of definitional equalities
  7. Elimination principles
  8. Records with coconditions.
  9. Path type and HITs.
  10. The interval type $\mathrm{\color{datatype} \mathbb I}$.
  11. The $\mathrm{\mathrm{\color{datatype} Path}}$ type.
  12. $\mathrm{\mathrm{\color{datatype} Path}}$ is a record with coconditions.
  13. Cubical syntax of HITs.
  14. Formalization of (co)conditions
  15. Core language syntax
  16. ...and 8 more sections

Key Result

Lemma 2.3

The $\mathrm{\mathrm{\color{datatype} Path}}$ encoding satisfies the computation $\mathrm{\color{function} J}~P~p~\mathrm{\color{builtin} refl}_x \mapsto p$.

Figures (6)

  • Figure 3.1: Syntax of terms
  • Figure 3.2: Syntax of signature and declarations
  • Figure 3.3: Reduction rules
  • Figure 3.4: Typing rules for types, terms, and conditions
  • Figure 3.5: Well-formedness of signature $\Sigma$
  • ...and 1 more figures

Theorems & Definitions (15)

  • Lemma 2.3: $J\beta$
  • proof
  • Corollary 2.4
  • Remark 3.2
  • Remark 3.3
  • Remark 3.4
  • Lemma 3.5: Ended
  • proof
  • Remark 3.6
  • Remark 3.7
  • ...and 5 more