arxiv: 2604.18668 · v1 · submitted 2026-04-20 · 🧮 math.CT

Recognition: unknown

Fibrations in Directed Type Theory

Benno Lossin

Pith reviewed 2026-05-10 02:48 UTC · model grok-4.3

classification 🧮 math.CT

keywords cocartesian fibrationsdirected type theorysimplicial type theoryLARI adjunctionsinitial sectionsinfinity-categoriesrzk formalization

0 comments

The pith

Cocartesian fibrations are defined in synthetic simplicial type theory and proven closed under key operations via a new equivalence between LARI adjunctions and initial sections.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper works inside the synthetic simplicial type theory of Riehl and Shulman to treat infinity-categories. It supplies a definition of cocartesian fibrations and then proves several closure properties by establishing an equivalence that connects LARI adjunctions to initial sections. All of this is implemented in the rzk proof assistant and contributed to an existing formalization project. A sympathetic reader would care because the result supplies concrete, machine-checked tools for working with directed structures and fibrations inside a type-theoretic foundation for higher categories.

Core claim

We study infinity-categories in the synthetic simplicial type theory developed by Riehl and Shulman. In particular, we define cocartesian fibrations and prove their closure properties using a novel equivalence between LARI adjunctions and initial sections. We formalize our work using the experimental proof assistant rzk and upstream our work to the formalization effort by Riehl et al.

What carries the argument

The novel equivalence between LARI adjunctions and initial sections, which is used to establish the closure properties of the defined cocartesian fibrations.

Load-bearing premise

The synthetic simplicial type theory accurately models the semantics of infinity-categories and the rzk implementation faithfully realizes the paper's definitions and proofs.

What would settle it

A counter-model of infinity-categories in which a cocartesian fibration fails to remain closed under one of the claimed operations, or a type-checking failure discovered in the rzk code for one of the closure proofs.

Figures

Figures reproduced from arXiv: 2604.18668 by Benno Lossin.

**Figure 2.** Figure 2: Decomposition of 𝜕Δ1 ⊗ Λ 2 1 A more complex example is 𝜕Δ1 ⊂ Δ1 and Λ 2 1 ⊂ Δ2 shown in [PITH_FULL_IMAGE:figures/full_fig_p043_2.png] view at source ↗

**Figure 3.** Figure 3: Inner family that we don’t require the base 𝐴 to be Segal. Definition 4.0.1: Right orthogonal family We call a type family 𝐵 : 𝐴 → 𝒰︀ a right orthogonal family with respect to a shape inclusion 𝑌 ⊂ 𝑋 if: is-orthogonal-family𝑌 (𝐵) ≔ ( 𝑎 : 𝑋 → 𝐴 𝑓 : (𝑦 : 𝑌 ) → 𝐵(𝑎(𝑦)) ) → is-contr(⟨(𝑥 : 𝑋) → 𝐵(𝑎(𝑥)) | 𝑌 𝑓 ⟩) holds. This definition essentially says that for every diagram of shape 𝑋 in the base and a diagram o… view at source ↗

**Figure 4.** Figure 4: Proof structure for showing equivalence of initial sections and LARI adjunctions [PITH_FULL_IMAGE:figures/full_fig_p074_4.png] view at source ↗

**Figure 5.** Figure 5: Composition for proof of Theorem 6.1.1. 76 [PITH_FULL_IMAGE:figures/full_fig_p076_5.png] view at source ↗

**Figure 6.** Figure 6: 𝑗-LARI cell condition with 𝑗 : Δ1 ⊂ Λ 2 1 . For the bold maps, we require the dashed map to be unique for any 𝑚, 𝑤, 𝛼 and 𝛽. 82 [PITH_FULL_IMAGE:figures/full_fig_p082_6.png] view at source ↗

read the original abstract

We study $\infty$-categories in the synthetic simplicial type theory developed by Riehl and Shulman. In particular, we define cocartesian fibrations and prove their closure properties using a novel equivalence between LARI adjunctions and initial sections. We formalize our work using the experimental proof assistant rzk and upstream our work to the formalization effort by Riehl et al. In addition to our new work, we also give an introduction to general type theory, homotopy type theory, and the simplicial type theory used by the rest of the thesis.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

Machine-checked cocartesian fibrations in synthetic simplicial type theory via a new equivalence between LARI adjunctions and initial sections.

read the letter

This paper defines cocartesian fibrations in Riehl and Shulman's synthetic simplicial type theory and proves their closure properties by establishing an equivalence between LARI adjunctions and initial sections, which the author treats as new. The definitions and proofs are formalized in rzk and upstreamed to the existing formalization effort, which is the clearest point of value here. The work also includes background sections on general type theory, homotopy type theory, and the simplicial setting, making the technical development more approachable for readers who are not already deep in the area. The formalization supplies independent mechanical checking, which strengthens the internal consistency of the argument and reduces the usual worries about unstated assumptions in synthetic work. The central claim rests on the equivalence being sufficient to handle the closure results, and the stress-test note indicates no visible load-bearing gaps once the code is in place. On the softer side, the novelty of the equivalence would be easier to assess with a direct comparison to prior results on adjunctions or sections in related type-theoretic or categorical settings. The foundational assumption that the synthetic theory models infinity-categories correctly is standard in this line of work but remains an active area of development rather than settled fact. No other issues stand out from the material. This is for researchers already following synthetic homotopy theory, directed type theory, or formalizations of category theory in proof assistants. A reader interested in concrete, verified definitions of fibrations in this framework would get direct use from the definitions and the closure proofs. It deserves a serious referee because the machine-checked component and the focused technical contribution give it enough substance to warrant external review, even if the exposition or literature comparisons need tightening.

