Strictification of weakly stable type-theoretic structures using generic contexts

TL;DR

This paper introduces a new method to convert weakly stable type-theoretic structures into strictly stable ones using generic contexts, broadening the applicability of strictification in models of type theory.

Contribution

It generalizes the local universes method by employing categorical generic contexts, enabling strictification in categories with families without definitional equality.

Findings

Generic contexts can be constructed in any category with families supporting first-order unification.

Weakly stable structures can be transformed into strictly stable structures in equivalent models.

The method applies to models with typal equalities, broadening the scope of strictification techniques.

Abstract

We present a new strictification method for type-theoretic structures that are only weakly stable under substitution. Given weakly stable structures over some model of type theory, we construct equivalent strictly stable structures by evaluating the weakly stable structures at generic contexts. These generic contexts are specified using the categorical notion of familial representability. This generalizes the local universes method of Lumsdaine and Warren. We show that generic contexts can also be constructed in any category with families which is freely generated by collections of types and terms, without any definitional equality. This relies on the fact that they support first-order unification. These free models can only be equipped with weak type-theoretic structures, whose computation rules are given by typal equalities. Our main result is that any model of type theory with weakly stable weak type-theoretic structures admits an equivalent model with strictly stable weak type-theoretic structures.