Pith. sign in

REVIEW 5 major objections 5 minor 4 references

On combinatorial aspects of fat Delta

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

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

Pith's one-line read Three face classes and six relations generate fat Delta uniquely

desk verdict New and plausible presentation of fat Delta, but the submitted proof has self-referential citations and unverified crossed relations that need referee attention. read the letter →

arxiv 2506.01717 v1 pith:Z23F44SJ submitted 2025-06-02 math.CT

Stiéphen Pradal This is my paper
classification math.CT MSC 18A3218G30
keywords fatDeltasimplexcategoryweakdegeneraciesgeneratorsandrelationsfacemapsternaryfactorisationsystemrelativesemiordinalshighercategories
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

This paper gives a finite presentation of the category fat $\Delta$, a variant of the simplex category in which degeneracies behave weakly rather than as identities. It isolates three classes of morphisms — degenerated faces, vertical faces, and standard faces — and six relations among them, and proves that every morphism of fat $\Delta$ factors uniquely, up to those relations, as a composition of the three face types. If correct, this makes fat $\Delta$ as tractable as the ordinary simplex category, whose faces and degeneracies generate all maps and satisfy the simplicial identities. The presentation also recovers the ternary factorisation system on fat $\Delta$ as a corollary.

What carries the argument

The central object is the face factorisation of morphisms in fat $\Delta$, whose objects are epimorphisms $\eta\colon[m]\twoheadrightarrow[n]$ of the simplex category and whose morphisms are commutative squares of epimorphisms and monomorphisms. The generators are three types of squares: degenerated faces $s_i$, vertical faces $v_i$, and standard faces $d_i$; a fourth derived composite, the bordering extension $w^\epsilon_i = s_i d_{i+\epsilon}$, is used in the reordering machinery. The proof of Theorem 3.23 works by first splitting the bottom arrow of a morphism into an epimorphism followed by a monomorphism, then decomposing vertical and horizontal morphisms into face blocks using pullbacks and pushouts, and finally proving uniqueness by induction in which a single face is commuted through an already-normal form using relations (6)–(11) and their consequences for bordering extensions.

What would settle it

Compute both sides of each of relations (9)–(11) as actual morphisms in fat $\Delta$ on a small object such as $\eta:[2]\twoheadrightarrow[1]$; any mismatch refutes the presentation. A stronger quantitative check is to compare the hom-sets of fat $\Delta$ with those of the free category on the three face generators modulo relations (6)–(11) for all objects $[m]\twoheadrightarrow[n]$ with $m,n\le 3$; a single cardinality mismatch would refute Theorem 3.23.

Watch

Extended reading notes

Core claim

The central claim is Theorem 3.23: every map in fat $\Delta$ factors uniquely, up to the six relations (6)–(11), as a composition of degenerated faces, vertical faces, and standard faces. The three face classes are the fat-$\Delta$ analogues of simplicial degeneracies and faces: degenerated faces mark a previously unmarked edge, vertical faces insert an inner marked vertex into a marked edge, and standard faces insert a new standard vertex into an unmarked edge. The six relations govern self-interactions and crossed interactions between the classes, with the delicate cases handled by the derived bordering extensions $w^\epsilon_i$ that appear when a degenerated face meets a standard face. The result gives an explicit presentation of fat $\Delta$ by generators and relations, and recovers the ternary factorisation system as a corollary.

Load-bearing premise

The uniqueness theorem depends on the six crossed relations between the face classes being exactly the right identities, and on a borrowed splitting lemma that decomposes a horizontal morphism into a horizontal part followed by a vertical part; as written, two of the proof lemmas (Lemma 3.17 and Lemma 3.22) also cite themselves, so the induction is circular unless those citations are read as shorthand for the same induction.

Editorial extensions

If this is right

  • Every morphism of fat Delta has a normal form as a composition of degenerated, vertical, and standard faces, unique up to the six relations.
  • The ternary factorisation system $(D,V,H)$ on fat Delta follows directly from the unique factorisation theorem.
  • The presentation lifts the simplicial identities to the weak-degeneracy setting, giving fat Delta a combinatorial description comparable to the simplex category.
  • Questions about equality of morphisms in fat Delta can be decided by manipulating the six relations rather than by computing in relative semiordinals.
  • The machinery gives a concrete route for using fat Delta in simplicial, nerve, and Segal-style constructions where weak identities are needed.

