Strict stability of extension types

TL;DR

This paper demonstrates that extension types in synthetic $( Infty,1)$-categories can be interpreted with strict stability under substitution, using a splitting method based on Voevodsky's approach and extended by Lumsdaine--Warren.

Contribution

It introduces a strict interpretation of extension types in the semantics of synthetic $( Infty,1)$-categories, leveraging the splitting method for stability.

Findings

Extension types are shown to be strictly stable under substitution.

The splitting method is effectively applied to interpret extension types.

The approach generalizes previous methods to achieve strict stability.

Abstract

We show that the extension types occurring in Riehl--Shulman's work on synthetic $(\infty,1)$-categories can be interpreted in the intended semantics in a way so that they are strictly stable under substitution. The splitting method used here is due to Voevodsky in 2009. It was later generalized by Lumsdaine--Warren to the method of local universes.