Emily Riehl, Michael Shulman (2017), Higher Structures 1(1):147–224 (2017); arXiv preprint first — ARXIV-1705.07442
Key takeaways
- Adding a directed interval 2 and a separate “shape” layer (the coherent theory of a strict interval) to homotopy type theory yields a synthetic theory of (∞,1)-categories. Segal types, where binary composites are unique up to homotopy, automatically get coherent associativity and unitality, and a dependent Yoneda lemma holds for covariant families. The model is bisimplicial sets, where Segal and Rezk types are (complete) Segal spaces.
Seeded from the abstract and a skim, before the reading in NOTE-069. What follows is what the work says about itself.
The authors propose foundations for synthetic (∞,1)-category theory inside homotopy type theory. They axiomatize a directed interval type, build higher simplices from it, and use these to probe the categorical structure of any type. Segal types have homotopically unique binary composites, which is enough for coherent associativity and unitality in all dimensions. Rezk types additionally identify categorical isomorphisms with type-theoretic identities, a local univalence. Covariant fibrations vary functorially over Segal types and satisfy a dependent Yoneda lemma, a directed analogue of identity elimination. Having an adjoint is shown to be a mere proposition for functors between Rezk types. To manage the bookkeeping, the paper uses a three-layer type theory with shapes (polytopes in directed cubes) and extension types generalising cubical path types. An appendix gives semantics in the Reedy model structure on bisimplicial sets.
Standing in the record
Filed from the survey of 2026-09-25 of work the anthology set aside as out of scope (tier C): 570 seconds of active reading over 2 sessions in the papers-feed tracker. It was filed Deferred, unread. NOTE-069 is the close reading of 2026-09-25, and it placed the work: Active — This is the founding paper of simplicial HoTT, where synthetic (∞,1)-category theory starts. It is worth reading as mathematics by anyone following directed type theory. Its semantics appendix is explicitly a sketch.
When seeded, before the reading in NOTE-069, the entry gave a priority for a deeper reading: medium — It has the highest owner time in the maths half (t=570, n=2) and is the foundational paper for directed HoTT. The skim captures the architecture but none of the proofs.
What the seeding asked a deeper reading to check (NOTE-069 is that reading):
- It is directly paired with c26 (nLab, two-level type theory). This paper names 2LTT as the alternative it rejects, and the nLab page lists “type theory with shapes” under See also. A reading should file them together.
- Later developments to check include the Rzk proof assistant, which implements this simplicial type theory, and the follow-up synthetic ∞-category work. The v5 correction to the proof of 8.13 is noted on the arXiv page.
Access when seeded: arXiv abs page (v1 21 May 2017 through v5 8 Jun 2023; v4 is the final journal version) and full PDF of v5 (78 pp.) read directly: abstract, table of contents, §1 introduction including Remark 1.1 and the section roadmap. The arXiv page lists no DOI. I found the journal record by a Crossref bibliographic search: Higher Structures 1:147–224, issued 2017-12-22, DOI 10.21136/hs.2017.06. That DOI string is taken from Crossref and I did not resolve it.