Reading between the lines

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

  • Because the presentation is finite, one could encode the three face types and six relations as a rewrite system; a terminating and confluent such system would provide a true normal-form algorithm, a step the paper does not take.
  • The same three-face decomposition may adapt to the closely related direct-category variant of fat Delta used in type-theoretic work, since the two categories share objects; the paper does not address that variant.
  • The derived bordering extensions $w^\epsilon_i$ behave like composites of a degeneracy with a face at the boundary of a marked fibre, and they may deserve independent study as the fat-Delta shadow of source and target structure for weak identities.
  • The finite, explicit nature of the presentation makes Theorem 3.23 a plausible target for full formalisation in a proof assistant, which would also settle whether the self-referential citations in two of the uniqueness lemmas are harmless shorthand.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

5 major / 5 minor

Summary. The paper develops a generators-and-relations presentation of Kock's fat Delta category. It defines three classes of face morphisms in fat Delta -- degenerated faces, vertical faces, and standard faces -- and proposes six relations (6)--(11) among them. The main results are Theorem 3.18, asserting that every morphism of fat Delta factors as a composition of these faces, and Theorem 3.23, asserting that this factorisation is unique up to the six relations. The paper also derives auxiliary relations (12)--(16) for bordering extensions and uses the presentation to recover the ternary factorisation system on fat Delta (Proposition 3.24).

Significance. If the presentation is correct, it is a genuinely useful combinatorial description of fat Delta, comparable in spirit to the simplicial identities for the simplex category. The paper is explicit about the three classes of generators, provides concrete index notation, and gives a constructive factorisation algorithm. The claimed presentation also yields the previously sketched ternary factorisation system as a corollary. However, the proof of uniqueness is not yet convincing: two lemmas contain self-referential proof steps, and the crossed relations (9)--(11), on which everything rests, are asserted rather than verified. The central claim is plausible and likely repairable, but the manuscript as written does not establish it.

major comments (5)
  1. [Section 3.4, Lemma 3.17] The proof of Lemma 3.17 is circular: after constructing the horizontal morphism δ and the vertical morphism ω, it says "Finally, we use Lemma 3.17 to factor ω into ψτ". This invokes the very statement being proved. The factorisation of the vertical morphism ω is essential to the existence part of Theorem 3.18, so a self-contained proof (or a clearly stated independent lemma) must be supplied.
  2. [Section 3.2, relations (9)--(11)] The crossed relations among standard, vertical, and degenerated faces are stated with explanatory prose but no verification that they hold as identities in fat Delta. These relations are load-bearing: Theorem 3.23 and the auxiliary relations (12)--(16) of Proposition 3.14 depend on them case by case. The index bookkeeping is delicate; for example, relation (10) leaves implicit the condition that ς_{i+1} is an inner marked vertex in the merged object, and Remark 3.10 flags a further subtlety in the second case of (9). Each of (9), (10), and (11) should be verified by explicit commutative diagrams or by a systematic pushout/pullback argument.
  3. [Section 3.2, Proposition 3.14] Proposition 3.14 derives only relation (12); relations (13)--(16) are dismissed with "The other relations are shown by similar calculation and careful treatment of the indexation." These derived relations are used repeatedly in the uniqueness proofs: Lemma 3.21 uses (16), Lemma 3.22 uses (15) and (16), and Theorem 3.23 uses (16). Since a single off-by-one error in these identities would break the rewrite system, the omitted derivations cannot be left as an exercise in a paper whose main theorem is a presentation by generators and relations.
  4. [Section 3.4, Lemma 3.22] The proof of Lemma 3.22 contains a self-referential step. In the case where g is a degenerated face, after reducing to the expression f = τ'ψ'w^1_{¤p} d_{jβ} ... d_{jβ0} ... d_{j1} ν'φ', the proof says "By Lemma 3.22 we are done." This is the lemma being proved, not the induction hypothesis. If the intended argument is to apply the induction hypothesis to a shorter factorisation, that must be stated explicitly and the hypotheses of the induction must be checked.
  5. [Section 3.3, Lemma 3.17] The proof relies on [Pao25, Lemma 6.11] to split a horizontal morphism into a horizontal part δ followed by a vertical part ω. The referenced lemma is not stated in the manuscript, and the splitting is doing substantial work: it constructs all fibres not pulled back from the codomain. Please state the lemma or provide a self-contained proof, because without this splitting the factorisation construction of Lemma 3.17 does not go through.
