Pith. sign in

REVIEW 5 minor 3 references

The Leibniz adjunction in homotopy type theory, with an application to simplicial type theory

T0 review · 0 major / 5 minor · reviewed 2026-08-03 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The Segal composition condition forces all higher coherences in directed type theory

desk verdict Solid, machine-checked proof that all inner horn inclusions follow from the Segal condition in simplicial type theory—worth serious referee time. read the letter →

arxiv 2601.21843 v2 pith:XQQKDKZ7 submitted 2026-01-29 math.CT cs.LOmath.LO

Tom de Jong , Nicolai Kraus , Axel Ljungström This is my paper · ORCID
classification math.CTcs.LOmath.LO MSC 03B3818N65
keywords homotopytypetheorysimplicialSegaltypesinneranodynemapsLeibnizadjunctionpushout-productpullback-homorthogonality
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

The paper proves that in homotopy type theory with a postulated interval type, the single requirement that directed morphisms compose — the Segal condition, unique fillers for the basic (2,1)-horn — automatically forces unique fillers for every inner horn in every dimension. This collapses the infinite hierarchy of higher coherences of directed types into one condition, generalizing an earlier result that covered only the 3-dimensional case. The proof is carried out internally, using an adjunction between pushout-product and pullback-hom in the 'wild' category of types, together with a classical retract argument. A machine-checked formalization accompanies the paper, so the combinatorial bookkeeping is verified.

What carries the argument

The pushout-product functor, left adjoint to the pullback-hom, in the wild category of types. The adjunction is proved via the equivalence between the wild category of maps and the wild category of families, a consequence of the univalence axiom; this shifts the work to a setting where the definitions are simpler. The interval type is assumed to form a bounded distributive lattice, and its operations define the retraction r(x,y)_i = x_i ∨ y_1 for i ≤ k and x_i ∧ y_2 for i > k; the lattice laws ensure that r composed with the section s is the identity.

What would settle it

Construct a model of homotopy type theory with an interval that is a bounded distributive lattice but where a type has unique (2,1)-horn fillers yet lacks a unique filler for some inner (n,k)-horn; in particular, test the specific lattice identities x∨(x∧y)=x and x∧(x∨y)=x that make r∘s equal the identity.

Watch

Extended reading notes

Core claim

The central claim is Theorem 4.9: for every n and every inner k, the horn inclusion λⁿₖ is inner anodyne, meaning any Segal type has unique fillers for all inner (n,k)-horns. The proof exhibits λⁿₖ as a retract of the pushout-product λⁿₖ ×̂ λ²₁, then uses the Leibniz adjunction and closure properties of orthogonality to transfer the Segal property from λ²₁ to λⁿₖ. This is an internal version of a classical quasi-category result, obtained in plain homotopy type theory with an interval merely assumed to be a bounded distributive lattice.

Load-bearing premise

The argument assumes the interval type is a bounded distributive lattice satisfying the stated absorption, commutativity, associativity, and distributivity equations; if the lattice laws fail, the retraction r∘s is not provably the identity, and the transfer collapses.

Editorial extensions

If this is right

  • Segal types in this setting satisfy the full inner horn lifting condition, so composition, associativity, and all higher coherences follow from a single axiom.
  • The closure of left-orthogonal maps under pushout-products and retracts becomes a general toolkit for orthogonality arguments in homotopy type theory.
  • The result extends from Segal types to Segal fibrations: any map right orthogonal to the (2,1)-horn inclusion is right orthogonal to every inner horn inclusion.
  • Because the interval needs only a bounded distributive lattice structure, the theorem applies to a wide family of interval types, not just the total order.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The same retract formula might adapt to prove outer horn lifting under additional assumptions on the interval, opening a route to synthetic weak factorization systems.
  • The internal Leibniz adjunction could serve as a foundation for developing quasi-category theory synthetically, such as the theory of (∞,1)-categories, without moving to a two-level type theory.
  • The proof's reliance on distributive lattice laws suggests a testable boundary: if the interval is only a poset or lacks distributivity, the specific retraction no longer composes to the identity, and the theorem may fail.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

0 major / 5 minor

Summary. The paper works in homotopy type theory with a postulated interval type I assumed to be a set equipped with a bounded distributive lattice structure. It develops the Leibniz adjunction for the wild category of types: the pushout-product is left adjoint to the pullback-hom (Theorem 3.16), proved via an equivalence between the wild category of maps and the wild category of families. Using this, it proves Theorem 4.9: every inner horn inclusion λ^n_k is inner anodyne, so that any type with unique fillers for the (2,1)-horn has unique fillers for all inner (n,k)-horns. The proof constructs a retraction of λ^n_k onto λ^n_k b× λ²₁ via the lattice operations and transfers orthogonality using the Leibniz adjunction and closure properties. The results are claimed to be fully formalized in Cubical Agda, with /cog links to the formalization.