Referee Report

0 major / 2 minor

Summary. The paper studies ∞-categories in the synthetic simplicial type theory of Riehl and Shulman. It defines cocartesian fibrations and proves their closure properties via a novel equivalence between LARI adjunctions and initial sections. The results are formalized in rzk and upstreamed to the Riehl et al. formalization effort; the manuscript also supplies introductory material on type theory, homotopy type theory, and simplicial type theory.

Significance. If the central claims hold, the work advances the synthetic treatment of directed ∞-category theory by supplying machine-verified definitions and closure results for cocartesian fibrations, a load-bearing notion. The rzk formalization and upstreaming provide independent mechanical verification, which is a clear strength. The novel LARI–initial-section equivalence may also streamline future synthetic arguments.

minor comments (2)

[Abstract] Abstract: the sentence 'the rest of the thesis' is inconsistent with a standalone arXiv submission; replace with 'the remainder of the paper' or similar.
[Introduction] The introductory sections on ordinary type theory and HoTT are lengthy relative to the novel contribution; consider condensing or moving non-essential background to an appendix.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment of our work on cocartesian fibrations in synthetic simplicial type theory and for recommending acceptance. No major comments were raised in the report.

Circularity Check

0 steps flagged

No significant circularity; derivation self-contained via formalization

full rationale

The paper defines cocartesian fibrations and establishes their closure properties via a novel equivalence between LARI adjunctions and initial sections inside Riehl-Shulman synthetic simplicial type theory. All new definitions and proofs are formalized in the external rzk proof assistant and upstreamed to the Riehl et al. formalization effort, supplying independent machine-checked verification. The work cites prior type theory for background but introduces original content whose internal consistency is externally validated rather than reduced to fitted inputs, self-definitions, or load-bearing self-citations.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the background synthetic simplicial type theory and the correctness of the rzk implementation; no free parameters or new entities are introduced in the abstract.

axioms (1)

domain assumption Synthetic simplicial type theory developed by Riehl and Shulman models ∞-categories
The paper studies ∞-categories inside this theory.

pith-pipeline@v0.9.0 · 5370 in / 1125 out tokens · 42561 ms · 2026-05-10T02:48:46.265457+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

9 extracted references · 5 canonical work pages

[1]

Synthetic Category Theory,

D.-C. Cisinski, B. Cnossen, K. Nguyen, and T. Walde, “Synthetic Category Theory, ” Nov
[2]

Available: https://drive.google.com/file/d/1lKaq7watGGl3xvjqw9qHjm6SDPFJ2- 0o/view

[Online]. Available: https://drive.google.com/file/d/1lKaq7watGGl3xvjqw9qHjm6SDPFJ2- 0o/view. Note: Accessed 27.11.2025

2025
[3]

Land, Introduction to Infinity-Categories , 1st ed

M. Land, Introduction to Infinity-Categories , 1st ed. in Compact Textbooks in Mathematics. Birkhäuser Cham, 2021. [Online]. Available: https://doi.org/10.1007/978-3-030-61524-6

work page doi:10.1007/978-3-030-61524-6 2021
[4]

dependent sum

nLab authors, “dependent sum. ” [Online]. Available: https://ncatlab.org/nlab/show/dependent+ sum. Note: Revision 19
[5]

dependent product

nLab authors, “dependent product. ” [Online]. Available: https://ncatlab.org/nlab/show/ dependent+product. Note: Revision 54
[6]

Directed univalence in simplicial homotopy type theory

D. Gratzer, J. Weinberger, and U. Buchholtz, “Directed univalence in simplicial homotopy type theory. ” [Online]. Available: https://arxiv.org/abs/2407.09146

work page arXiv
[7]

36th Annual

J. Sterling and C. Angiuli, “Normalization for Cubical Type Theory, ” in 2021 36th Annual ACM/ IEEE Symposium on Logic in Computer Science (LICS) , IEEE, June 2021, pp. 1–15. doi: 10.1109/ lics52264.2021.9470719

work page arXiv 2021
[8]

Controlling unfolding in type theory

D. Gratzer, J. Sterling, C. Angiuli, T. Coquand, and L. Birkedal, “Controlling unfolding in type theory. ” [Online]. Available: https://arxiv.org/abs/2210.05420

work page arXiv
[9]

Ambidexterity and Height

S. Carmeli, T. M. Schlank, and L. Yanovski, “Ambidexterity and Height. ” [Online]. Available: https://arxiv.org/abs/2007.13089 96

work page arXiv 2007