Open Research Index

Directed univalence for simplicial objects in an $\infty$-topos

Evan Cavallo, Emily Riehl, Christian Sattler

arXivarxiv/2607.02420Jul 2, 2026math.CTscore 0

A fundamental component of homotopy type theory, a synthetic theory of $\infty$-groupoids, is Voevodsky's univalence axiom. Univalence characterizes the identity types in the universal fibration, a classifier for small type families: identity types in the universe are equivalent to types of equivalences. The directed univalence axiom plays a similar foundational role in simplicial type theory, a synthetic theory of $\infty$-categories. In its original form, which does not include universes or directed univalence, the simplicial type theory has semantics in categories of simplicial objects in…

SourceJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/arxiv/2607.02420
curl -X POST /api/v1/records/arxiv/2607.02420/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2607.02420/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'