Pith. sign in

REVIEW 3 major objections 4 minor 31 references

The paper generalises the Phoa principle to the transfinite case, showing that functions from the infinite simplex into the interval are exactly the ascending sequences of interval elements.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

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

T0 review · deepseek-v4-flash

2026-08-01 18:28 UTC pith:7RZWLGP5

load-bearing objection The transfinite Phoa principle is likely right; the reported colimit gap is a red herring, but Lemma 6.16's composite-iso inference is a real hole in the completeness chapter. the 3 major comments →

arxiv 2607.17292 v1 pith:7RZWLGP5 submitted 2026-07-19 cs.LO cs.PLmath.CTmath.LO

Topology in Synthetic Domain Theory and its Formalisation in Agda

Runze Xue This is my paper
classification cs.LO cs.PLmath.CTmath.LO MSC 03B1518B2506B35
keywords synthetic domain theoryPhoa principleinterval typetransfinite simplexsobriomorphismchain completenesslifting monadformal proof
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

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

Synthetic domain theory studies domains without building them from sets and orders; it uses a special interval type whose paths are meant to be the information order. The Phoa principle says that functions from the interval to itself are determined by their values at the two endpoints. This paper extends that principle to the infinite simplex, the colimit of all finite simplexes, and to the corresponding infinite spine. Its central theorem is that evaluating a function at the natural-number vertices is an isomorphism onto the type of ascending sequences in the interval, making the infinite simplex and the infinite spine topologically indistinguishable. If the paper's concluding conjecture is right, this single topological identification unifies the two completeness properties that define a synthetic domain, merging the Segal and chain-completeness conditions.

Core claim

The central claim is the transfinite Phoa principle (Theorem 5.8): the evaluation map on vertices v : N ↪ Δω is an isomorphism I^{Δω} ≅ Δ∞, where Δω is the ω-simplex formed as the sequential colimit of the finite descending simplices and Δ∞ is the type of ascending sequences in the interval I. The same isomorphism holds for the ω-spine Λω (Theorem 5.10). As a corollary, the precomposition maps O(Λω) ≅ O(Δω) are lattice isomorphisms, so Λω and Δω are sobriomorphic; conversely, the paper shows that the sobriomorphism Λω ⊴ Δ∞ implies the interval is a synthetic domain. The proof runs by establishing the higher Phoa principle for finite simplices, then passing to the colimit, and relies on an ex

What carries the argument

The paper's central object is the interval type I, a dominance and subobject classifier that carries a distributive lattice structure and a lifting operation L; from it are built the finite simplices Δn and, by a sequential colimit, the transfinite objects Δω and Δ∞. The key identity is the higher Phoa principle I^{Δn} ≅ Δ^{n+1}, which the paper re-expresses as a sampling map from vertex evaluation. The transfinite version is obtained by taking the colimit of these isomorphisms and commuting the exponential out of I with the colimit. Sobriomorphisms—maps whose induced maps on observational algebras X→I are lattice isomorphisms—turn these isomorphisms into statements that two spaces have the

Load-bearing premise

The theorem collapses if the exponential functor out of the interval does not preserve the sequential colimit that defines the infinite simplex—a step the paper asserts without proof or axiom—and a separate premise, that the initial lifting-algebra is the colimit of iterated lifting of the initial object, is admitted to fail in the effective topos.

What would settle it

In a topos satisfying Axioms 3.1, 3.2, 3.10 and 4.1, check whether I^{Δω} is isomorphic to the ascending-sequence type Δ∞ under vertex evaluation; if the exponential out of I fails to preserve the ω-colimit, the isomorphism fails and Theorem 5.8 is refuted.

Watch this falsifier. Get emailed when new claim-graph text bears on it.

Share X Bluesky LinkedIn Reddit HN

