The univalence axiom in posetal model categories

TL;DR

This paper interprets Voevodsky's Univalence Axiom within posetal model categories, demonstrating that certain posetal locally Cartesian closed categories satisfy a trivial form of the axiom, addressing a question about alternative models.

Contribution

It provides a new interpretation of the Univalence Axiom in the context of posetal model categories and shows these categories can satisfy a trivial version of the axiom.

Findings

Posetal locally Cartesian closed model categories satisfy a trivial form of the Univalence Axiom.

The interpretation is functorial and represented within the category.

Addresses the question of alternative models of the Univalence Axiom.

Abstract

In this note we interpret Voevodsky's Univalence Axiom in the language of (abstract) model categories. We then show that any posetal locally Cartesian closed model category $Qt$ in which the mapping $Hom^{(w)}(Z\times B,C):Qt\longrightarrow Sets$ is functorial in $Z$ and represented in $Qt$ satisfies our homotopy version of the Univalence Axiom, albeit in a rather trivial way. This work was motivated by a question reported in [Ob], asking for a model of the Univalence Axiom not equivalent to the standard one.