sec-homotopy-oudl
9.12 Homotopy-coherent online UDL
The ordinary nerve records strict categorical composition. Learning and repair generally produce a weaker structure: two composites may be related by a specified transformation rather than equality, and those transformations must themselves satisfy higher compatibility. Categorical homotopy theory supplies the language for retaining this coherence while discarding accidental features of a presentation [ Riehl , 2014 ] . The first datum is therefore not a model structure chosen for convenience, but a semantic declaration of which changes preserve decision content.
A homotopical decision target is a relative category \((\mathcal D,W)\), where \(W\) is a declared class of semantic weak equivalences, together with a chosen localization
that admits the required Kan extensions. A morphism belongs to \(W\) only when the declaration says that it preserves the observable decision content; representational similarity alone is insufficient.
A simplicial model category, a category enriched in Kan complexes, or a direct presentation as an \(\infty \)-category can realize this declaration. For a locally Kan simplicial category, its homotopy-coherent nerve replaces strictly unique compositions by coherently compatible spaces of composition. The ordinary nerve \(N\mathcal H\) is recovered when every mapping space is discrete.
Let \(F:\mathcal S\to \mathcal D_\infty \) be a decision decoration, with declared functors \(J:\mathcal S\to \mathcal C\) and \(K:\mathcal C\to \mathcal Q\). Its homotopy-coherent UDL semantics is
where the superscript records Kan extension after localization. In a compatible model presentation this is computed by the corresponding total derived Kan extensions.
A homotopy-coherent online UDL is a functor
whose value at \(t\) is adapted to the information available at \(t\). Persistent homotopy-coherent UDL retains the entire induced functor \(\mathsf U^h\mathbf F:N\mathbb T\to \operatorname {Fun}(\mathcal Q,\mathcal D_\infty )\), including its higher coherence data, rather than only its objects in the homotopy category.
The fixed common domain \(\mathcal S\) in the definition is obtained from growing simplex categories by the extensions used in 9.11. A functor out of \(N\mathbb T\) encodes not only prefix transports but the coherent homotopies relating their composites. Passing immediately to the homotopy category would erase this information.
If \(F,F':\mathcal S\to \mathcal D_\infty \) are related by an objectwise equivalence and the displayed homotopy Kan extensions exist, then
The same statement holds naturally for equivalences of persistent online diagrams.
Left and right Kan extension are functors between the corresponding \(\infty \)-categories of diagrams. Functors preserve equivalences. Applying first \(\operatorname {Lan}^h_J\) and then \(\operatorname {Ran}^h_K\) gives the asserted equivalence; functoriality in \(N\mathbb T\) gives the persistent statement.
This is the homotopical strengthening of online Kan invariance. It identifies strictly different implementations when the declared localization regards them as the same decision semantics, while preserving all higher witnesses of that identification.