Code Generation for Higher Inductive Types

TL;DR

This paper introduces a library that leverages Agda's metaprogramming to simplify the encoding of higher inductive types, reducing complexity and potential errors in traditional type theory implementations.

Contribution

The authors develop a metaprogramming-based library in Agda that automates the encoding of higher inductive types, streamlining their use in conventional type theories.

Findings

Reduces manual encoding errors in higher inductive types

Simplifies the specification process with minimal syntax

Enhances practical implementation of higher inductive types

Abstract

Higher inductive types are inductive types that include nontrivial higher-dimensional structure, represented as identifications that are not reflexivity. While work proceeds on type theories with a computational interpretation of univalence and higher inductive types, it is convenient to encode these structures in more traditional type theories with mature implementations. However, these encodings involve a great deal of error-prone additional syntax. We present a library that uses Agda's metaprogramming facilities to automate this process, allowing higher inductive types to be specified with minimal additional syntax.