Two tricks to trivialize higher-indexed families

TL;DR

This paper introduces two techniques to simplify complex higher-indexed families in dependent type theories, making them easier to encode and manipulate within existing type systems.

Contribution

It presents two novel tricks that trivialize higher-indexed families, enabling their encoding with simpler inductive types and universe-based indexing.

Findings

Fording encodes indexed families with index-free inductive types.

Interleaving higher inductive-inductive types into a single family simplifies their structure.

Both methods make complex higher-indexed families more manageable.

Abstract

The conventional general syntax of indexed families in dependent type theories follow the style of "constructors returning a special case", as in Agda, Lean, Idris, Coq, and probably many other systems. Fording is a method to encode indexed families of this style with index-free inductive types and an identity type. There is another trick that merges interleaved higher inductive-inductive types into a single big family of types. It makes use of a small universe as the index to distinguish the original types. In this paper, we show that these two methods can trivialize some very fancy-looking indexed families with higher inductive indices (which we refer to as higher indexed families).