Univalent Weakly Universal Kan Fibrations in Toposes

Definitions and mathematical statement

Let $\Delta$ be the simplex category, whose objects are the finite ordered sets $[n]=\{0,\ldots,n\}$, for $n\geq 0$, and whose morphisms are order-preserving maps. For a topos $\mathcal E$, its category of simplicial objects is \[ s\mathcal E=\operatorname{Fun}(\Delta^{\mathrm{op}},\mathcal E). \] The supplied question asks:

Does every topos $\mathcal E$ admit a morphism $p:\widetilde U\to U$ in $s\mathcal E$ that is a univalent, weakly universal Kan fibration?

The universal quantifier ranges over toposes, with the fibration allowed to depend on $\mathcal E$. The source does not specify whether "topos" means an elementary topos, a Grothendieck topos, or a class with additional hypotheses.

The terminology requires qualifications that the supplied record does not resolve. A Kan condition concerns lifting against the horn inclusions $\Lambda^k[n]\hookrightarrow\Delta[n]$, for every $n\geq 1$ and $0\leq k\leq n$. For simplicial objects in a general topos, one must specify whether these lifting requirements are internal or external, whether fillers need exist only locally, and whether chosen fillers are part of the structure.

Weak universality requires a specified class $\mathscr K_{\mathcal E}$ of fibrations to be classified and a specified meaning of classification. For example, under classification up to isomorphism by pullback, the requirement would be \[ \forall\,(q:X\to B)\in\mathscr K_{\mathcal E}\quad \exists\,f:B\to U\quad X\cong B\times_U\widetilde U\quad\text{over }B, \] with no uniqueness of $f$ required. This is a conditional interpretation, not a convention established by the supplied source: classification up to homotopy or equivalence may instead be intended. The record gives neither the class $\mathscr K_{\mathcal E}$ nor any size bound on its fibers.

Univalence expresses that the canonical passage from paths between parameters in $U$ to equivalences between the corresponding fibers of $p$ is an equivalence. Turning this description into a mathematical condition requires specified notions of paths, fiber equivalence, and weak equivalence in $s\mathcal E$, together with any required fibrancy assumptions. These are not supplied.

Thus the displayed existence question preserves the source's intended target, but its scope and predicates remain unresolved. A fully specified existence assertion cannot be extracted without settling these conventions; no choice of them is asserted here.

Short English statement

The question asks whether every topos has a simplicial Kan fibration that weakly classifies an intended class of fibrations and satisfies univalence. The source leaves the class being classified, size restrictions, the scope of "topos," and the internal and homotopical conventions unspecified. Its supplied status is "partially solved"; this draft does not independently verify that assessment.

Sources

• Supplied local UnsolvedMath registry record, permanent ID $30001723$, title "Univalent Weakly Universal Kan Fibrations in Toposes," source problem code catalogue entry, in the Oberwolfach Reports Open Problems collection. The record gives the proposed year as 2011 and names no individual proposer.
• Supplied authoritative report citation: Mini-Workshop: The Homotopy Interpretation of Constructive Type Theory (2011), Oberwolfach Reports, pp. 609--638, DOI 10.4171/owr/2011/11. https://doi.org/10.4171/owr/2011/11. The registry labels the statement corrected_verified and reports that the official report confirms the open-session question, with only an extraction label removed. This is supplied verification metadata, not an independent source check for this draft.
• Supplied literature reference labeled "van den Berg--Moerdijk": https://doi.org/10.1007/s00208-017-1614-3.
• Supplied literature reference labeled "Riehl": https://doi.org/10.1112/blms.12997.
• Supplied literature reference labeled "Directed univalence in any infinity-topos": https://arxiv.org/abs/2607.02420.
• Literature assessment dated exactly 2026-08-21: supplied dated curation, not independently verified. It labels the problem partially solved and states that universal univalent Kan fibrations have been constructed for simplicial sets and broad higher-topos settings, while the exact existence claim for simplicial objects in every ordinary topos is not established by the located sources in that full generality. The supplied background describes this as literature triage derived from the OWR curation and requests independent verification of time-sensitive status and cited claims.