minor comments (5)
  1. [Section 3.2, relation (10)] Relation (10) writes "v_j s_i = s_i w^ε_{i+1-ε}" for j = ς_{i+1}, but ε is left unspecified. The two values of ε should be tied explicitly to whether the new marked edge is created at the left or right bordering vertex of the fibre.
  2. [Section 2.5, Definition 2.16 and notation 2.18] The notation ς^0_i and ς^1_i is introduced carefully, but the dependency on η is implicit throughout Section 3. In several relations, for example (9) and (10), it would aid readability to write ς^η_i explicitly at least once in each formula or to state that the fibre under consideration is clear from the domain object.
  3. [Section 3.2, Proposition 3.14 relation (14)] The subscript in "v_{ς_i+ε+1-ε}" is written so that the expression simplifies to ς_i+1, but the intended index may be ς_{i+ε}+1-ε or something else. This should be disambiguated with parentheses or braces.
  4. [Section 2.2, Definition 2.5] The sentence defining the augmented fat Delta category says it is obtained by "restricting the augmented simplex category Δ* to its epimorphisms". This is imprecise: the objects of Δ* are not simply epimorphisms of Δ* in the same way; please clarify the definition.
  5. [Section 3.4, after (19)] The proof uses the notation ¤p as a "dynamic variable" and says its exact value will not be tracked. While this is a reasonable expository device, the uniqueness proof ultimately depends on knowing which relation applies at each step, so the dynamic variable notation should be supplemented by a precise statement of how the index changes under each rewrite.

Circularity Check

2 steps flagged · score 4.0 of 10

Two self-referential proof lines in Lemmas 3.17 and 3.22 sit at load-bearing junctions of the existence/uniqueness chain, but the presentation theorem itself is an independent claim about a concretely defined category.

  1. other [§3.3, Lemma 3.17 (proof, final step of the horizontal-morphism factorisation)]
    "Finally, we use Lemma 3.17 to factor𝜔 into𝜓𝜏, where𝜓 = w𝜖𝛼𝑖𝛼··· w𝜖1𝑖1 and𝜏 = v𝑡𝜄··· v𝑡1."

    The proof of Lemma 3.17 (existence of the three-face factorisation for horizontal morphisms) invokes Lemma 3.17 itself to split the vertical morphism 𝜔 into bordering extensions and vertical faces. As written, the lemma's proof assumes the lemma under proof, so the derivation chain from the generators to Theorem 3.18 (and hence Theorem 3.23) contains a circular step at this exact point. The internal evidence suggests the intended reference is Lemma 3.15, which proves the needed decomposition of vertical morphisms into v's and w's; but the printed text reduces Lemma 3.17 to itself, and no other proof of the horizontal factorisation is supplied.

  2. other [§3.4, Lemma 3.22 (proof, degenerated-face case)]
    "We use (6) to move d𝑗𝛽0 next to s¤𝑝 and combine it to obtain the following 𝑓 =𝜏′𝜓′w1¤𝑝 d𝑗𝛽··· dd𝑗𝛽0··· d𝑗1𝜈′𝜙′. By Lemma 3.22 we are done."

    In the degenerated-face case of Lemma 3.22's proof, after relocating the bordering extension the text concludes 'By Lemma 3.22 we are done.' Since Lemma 3.22 is exactly the statement being proved (uniqueness of the horizontal factorisation), and Theorem 3.23's uniqueness result depends directly on Lemma 3.22, this is a self-referential closing rather than an appeal to the stated induction hypothesis on the number of faces. A strong-induction reading could repair the argument, but the printed proof cites the lemma under proof as its justification, making the written derivation chain circular at a load-bearing junction.

full rationale

Score 4: the central claim retains independent content, but the written proof chain contains two self-referential steps at load-bearing junctions. The main theorem (Theorem 3.23) asserts a generators-and-relations presentation of 𝚫, where 𝚫 is defined independently in §2.2 as a subcategory of the arrow category of epimorphisms in Δ. The three face classes and six relations are concrete squares in Δ; the relations are asserted as genuine identities in 𝚫, not introduced so as to make the conclusion true by construction. There are no fitted parameters, no 'predictions' that coincide with inputs, and no renaming of a known pattern: the presentation is new, and the ternary factorisation system is derived (Prop. 3.24) rather than imported. So the core claim does not reduce to its inputs. The circularity found is in the proof text, not in the statement. Lemma 3.17's proof invokes Lemma 3.17 to factor the vertical morphism 𝜔 (the needed fact is Lemma 3.15's content, suggesting a numbering slip); Lemma 3.22's proof closes with 'By Lemma 3.22 we are done' instead of applying the stated induction hypothesis. Both sit in the load-bearing chain: Theorem 3.18 (existence) depends on Lemma 3.17, and Theorem 3.23 (uniqueness) depends on Lemmas 3.21–3.22. Each appears patchable within the paper's own resources, which is why the score is 4 and not higher. Self-citations to [JKPP25] (the isomorphism of the two descriptions of 𝚫, Theorem 4.22; the active-inert factorisation system used to motivate the vertical faces) are present, but these are separate results with their own proofs and do not assert the presentation theorem; they are self-citation with independent content, not a circular reduction. Relations (13)–(16) are asserted with only (12) verified ('the other relations are shown similarly'), and the crossed relations (9)–(11) are stated with prose rather than commutative-diagram verification; these are correctness and verification risks, not circularity, since the relations are claims about an independently defined category. No self-definitional, fitted-input, uniqueness-import, or renaming pattern was found.

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

