A Note on the Uniform Kan Condition in Nominal Cubical Sets

TL;DR

This paper clarifies the uniform Kan condition in nominal cubical sets, providing explicit formulations and an analogue of the Yoneda Lemma to better understand uniform Kan fibrations in higher type theory.

Contribution

It offers a detailed, explicit formulation of the uniform Kan condition and introduces an analogue of the Yoneda Lemma for co-sieves in the context of nominal cubical sets.

Findings

Explicit formulation of the uniform Kan condition

An analogue of the Yoneda Lemma for co-sieves

Characterization of uniform Kan fibrations as naturality in additional dimensions

Abstract

Bezem, Coquand, and Huber have recently given a constructively valid model of higher type theory in a category of nominal cubical sets satisfying a novel condition, called the uniform Kan condition (UKC), which generalizes the standard cubical Kan condition (as considered by, for example, Williamson in his survey of combinatorial homotopy theory) to admit phantom "additional" dimensions in open boxes. This note, which represents the authors' attempts to fill in the details of the UKC, is intended for newcomers to the field who may appreciate a more explicit formulation and development of the main ideas. The crux of the exposition is an analogue of the Yoneda Lemma for co-sieves that relates geometric open boxes bijectively to their algebraic counterparts, much as its progenitor for representables relates geometric cubes to their algebraic counterparts in a cubical set. This characterization is used to give a formulation of uniform Kan fibrations in which uniformity emerges as naturality in the additional dimensions.