If this is right

  • The ω-simplex Δω and the ω-spine Λω are sobriomorphic: they support the same observational topology, so functions into the interval cannot tell them apart.
  • The observational algebra of either infinite object is isomorphic to the type Δ∞ of ascending sequences, giving a concrete description of the topology.
  • If the paper's Conjecture 6.20 holds, chain-completeness of a type is equivalent to being right-orthogonal to the embedding Λω ↪ !, tying a domain-theoretic property to a single orthogonality condition.
  • The machine-checked proofs make the reduction from the classical to the transfinite Phoa principle fully constructive.
  • The dual treatment of ascending and descending sequences explains why the finite results do not automatically extend to the transfinite case.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The unproved colimit-interchange step suggests the theorem is really about compactness of the interval; stating 'I preserves ω-colimits' as an explicit axiom would likely make the proof load-bearing and testable across models.
  • If sobriomorphism, not isomorphism, is the right notion of topological identity, then the paper's construction suggests a general recipe: any object whose vertices span its observational algebra admits a Phoa-style representation.
  • The conjectural unification of Segal and chain completeness could be tested in the effective topos, where the colimit axiom fails; failure there would show which separate axioms are needed.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 4 minor

Summary. The paper develops a synthetic domain theory of the interval type in Cubical Agda. It introduces dual simplices and spines, proves that the observational algebra of an n-simplex is isomorphic to an (n+1)-simplex via the higher Phoa principle, and then extends this to a transfinite Phoa principle: the observational algebra of the ω-simplex is isomorphic to the space of ascending sequences in the interval (Theorem 5.8), with an analogous statement for the ω-spine (Theorem 5.10). The paper then introduces sobriomorphisms as isomorphisms of observational algebras and uses them to connect the transfinite Phoa principle to chain completeness, culminating in a conjectural unified completeness statement. The paper also reports a formalisation of several theorems in Cubical Agda, including the finite and transfinite Phoa principles.

Significance. If the main claims are correct, the transfinite Phoa principle is a genuinely useful bridge between the combinatorial structures of simplices/spines and the initial/final algebras of the lifting functor, and the sobriomorphism reformulation is a clean conceptual packaging. The finite-dimensional theorems (3.20, 4.6, 4.13) are coherent, and the paper's reliance on explicit Agda formalisation for several of them is a strength, although no code artifact is included. The transfinite results are however conditional on Axiom 5.3, which the paper acknowledges is false in the effective topos; this limits the scope to an axiomatic extension rather than a theorem of standard SDT. The completeness narrative in Chapter 6 is not supported as written because of an invalid inference in Lemma 6.16 and because the required inclusions between spines, simplices, and their duals are not established. The central transfinite Phoa principle itself appears defensible after a clarification of notation.

major comments (3)
  1. [§6.3, Lemma 6.16] Lemma 6.16 is not proved. The text says that because the composite restriction O(C)→O(A) is invertible and factors as O(C)→O(B)→O(A), both factors are invertible. This is the invalid inference 'composite iso ⇒ each factor iso'. In bounded lattices a counterexample is O(C)=O(A)=2, O(B)=4, with f:2→4 the bottom/top inclusion and g:4→2 given by g(0)=g(a)=0, g(1)=g(b)=1; then g∘f is an iso but neither f nor g is. No special property of restriction maps of observational algebras is supplied to rule out such a configuration. Since Theorem 6.19 and the route to Conjecture 6.20 rely on this lemma, that part of the completeness narrative is unsupported as written.
  2. [§5.2, Theorem 5.8] The proof of Theorem 5.8 uses the notation [I,X] ambiguously. If [I,X] means O(X)=X→I, then I^{Δω}=[I,Δω] is fine, and the step [I,colim_n s_n] = lim_n [I,s_n] is the standard universal property of maps out of a sequential colimit; it does not require tinyness or compactness of I. If instead [I,X] denotes the exponential I→X, then the first equality I^{Δω}=[I,Δω] is false. The proof should state the intended convention and invoke the colimit recursion principle explicitly, rather than calling it a 'property of the internal-hom'. This is a local fix, but as printed it obscures a central step.
  3. [§6.3, Theorem 6.19] Theorem 6.19 is asserted without a proof and its ingredients are not compatible. Lemma 6.16 requires A⊆B⊆C, but Λω is a coequalizer/HIT and Δω is a sequential colimit of simplices; no inclusions Λω⊆Δω⊆Δ∞ are defined. The sobriomorphism of Theorem 5.11 is not an inclusion, so it does not supply the hypothesis of Lemma 6.16. Thus even independently of the invalid inference in Lemma 6.16, the chain of reasoning leading to Theorem 6.19 is incomplete. Either the theorem should be made conditional on genuinely established embeddings, or it should be downgraded to a conjecture.