Significance. If correct, this is a substantial contribution to simplicial type theory. It internalizes and generalizes Riehl–Shulman's Proposition 5.12 from n=3 to all n, turning a meta-theoretic schema into a single theorem inside HoTT with an internal interval. The proof strategy via the Leibniz adjunction is elegant and the assumptions on the interval are minimal (no totality, no modalities). The formalization is a major strength: the paper pins Agda 2.8.0 and a specific Cubical library commit, and nearly every key statement is linked to a machine-checked proof. No ad-hoc axioms beyond the bounded distributive lattice structure are introduced, and the derivation is parameter-free. The paper should be of significant interest to the HoTT and higher-category communities.

minor comments (5)
  1. [§4.2, definition of ≤] The displayed definition 'x ≤ y (and y ≥ x) for x ∧ y = y' is backwards: in a lattice the standard convention is x ≤ y iff x ∧ y = x (equivalently x ∨ y = y, as the footnote says). The surrounding text and the proof of Theorem 4.9 use the intended order, so this is a presentation typo, but it should be corrected.
  2. [§4.2, displayed equivalence for Λ²₁] The equivalence 'Λ²₁ ≃ Σ(x, y : I). (x = 0) ∨ (y = 1)' appears to have the two sides swapped. With the convention x = x₁, y = x₂, the condition should read (x = 1) ∨ (y = 0). The proof of Theorem 4.9 correctly uses 'y₁ = 1 or y₂ = 0', so the error is local and does not affect the main argument.
  3. [§3.1.2 / Proposition 3.7] In the statement of Proposition 3.7, the first displayed type writes 'Fam((A, B) ⋔ (A′, B′); ...)' where the pushout-product '(A, B) b× (A′, B′)' is clearly intended. This notational slip could confuse readers.
  4. [§4.2, proof of Theorem 4.9] In the final sentence of the proof, 'the codomain ∆ 2 is a set' should read '∆n': the lower horizontal row in diagram (4) has codomain ∆n. The point that the relevant hom types are sets because ∆n is a set is correct, but the symbol is wrong.
  5. [§4.2, proof of Theorem 4.9] The verification that rcod maps into ∆n (in particular the decreasing condition at the seam i = k, k+1) is summarized rather than shown in detail. The argument follows from monotonicity of the lattice operations and the assumptions 0 < k < n, and the /cog formalization covers it; adding one sentence with the lattice identity would improve readability.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the main theorem is derived from an explicit interval-lattice assumption and a constructive retraction argument, not from its conclusion.

full rationale

The paper's central claim (Theorem 4.9: every inner horn inclusion is inner anodyne, so every Segal type has unique fillers for all inner horns) is not obtained by assuming the target result. It is proved by constructing an explicit section–retraction pair s : λⁿₖ → λⁿₖ b× λ²₁ and r : λⁿₖ b× λ²₁ → λⁿₖ, then checking r∘s = id pointwise using the postulated bounded distributive lattice laws on the interval I, e.g. absorption (x∨(x∧y)=x and x∧(x∨y)=x). The bounded-distributive-lattice structure on I is stated as an explicit framework axiom in Section 4.2, not smuggled in or renamed as a prediction; it is an input, not a consequence of the theorem. The cited Riehl–Shulman result [RS17, Proposition 5.12] covers only n=3 and is generalized, so it is not used to force the general statement. The formalization in Cubical Agda, stated in Section 1.3 and referenced throughout via /cog links, provides machine-checked support rather than a self-referential uniqueness import. The only minor textual issue is the displayed definition of ≤ (x∧y = y where the surrounding text intends x∧y = x), which is a typo and does not affect the argument. Remark 4.10's discussion of set-pushouts is explanatory: the retraction is defined out of the type-theoretic pushout directly, so no hidden transfer from set-level pushouts is load-bearing. There are no fitted parameters, no quantity is renamed as a prediction, and no author-specific uniqueness theorem is invoked to forbid alternatives. The derivation is therefore self-contained with respect to the stated assumptions; no circularity score above 0 is warranted.

Assumptions & free parameters 0 free parameters · 7 assumptions · 0 invented entities

No free parameters or fitted constants appear. The only postulated mathematical object is the interval type I, which is listed as an axiom of the framework. The paper introduces no new empirical or physical entities.

