Paper statuses — A work’s standing in this record: whether it is worth reading. Not whether its findings are true — that is the THEORY scheme’s business, and the two can disagree in either direction.
Superseded — later work covers this better, and the note names it.
4 of 2004 LIT documents. Back to the full index.
| # | Title | Summary | Status |
|---|---|---|---|
| LIT-040 v2 | two-level type theory [descriptive title: nLab wiki entry “two-level type theory”] | nLab (2018), https://ncatlab.org/nlab/show/two-level+type+theory. Two-level type theory pairs a homotopy (univalent, fibrant) type theory with an outer level having UIP “exact equality” (the internalised metatheory). The nLab page is an accurate but thin gloss on two-level type theory. It says nothing about the result that makes 2LTT usable: basic 2LTT is conservative over HoTT (ACKS Prop. 2.18: an inner type provably inhabited in 2LTT is inhabited in HoTT), which answers much of the page’s own “open question” about the principle of equivalence. It also omits that a fibrant-replacement type former would force UIP on the inner level (ACKS Thm 2.20). The paper it cites, ACKS arXiv:1705.03307, is the proper source: definitions via models, conservativity, the axiom menu (A1)–(A6)/(T1)–(T3), and internal Reedy-fibrant diagrams over inverse categories with a definition of univalent (∞,1)-category. | Superseded — by LIT-095; read in full 2026-09-25 (NOTE-047); superseded by Annenkov–Capriotti–Kraus–Sattler, “Two-Level Type Theory and Applications” (arXiv:1705.03307; MSCS 2023, DOI 10.1017/S0960129523000130), which the page itself cites and which covers everything the page says, with proofs and the conservativity theorem the page lacks. That paper is now filed as LIT-095, and this page is superseded by it. |
| LIT-064 v3 | Talagrand Meets Talagrand: Upper and Lower Bounds on Expected Soft Maxima of Gaussian Processes with Finite Index Sets | Chu & Raginsky (2025), ARXIV-2502.06709. Take a centered Gaussian process on a finite set T with max variance σ² and minimum separation a. The expected softmax-weighted average g(β) = E[Σ_t X_t e^{βX_t}/Z] satisfies g(β) ≤ √(2σ²·E D(ν_β‖ν₀)) for every β (Thm 1, D = KL from uniform). For β ≥ β*, g(β) ≥ c·a·√(E D(ν_β‖ν₀)), with c the Sudakov constant (1/17 via Marcus–Rosen) (Thm 2). For i.i.d. N(0,σ²) logits there is an exact identity, g(β) = βσ²(1 − E‖ν_β‖²₂) (Lemma 2). The quenched free energy is bounded above by √(2σ²·E D_{1/2}(ν_β‖ν₀)), with an i.i.d. lower bound of (cσ/2)√(E D_{1/2}) (Thms 4–5). | Superseded — by ANTH-LIT-726; moved to the Anthology of the SOTA as ANTH-LIT-726 on 2026-09-26, at the owner’s request, with its Read NOTE; nothing is held in both records (ADR-001) |
| LIT-380 v2 | A Topos Perspective on the Kochen-Specker Theorem: III. Von Neumann Algebras as the Base Category | Hamilton et al. (1999), arXiv:quant-ph/9911020. Hamilton, Isham & Butterfield move the series’ base category from operators (O) and Boolean subalgebras (W) to the poset V of commutative von Neumann subalgebras of B(H). There they restate Kochen–Specker as “the spectral presheaf Σ(V) = Gelfand spectrum of V has no global elements” (dim H > 2, cited, §2.2). They identify the coarse-graining presheaf G(V) = L(V), G(i)(P̂) = inf{Q̂ ∈ L(V₂) | P̂ ≤ Q̂} (Def. 3.1), with the presheaf CloΣ of clopen subsets of the spectra; the isomorphism is asserted, and part IV proves it. A state ρ yields the sieve-valued valuation ν^ρ_V(P̂) = {V′ ⊆ V | ρ(G(P̂)) = 1} (Def. 3.4) and the support projectors inf{P̂ ∈ L(V) | ρ(P̂) = 1}. These form a global element of G and hence an “interval valuation”, a subobject of Σ (§§4.2–4.4). The probability-r valuations give subobjects of G but not global elements. | Superseded — by LIT-382; read in full 2026-10-01 (NOTE-327); covered better by part IV (Butterfield & Isham 2002, read alongside), which restates this paper’s V-framework definitions nearly verbatim, proves the G ≅ CloΣ isomorphism that this paper only asserts and develops its interval valuations into theorems, and by Döring–Isham II (LIT-335), whose spectral presheaf over V(H) and clopen propositions are the mature form; it remains the citation for introducing V as the base category (as LIT-335 credits it). |
| LIT-813 v2 | The Sheaf-Theoretic Structure of Definite Causality | Gogioso & Pinzani (2021), QPL 2021, EPTCS 343:301–324; withdrawn by the authors in 2024. Extends Abramsky–Brandenburger to a finite causal order. Inputs live on lower sets, sections are causal functions (an output depends only on inputs in its past), and an empirical model is a causal conditional distribution. Locality is a global section, equivalently a mixture of deterministic causal functions (Proposition 21). The models form a polytope cut out by linear causality equations, and pre-orders sketch indefinite causality. The construction’s “locale of inputs” is not a locale, as the authors’ withdrawal says. | Superseded — by LIT-800, LIT-808, LIT-788; read 2026-10-09 (NOTE-629), and superseded by its authors’ trilogy: LIT-800 (The Combinatorics of Causality, arXiv 2206.08911), LIT-808 (The Topology of Causality, 2303.07148) and LIT-788 (The Geometry of Causality, 2303.09017). The authors withdrew it: the arXiv record’s v3 (3 April 2024) states that the paper “has been superseded by arXiv:2206.08911v4, arXiv:2303.07148 and arXiv:2303.09017”, that its Definition 3 (the locale of inputs) “is not fit for purpose”, and that it is “unlikely to be the right reference”. The reading confirms the defect: the meet given in Proposition 5 can leave the poset, and the poset is not distributive, so it is not a locale (NOTE-629 gives a two-event counterexample). The successors replace the locale of inputs with spaces of input histories under the lowerset topology, a genuine topology; the sheaf of causal functions and locality as a global section are redone in LIT-808, and the polytope and the BFW causal fractions are proved in LIT-788. |