minor comments (4)
  1. [§5.3, Definition 5.9] The text says Λω is 'the limit of the following diagram' and then 'Equivalently, Λω is the coequalizer of p0 and p1'. A coequalizer is a colimit, not a limit; this should be corrected.
  2. [§5.1–§5.2] The symbol Δ∞ is used for both the descending sequences of §5.1 and the ascending sequences of §5.2. The two objects should have distinct notations throughout; the current rendering is confusing, especially in the statement and proof of Theorem 5.8.
  3. [Appendix A] The paper reports an Agda formalisation of several key theorems but no repository or machine-checked artifact is included. For reproducibility, the codebase should be archived and linked, or the status of the formalisation should be described more precisely.
  4. [§5.2, Lemma 5.7] The diagram in Lemma 5.7 labels the maps I^{s_n}; the proof discusses O(s_n)(f)=f∘s_n. This is consistent, but the notation should be explained once, since the same symbol I^{s_n} could be misread as an exponential applied to s_n.

Circularity Check

0 steps flagged

No significant circularity: the transfinite Phoa principle is derived from the higher Phoa principle plus universal properties of colimits/limits, not from its own conclusion.

full rationale

Walking the derivation chain, I find no load-bearing step that reduces to its own input by construction. Theorem 5.8 derives I^{Δω} ≅ Δ∞ from the finite higher Phoa principle (Theorem 4.6) and the identification of Δω and Δ∞ as colimit/limit of the corresponding chains: I^{Δω} = lim_n I^{s_n} ≅ lim_n d_n = Δ∞. Δ∞ is defined independently as a limit of finite simplices and the isomorphism is not assumed as the conclusion. The higher Phoa principle is attributed to [15] and also proved in the text, so the argument does not rest on an unverified self-citation; [15] and [21] are external works with no author overlap with the present thesis. The formalisation in Cubical Agda further supplies independent support for the main theorems. The paper is transparent about its axiomatic input: Axiom 5.3 is explicitly stated as an axiom and the paper itself notes that the inductive construction was disproved in the effective topos. The genuinely fragile steps are correctness risks rather than circularity: Lemma 6.16 uses the invalid inference that if a composite restriction map is an isomorphism then each factor is an isomorphism, which undermines Theorem 6.19 and Conjecture 6.20; and the proof of Theorem 5.8 has ambiguous bracket notation around [I;Δω] that needs a one-line clarification. These are not cases where a prediction is defined as the fitted input or where a conclusion is assumed in a premise. No fitted parameters are present, and the sobriomorphism terminology is a transparent definitional repackaging, not a disguised renaming of the target result.

Axiom & Free-Parameter Ledger

0 free parameters · 7 axioms · 0 invented entities

The central results are derived from a stack of explicitly postuled axioms about the interval and the initial L-algebra, plus one unstated compactness assumption. No free parameters are fitted to data.

axioms (7)
  • domain assumption Axiom 3.1: J_K : I → Ω is an embedding; 0≠1; I is an h-set.
    Postulates that the interval type classifies propositions and rules out trivial models.
  • domain assumption Axiom 3.2: I is a bounded distributive lattice with J iuj K = JiK ∧ JjK, J itj K = JiK ∨ JjK, i⊑j = JiK→JjK.
    Gives the interval its order/lattice structure used throughout.
  • domain assumption Axiom 3.10: ∃∇: LI→I with J∇(i,j)K = Σ_{φ:JiK} Jj(φ)K.
    Σ-closure/dominance; needed for Δ^n ≅ L^n⊤.
  • domain assumption Axiom 4.1 (Interpolation): ∀p:I→I. p(i) = p(0) ⊔ (i ⊓ p(1)).
    This is the Phoa principle; used in the higher Phoa theorem.
  • domain assumption Axiom 5.3: initial L-algebra ! exists and ! = lim_{→n} L^n⊥.
    Explicitly assumed; the text notes the Adámek construction fails in effective topos, so this is not a theorem.
  • domain assumption Axiom 6.12: I is chain-complete.
    Postulated for the synthetic-domain results in Chapter 6.
  • ad hoc to paper I^ preserves ω-colimits (I is tiny/compact).
    Used silently in the proof of Theorem 5.8 as '[I, colim s_n] = colim [I, s_n]'; not stated, proved, or cited. Without it the transfinite Phoa proof fails.

pith-pipeline@v1.3.0-alltime-deepseek · 19177 in / 26032 out tokens · 243082 ms · 2026-08-01T18:28:03.690406+00:00 · methodology