assumptions (7)
  • domain assumption Univalence axiom.
    Used to prove the isomorphism between the wild category of maps and the wild category of families (Proposition 3.3, citing Uni13 Theorem 4.8.3). This transfer is central to Theorem 3.16.
  • domain assumption The interval type I is a set with a bounded distributive lattice structure: constants 0,1 and operations ∧,∨ satisfying idempotence, commutativity, associativity, absorption, and distributivity.
    Assumption in §4.2. The definitions of ∆ⁿ, Λⁿₖ and the retraction in Theorem 4.9 use these identities; in particular, absorption makes rcod∘scod = id.
  • standard math Types are closed under pushouts / higher inductive types (joins, pushout-products, pullbacks).
    Needed for the join construction, the pushout-product f b× g, and pullback-hom; available through Cubical Agda's higher inductive types.
  • standard math Distributivity of Π over Σ (type-theoretic axiom of choice, actually a theorem) and contractibility of singletons.
    Used throughout Section 3 and explicitly in the proof of Theorem 3.16; stated in Section 2.
  • standard math Equivalences are closed under retracts (Uni13, Theorem 4.7.4).
    Used in Lemma 4.6 to transfer orthogonality from a map i to a retract j.
  • domain assumption The inclusion of the 1-category of sets into the wild category of types preserves pushouts along embeddings.
    Invoked in Remark 4.10 to reconcile Joyal's set-based retract argument with homotopy pushouts; without it the horn inclusions might not behave as needed.
  • standard math Yoneda lemma for wild categories; wild functors preserve retracts; isomorphisms of proto-wild categories preserve properties that do not mention equations.
    Used in Corollary 3.17 and Lemma 4.6; Remark 3.2 explains the transfer principle.

how reviews work

0 comments
Cite this review

Pith. "Pith review of The Leibniz adjunction in homotopy type theory, with an application to simplicial type theory." pith.science (2026). https://pith.science/paper/XQQKDKZ7

@misc{pith2026260121843,
  author       = {Pith},
  title        = {Pith review of: The Leibniz adjunction in homotopy type theory, with an application to simplicial type theory},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/XQQKDKZ7}},
  note         = {Machine review of arXiv:2601.21843}
}
abstract

Simplicial type theory extends homotopy type theory and equips types with a notion of directed morphisms. A Segal type is defined to be a type in which these directed morphisms can be composed. We show that all higher coherences can be stated and derived if simplicial type theory is taken to be homotopy type theory with a postulated interval type. In technical terms, this means that if a type has unique fillers for $(2,1)$-horns, it has unique fillers for all inner $(n,k)$-horns. This generalizes a result of Riehl and Shulman for the case $n = 3, k \in \{1, 2\}$. Our main technical tool is the Leibniz adjunction: the pushout-product is left adjoint to the pullback-hom in the wild category of types. While this adjunction is well known for ordinary categories, it is much more involved for higher categories, and the fact that it can be proved for the wild category of types (a higher category without stated higher coherences) is non-trivial. We make profitable use of the equivalence between the wild category of maps and that of families. We have formalized the results in Cubical Agda.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

3 extracted references · 1 linked inside Pith

  1. [2006]

    Representing type theories in two- level type theory

    arXiv: math/0607820 [math.AT]. [KdJ25] Nicolai Kraus and Tom de Jong. “Representing type theories in two- level type theory.” In: TYPES 2025 . Available at https://msp.cis. strath . ac . uk / types2025 / abstracts / TYPES2025 _ paper42 . pdf. Glasgow, UK, 2025. 16 REFERENCES [KvR19] Nicolai Kraus and Jakob von Raumer. “Path Spaces of Higher Inductive Type...

    arXiv 2025

  2. [2008]

    Quasi-categories vs Segal spaces

    url: https : / / math . uchicago . edu /~may / PEOPLE / JOYAL / 0newqcategories.pdf. [JT06] Andr´ e Joyal and Myles Tierney. “Quasi-categories vs Segal spaces.”

  3. [2026]

    Formalizing Equivalences Without Tears

    url: https://github.com/agda/cubical. Commit: a6cf6b5. [dJon25] Tom de Jong. “Formalizing Equivalences Without Tears.” In: 30th International Conference on Types for Proofs and Programs (TYPES 2024). Ed. by Rasmus Ejlers Møgelberg and Benno van den Berg. Vol. 336. Leibniz International Proceedings in Informatics (LIPIcs). Schloss Dagstuhl – Leibniz-Zentru...

    arXiv 2024

Pith tools

Reviewed August 3, 2026 · model on record in the stance chip above.