The central theorem rests on the chosen definition of fat Delta ([Koc06]), the equivalence of descriptions ([JKPP25, Theorem 4.22]), the existence of pushouts in Delta ([CFPS23, Corollary 3.3]), and the vertical-horizontal splitting ([Pao25, Lemma 6.11]). No free parameters or new entities are introduced.

assumptions (4)
  • domain assumption The working definition of fat Delta is the subcategory of monomorphisms in the arrow category of epimorphisms of the simplex category Delta.
    Adopted in Section 2.2 from [Koc06]; the paper states this is the definition used throughout.
  • domain assumption The relative semiordinal description and the epimorphism-subcategory description of fat Delta are equivalent, per [JKPP25, Theorem 4.22].
    Used for intuition; the paper says it relies exclusively on the Section 2.2 definition.
  • standard math The span [n] <- [m] -> [k] in Delta has a pushout, per [CFPS23, Corollary 3.3].
    Used in the proof of Lemma 2.7 and in constructing face squares.
  • domain assumption A horizontal morphism in fat Delta can be factored into a horizontal morphism followed by a vertical morphism, per [Pao25, Lemma 6.11].
    Used in the proof of Lemma 3.17 to decompose the monomorphism case.

how reviews work

0 comments
Cite this review

Pith. "Pith review of On combinatorial aspects of fat Delta." pith.science (2026). https://pith.science/paper/Z23F44SJ

@misc{pith2026250601717,
  author       = {Pith},
  title        = {Pith review of: On combinatorial aspects of fat Delta},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/Z23F44SJ}},
  note         = {Machine review of arXiv:2506.01717}
}
read the original abstract

The category fat Delta, introduced by J. Kock, is a modification of the simplex category where the degeneracies behave weakly. The objective of this note is to provide tools for working with fat Delta. In particular, we identify three types of morphisms: degenerated, standard and vertical faces, and establish six relations between these classes. We then show that fat Delta is generated by these morphisms and relations.

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

4 extracted references · 4 canonical work pages

  1. [1]

    Monads with Arities and Their Associated Theories

    [BMW12] Clemens Berger, Paul-André Melliès, and Mark Weber. “Monads with Arities and Their Associated Theories”. In: Journal of Pure and Applied Algebra216.8 (2012). doi: 10.1016/j.jpaa.2012.02

    work page doi:10.1016/j.jpaa.2012.02 2012

  2. [39]

    Weak Cartesian Properties of Simplicial Sets

    [CFPS23] Carmen Constantin, Tobias Fritz, Paolo Perrone, and Brandon T. Shapiro. “Weak Cartesian Properties of Simplicial Sets”. In: Journal of Homotopy and Related Structures 18.4 (2023). doi: 10.1007/s40062-023-00334-1 . [JKPP25] Tom de Jong, Nicolai Kraus, Simona Paoli, and Stiéphen Pradal.A study of Kock’s fat Delta

    work page doi:10.1007/s40062-023-00334-1 2023

  3. [2017]

    Space-Valued Diagrams, Type-Theoretically (Extended Abstract)

    doi: 10.48550/arXiv.1704.04543. [Pao25] Simona Paoli. “Weakly globular double categories and weak units”. In:Higher Structures (2025). To appear. doi: 10.48550/arXiv.2008.11180. [Sat17] Christian Sattler. “Kock’s Fat Δ Is a Direct Replacement of Δ.”

    work page Pith review arXiv doi:10.48550/arxiv.1704.04543 2025

  4. [2025]

    A study of Kock's fat Delta

    doi: 10.48550/arXiv.2503.10963. [Koc06] Joachim Kock. “Weak identity arrows in higher categories”. In:International Mathematics Research Papers 2006 (2006), pp. 1–54. doi: 10.1155/IMRP/2006/69163. [Koc10] Joachim Kock. On Ternary Factorization Systems. Comment on an n-Category Café’s blog post. Aug. 1, 2010.url: https://golem.ph.utexas.edu/category/2010/0...

    work page Pith review arXiv doi:10.48550/arxiv.2503.10963 2006

Pith tools

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