0 comments
Cite this review

Pith. "Pith review of Topology in Synthetic Domain Theory and its Formalisation in Agda." pith.science (2026). https://pith.science/paper/7RZWLGP5

@misc{pith2026260717292,
  author       = {Pith},
  title        = {Pith review of: Topology in Synthetic Domain Theory and its Formalisation in Agda},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/7RZWLGP5}},
  note         = {Machine review of arXiv:2607.17292}
}
Share X Bluesky LinkedIn Reddit HN
read the original abstract

This project investigates the Phoa principle in synthetic domain theory (SDT), and provides a generalisation to the transfinite cases. The Phoa principle plays a pivotal role in SDT by illustrating how the paths give the information order on the interval type and other algebraic structures in SDT. The project defines the dual simplices and spines and introduces the concept of sobriomorphisms, which contributes to a new interpretation of the Phoa principle and its generalisations. Finally, the project proposes a hypothetical completeness theorem that may unify the Segal completeness and the chain completeness in SDT based on investigations on the Phoa principle in the project. The project also includes axiomatisation of the interval type in Cubical Agda and the formalised proof for the main theorems.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

31 extracted references · 5 linked inside Pith

  1. [1]

    Free algebras and automata realizations in the language of categories

    Jiří Adámek. Free algebras and automata realizations in the language of categories. Commentationes Mathematicae Universitatis Carolinae , 15(4):589–602, 1974. Pub- lisher: Charles University in Prague, Faculty of Mathematics and Physics

    1974

  2. [2]

    First steps in synthetic guarded domain theory: step-indexing in the topos of trees

    Lars Birkedal, Rasmus Ejlers Møgelberg, Jan Schwinghammer, and Kristian Støvring. First steps in synthetic guarded domain theory: step-indexing in the topos of trees. Logical Methods in Computer Science , Volume 8, Issue 4, October 2012. Publisher: Episciences.org

    2012

  3. [3]

    Synthetic fibered (1; 1)-category theory, August 2022

    Ulrik Buchholtz and Jonathan Weinberger. Synthetic fibered (1; 1)-category theory, August 2022. arXiv:2105.01724 [math]

    Pith/arXiv arXiv 2022

  4. [4]

    Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom

    Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In 21st Interna- tional Conference on Types for Proofs and Programs (TYPES 2015) (2018) , pages 5:1–5:34. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2018

    2015

  5. [5]

    B. A. Davey and H. A. Priestley. Introduction to Lattices and Order . Cambridge University Press, Cambridge, 2 edition, 2002. 10.1017/CBO9780511809088

    doi:10.1017/cbo9780511809088 2002

  6. [6]

    Marcelo P. Fiore. Axiomatic Domain Theory in Categories of Partial Maps . Distin- guished Dissertations in Computer Science. Cambridge University Press, Cambridge, 1996

    1996

  7. [7]

    J. M. E. Hyland. First steps in synthetic domain theory. In Aurelio Carboni, Maria Cristina Pedicchio, and Guiseppe Rosolini, editors, Category Theory , pages 131–156, Berlin, Heidelberg, 1991. Springer

    1991

  8. [8]

    Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks, June 2022

    Magnus Baunsgaard Kristensen, Rasmus Ejlers Møgelberg, and Andrea Vezzosi. Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks, June 2022. arXiv:2102.01969 [cs]

    Pith/arXiv arXiv 2022

  9. [9]

    Formalizing the 1- Categorical Yoneda Lemma, December 2023

    Nikolai Kudasov, Emily Riehl, and Jonathan Weinberger. Formalizing the 1- Categorical Yoneda Lemma, December 2023. arXiv:2309.08340 [math]

    Pith/arXiv arXiv 2023

  10. [10]

    Denotational Semantics, December 2024

    Meven Lennon-Bertrand. Denotational Semantics, December 2024. 39

    2024

  11. [11]

    Sheaves in Geometry and Logic: A First Introduction to Topos Theory

    Saunders Mac Lane and Ieke Moerdijk. Sheaves in Geometry and Logic: A First Introduction to Topos Theory . Universitext. Springer, New York, NY, 1994

    1994

  12. [12]

    Bisimulation as path type for guarded recursive types

    Rasmus Ejlers Møgelberg and Niccolò Veltri. Bisimulation as path type for guarded recursive types. Proc. ACM Program. Lang., 3(POPL):4:1–4:29, January 2019

    2019

  13. [13]

    Domain theory for concurrency

    Mikkel Nygaard and Glynn Winskel. Domain theory for concurrency. Theoretical Computer Science , 316(1):153–190, May 2004

    2004

  14. [14]

    Domain Theory in Realizability Toposes

    Wesley Phoa. Domain Theory in Realizability Toposes . PhD thesis, University of Edinburgh, Edinburgh, July 1991

    1991

  15. [15]

    When is the partial map classifier a Sierpinski cone?, April 2025

    Leoni Pugh and Jonathan Sterling. When is the partial map classifier a Sierpinski cone?, April 2025

    2025

  16. [16]

    Reus and Th

    B. Reus and Th. Streicher. General synthetic domain theory — A logical approach (extended abstract). In Eugenio Moggi and Giuseppe Rosolini, editors, Category Theory and Computer Science , pages 293–313, Berlin, Heidelberg, 1997. Springer

    1997

  17. [17]

    Program verification in synthetic domain theory

    Bernhard Reus. Program verification in synthetic domain theory . Berichte aus der Informatik. Shaker, Aachen, als ms. gedr edition, 1996

    1996

  18. [18]

    A type theory for synthetic 1-categories, June

    Emily Riehl and Michael Shulman. A type theory for synthetic 1-categories, June

  19. [19]

    Dana S. Scott. Outline of a mathematical theory of computation. Technical Report PRG02, OUCL, November 1970

    1970

  20. [20]

    Dana S. Scott. Domains for denotational semantics. In Mogens Nielsen and Erik Meineche Schmidt, editors, Automata, Languages and Programming, pages 577– 610, Berlin, Heidelberg, 1982. Springer

    1982

  21. [21]

    Domains and Classifying Topoi, May 2025

    Jonathan Sterling and Lingyuan Ye. Domains and Classifying Topoi, May 2025. arXiv:2505.13096 [cs]

    Pith/arXiv arXiv 2025

  22. [22]

    Homotopy Type Theory: Univalent Founda- tions of Mathematics

    The Univalent Foundations Program. Homotopy Type Theory: Univalent Founda- tions of Mathematics . Institute for Advanced Study, 2013

    2013

  23. [23]

    Jaap van Oosten and Alex K. Simpson. Axioms and (counter)examples in synthetic domain theory. Annals of Pure and Applied Logic , 104(1):233–278, July 2000

    2000

  24. [24]

    Cubical agda: a dependently typed programming language with univalence and higher inductive types

    Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. Cubical agda: a dependently typed programming language with univalence and higher inductive types. Source code for examples from article Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types , 3(ICFP):87:1–87:29, July 2019

    2019

  25. [25]

    bottom-up

    Glynn Winskel. On powerdomains and modality. Theoretical Computer Science , 36:127–137, January 1985. 40 Appendix A Formalizing Proofs in Agda We have formalized some of the major theorems and lemmata in (Cubical) Agda. Table A.1 lists these results and their corresponding formalisations in the code base. This appendix will give a walkthrough of the techn...

    1985

  26. [27]

    (Axiom 3.1, PreSDT.SisSet) I is a h-set

  27. [28]

    (Axiom 3.1, PreSDT.s06=s1) 02 I and 12 I with 06= 1. 41

  28. [29]

    (Axiom 3.1, PreSDT.defIsMono) JiK = JjK implies i =j

  29. [30]

    (Axiom 3.10, SemiLattice.SΣ-def) There exists a L-algebra :LI! I satisfying J (i;j )K = X ϕ:JiK Jj( )K Define iuj := (i; _:j)

  30. [31]

    The simplices ∆n and ∆n are then defined as the sum type of In as Vector and a witness of the predicate IsMontonic

    (Axiom 3.2, Lattice.t-def) The exists a binary operation t : I! I! I satisfying JitjK = JiK JjK where A B is the pushout A B B A A B π2 π1 ⌟ A.2 Encoding of Cubes and Simplices To encode the finite cubes In and the simplices ∆n and ∆n, we introduced a vector type (SemiLattice.Vector.Vector) defined inductively as Vector : Type → N → Type Vector A zero = U...

  31. [2023]

    arXiv:1705.07442 [math]

    Pith/arXiv arXiv