{"id":"41b3314f-d926-4ea5-8cfb-789303297f4e","arxiv_id":"2607.27387","paper_version":1,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":8.0,"correctness_risk":"medium","formal_verification":"full","parameter_count":0,"one_line_summary":"Extension types are definable in two-level type theory, all their Riehl–Shulman rules become theorems, and cubical gluing is equivalent to univalence in this framework.","lead":"This paper shows that extension types — partially specified functions with fixed boundary values used across several type theories — can be defined rather than assumed inside two-level type theory, with all their standard rules following automatically. It also proves that cubical gluing and the univalence axiom are equivalent, opening a route to the open question of whether cubical and book homotopy type theory prove the same theorems.","discovery_kind":"unification","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Strict freeness claim is hostage to the on-the-nose conversion axioms (T1)–(T2); weakening them to homotopy-preserving conversion breaks the strict extension-type rules.","rationale":"The reader's weakest assumption identifies exactly the on-the-nose conversion axioms T1–T2 as the load-bearing premise, and this is indeed where the strictness of the entire extension-type calculus and the strict Glue boundary attach. I considered other possible concerns—pullback stability of cofibrations, substitution stability of the type former, and reliance on the AI-generated Agda code—but the paper explicitly flags the cofibrancy closure limitations (Theorem 3.8), the formalization is machine-checked and publicly available, and the main equivalence cycle is internally consistent and fully stated. Since the paper clearly declares T1–T2 as an assumption and the intended simplicial/cubical models satisfy them (per the cited literature), this does not undermine the verdict. No change to the reader's ACCEPT is warranted.","tokens_in":34244,"tokens_out":37107,"duration_ms":337295,"concrete_test":"In the accompanying Agda development, replace the definitional two-level conversion (T1)–(T2) by a version in which the conversion preserves Π, Σ, and Unit only propositionally, inserting the necessary transports into the boundary proofs of Definition 3.1, and re-type-check Theorems 3.2 and 3.11. If the strict β/η laws and the contractibility of relative extension types no longer hold as strict statements, the freeness claim is confirmed to rest precisely on T1–T2.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central 'extension types for free' claim is conditional on the 2LTT axioms (T1)–(T2) of Annenkov et al. [7], stated in Section 2.1: the conversion from inner to outer level preserves Π, Σ, and Unit *on the nose*, 'to avoid coercions'. The definable extension type of Definition 3.1 is the strict fiber of the restriction map i∗ over a partial section a, so its elements are pairs (f, p) with p : f∘i =s a. The strict Riehl–Shulman rules (Theorem 3.2), relative function extensionality (Theorem 3.11), the strict Glue boundary and coherence (Definition 4.3), and the univalence-to-contractible-Glue-data direction (Theorem 5.4) all use this strict boundary equality and the fibrancy of the strict fiber. If the conversion preserved Π/Σ/Unit only up to homotopy, the strict fiber would need coherence transports, the boundary would not be literally f∘i =s a, and the strict β/η rules would degrade to propositional versions. This is an explicit framework assumption, not proved in the paper; the semantic freeness claim over all HoTT models inherits it. The paper is transparent about the assumption, so this is a caveat rather than an internal inconsistency.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper develops a framework in two-level type theory (2LTT) in which extension types are defined rather than postulated. For a cofibration i : Φ → Ψ, a fibrant family A over Ψ, and a partial section a, the extension type is defined as the strict fiber of the restriction map over a (Definition 3.1). From this definition the paper derives the Riehl–Shulman extension-type calculus: the rules hold strictly (Theorem 3.2), the structural equivalences RS 4.1–4.5 become strict isomorphisms (Theorems 3.4–3.8), relative function extensionality becomes a theorem (Theorem 3.11), and realignment, extension extensionality, and the homotopy extension property follow (Corollary 3.12, Theorems 3.13–3.15). The paper then studies CCHM-style Glue, introduces several formulations (literal rules on sections, Glue structures, contractible Glue data, weak Glue structures), and proves that for a path interval univalence is equivalent to gluing in these senses (Theorem 5.15). The final section sketches a program, via 2LTT conservativity, toward the conjecture that cubical type theories are conservative over book HoTT. All results in Sections 2–5 are claimed to be formalized in Agda using the --two-level flag and Uskuplu's 2LTT library.","tokens_in":34564,"tokens_out":23524,"duration_ms":232643,"significance":"If correct, the paper gives a clean unification of the various extension-type notions in the literature and shows that a substantial portion of the Riehl–Shulman calculus is automatic once a cofibration class is fixed. The gluing–univalence equivalence is strong and reverses the usual Glue-to-univalence direction, giving a new internal characterization of univalence. A major strength is the machine-checked Agda formalization of the main body, including the representation-level fibrant-match statements. The main caveat—already disclosed by the author—is that the strictness of the extension-type calculus depends on the on-the-nose conversion axioms (T1)–(T2) of 2LTT; if conversion only preserved Π, Σ, and Unit up to homotopy, the strict boundary equalities and strict rules would degrade to propositional versions. Section 6 is explicitly a route toward the conservativity conjecture and is not formalized; it should not be read as a proof of that conjecture.","major_comments":[{"comment":"The proof asserts that from Θ being an equivalence one obtains glue(t,a) with strict boundary glue(t,a) ∘ i =s t. An element of the homotopy fiber of Θ over (t,a) only supplies an inner equality b∘i = t along with an equality of the unglue section; it does not, by itself, give the strict boundary. This matters because Corollary 5.5 and the advertised 'full constructor package up to homotopy, with term-bdry strict' depend on this point. The gap is probably repairable: when each unglue_γ is an equivalence, the type of b with b∘i =s t and unglue⊙b = a0 is contractible (unglue⊙(−) is an equivalence and the boundary condition is a strict proposition), and its center gives the required glue with strict term-bdry. Please spell this out, or explicitly refer to the formalized lemma Extension.GlueConstructorPackage for this precise step.","section":"§4.2, Lemma 4.2(2)"}],"minor_comments":[{"comment":"The abstract says that 'the only genuine assumptions are which maps count as cofibrations.' This is too strong: the strictness of the entire development also assumes the on-the-nose conversion axioms (T1)–(T2) of Annenkov et al. The assumptions are stated in §2.1, but the abstract and the introduction's freeness claim should be qualified so that the reader does not expect the strict extension-type rules to survive in a 2LTT where conversion preserves structure only up to homotopy.","section":"§2.1 / Abstract"},{"comment":"Cross-reference mismatch: §2.1 refers to 'Theorem 2.1 below', but the numbered statement in §2.2 is Lemma 2.2. Similarly, §5.3 refers to 'Theorem 5.9' where the text labels it Remark 5.9, and the introduction refers to 'Theorem 4.2' where the heading is 'Lemma 4.2'.","section":"§2.1 / §2.2"},{"comment":"The phrase 'family of mere maps u' is potentially confusing: 'mere' is used in HoTT for propositional truncation, but here it seems to mean 'plain functions without an equivalence witness'. Please use unambiguous terminology.","section":"Definition 5.11"},{"comment":"The Agda documentation reference [1] points to Agda v2.6.3, while the paper says the development type-checks with Agda 2.8.0. Please update the reference or note the discrepancy. A commit hash or version pin for the repository would also improve reproducibility.","section":"Formalization"},{"comment":"In the full text, the title is rendered as 'Extension Types for F ree'; this appears to be a formatting artifact and should be fixed.","section":"Title / Abstract"}],"recommendation":"minor_revision","confidential_remarks":"The paper is strong and the main claims are likely correct; the Agda formalization is a significant asset. My principal technical concern is the proof sketch of Lemma 4.2(2), which does not, as written, justify the claimed strict boundary of glue; I would like the author to expand that argument or point precisely to the corresponding formalized lemma. The T1/T2 caveat should also be made more prominent in the abstract and introduction. I did not independently inspect the Agda development; given that the formalization was described as AI-generated and only manually checked, an independent type-check by the author and a clear statement of the Agda/library versions would increase confidence."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Worth a serious look. The core idea is simple and elegant: in two-level type theory, define the extension type as the strict fiber of the restriction map along a cofibration. That definition validates the Riehl–Shulman rule package—strictly, with relative funext and realignment as theorems—and the same construction subsumes cubical, simplicial, and proposition-indexed extension types. The paper then goes further and proves an equivalence cycle: univalence, contractible Glue data, Glue structures, and weak Glue structures are all equivalent over a path interval. Reversing the usual Glue-to-univalence direction is a real contribution.\n\nThe machine-checked formalization is the strongest evidence. Sections 2–5 are formalized in Agda with the --two-level flag, on Uskuplu's library, and the paper links to the code. That's real support for the central derivations. The writing is careful about which claims are formalized and which are not: the conclusion section is clearly marked as not formalized, and the limitations are disclosed in place.\n\nThe main soft spot is exactly the one the stress-test flags, and it's disclosed rather than hidden: the strict rules depend on the on-the-nose preservation axioms T1–T2 for the inner-to-outer conversion. If that conversion only preserved Π, Σ, and Unit up to homotopy, the strict boundary equations would need coercions and the strict Riehl–Shulman rules would degrade to propositional versions. This is a real condition, not a cosmetic one, and the paper states it plainly. The semantic freeness claim inherits this: it rests on cited model constructions, not on a new proof in this paper. That's fine, but it means the 'free' in the title is conditional on the chosen 2LTT axiomatics.\n\nMinor points: the union law needs meet-closure of the cofibration class, which is stated; and the Section 6 conservativity route is only a suggestion, not a result—the author calls it a toy comparison, and that is accurate. Also, the formalization is described as written by Claude Opus with manual checking; I did not re-run it, so the machine-checked claim is as good as the author's word plus the linked code. In this case that seems reliable.\n\nOverall: this is a solid, honest paper. It doesn't settle the cubical-conservativity conjecture, but it gives a useful framework and a real equivalence that was not known. It deserves a serious referee. I'd bring it to reading group and cite the formalized results.","headline":"A formally checked 2LTT framework that derives extension types rather than postulating them, with a genuinely new gluing–univalence equivalence cycle; the strictness claims are conditional on the clearly-stated T1–T2 axioms.","tokens_in":35033,"tokens_out":2353,"would_cite":true,"duration_ms":22289,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B15","03F50"],"pacs":[],"model":"deepseek-v4-flash","headline":"In two-level type theory, extension types are definable rather than postulated, and the definition validates the full extension-type calculus and makes cubical gluing equivalent to univalence.","keywords":["extension types","two-level type theory","cofibrations","cubical type theory","univalence","Glue types","path interval","conservativity"],"falsifier":"Construct or locate a model of two-level type theory that satisfies the chosen axioms except that the inner-to-outer conversion preserves Π and Σ only up to homotopy, and check whether the boundary rule for the naive strict-fiber extension type still holds; the paper's Theorem 3.2 predicts it fails without on-the-nose preservation. Separately, any model with a path interval and a weak Glue structure but a non-univalent universe would directly contradict the paper's Theorem 5.14.","tokens_in":34120,"feed_emoji":"🧩","tokens_out":6063,"duration_ms":57407,"temperature":0.7,"pith_summary":"The paper aims to show that extension types—types of partially determined terms, like paths with fixed endpoints—are not a new postulate needing bespoke semantics. Working in two-level type theory, which layers a strict equality on top of homotopy type theory, the paper defines the extension type along a cofibration as the strict fiber of a restriction map. This one definition makes the entire known extension-type calculus hold strictly: introduction, elimination, β, η, and boundary rules, with relative function extensionality and the homotopy extension property as theorems rather than axioms. The framework then lets the paper prove that cubical gluing and univalence are equivalent notions: univalence yields contractible Glue data along every cofibration, and a weak Glue structure on a path interval forces univalence. A sympathetic reader should care because this unifies scattered extension-type constructions and gives a concrete route toward comparing cubical type theory with original homotopy type theory.","feed_headline":"Gluing and univalence proven equivalent in two-level type theory","feed_subtitle":"The same setup derives the whole extension-type calculus, making univalence and cubical gluing interchangeable.","key_machinery":"The load-bearing object is the extension type defined as the strict fiber of the restriction map i*: Π_Ψ A → Π_Φ (A∘i) over a partial section a, taken with the outer strict equality =s. Because the cofibration i is defined to make restriction preserve (trivial) fibrations, this strict fiber is automatically fibrant, which is what turns the definition into a type former with the right homotopy content. On the application side, the path interval—an interval whose endpoint inclusion is a cofibration and which carries a natural line-to-identity operation—is the detector that lets a weak Glue structure recover univalence.","core_discovery":"The central claim, on the paper's own terms: in two-level type theory, once a class of cofibrations is fixed, the extension type defined as the strict fiber of the restriction map over a partial section is all that extension types ever were. Every rule of the known extension-type calculus holds strictly for this definition, and the axioms that other presentations postulate—notably relative function extensionality—are provable. The same framework makes the various cubical formulations of gluing collapse into a single cycle of implications: univalence implies contractible Glue data for every cofibration, and contractible data implies Glue structures, which imply weak Glue structures, which imp","pith_inferences":["Restricting the outer face calculus to a decidable sub-universe of strict propositions (a dominance or cofibration classifier) should recover decidable boundary checking from this framework without disturbing the theorems; the paper names this parametrization as future work.","The equivalence cycle suggests that in any type theory with a strict boundary layer, adding interval-like cofibrations and extension types secretly adds univalence; the strength is not in the Glue former but in the strict boundary discipline.","A natural test extension: instantiate the framework with a non-cubical shape layer—simplicial or tope-theoretic—and check which structural equivalences survive when the cofibration class is not meet-closed; the paper's union-law caveat predicts failures there."],"forward_implications":["Every model of the base homotopy type theory automatically yields a model with extension types, since two-level type theory is conservative and its semantics extend the standard models.","The extension-type rules hold strictly, and principles that were axioms in earlier presentations—relative function extensionality, the homotopy extension property—are theorems here.","Univalence implies contractible Glue data along every cofibration, so Glue types no longer need to be assumed as primitive cubical structure.","A weak Glue structure, requiring only inner equalities at the boundary and mere maps, is strong enough to imply univalence on a path interval.","The paper's comparison of the internal theories HoTT + (int) and Cub shows that gluing and univalence are inter-derivable over a path interval, pointing toward the open conservativity question."],"fun_headline_variants":["Extension types for free in two-level type theory","Cubical gluing and univalence proven equivalent","Unified extension-type calculus, no new axioms","Two-level type theory makes extension types definable"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The whole derivation leans on the conversion from the inner to the outer level preserving Π, Σ, and the unit type on the nose; if that preservation were only up to homotopy, the strict boundary equality f∘i =s a in the extension type would need coercions and the strict extension-type rules would not follow automatically.","fun_headline_variants_meta":{"raw":{"variants":["Extension types for free in two-level type theory","Cubical gluing and univalence proven equivalent","Unified extension-type calculus, no new axioms","Two-level type theory makes extension types definable"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000144,"raw_usage":{"total_tokens":1075,"prompt_tokens":873,"completion_tokens":202,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":617,"completion_tokens_details":{"reasoning_tokens":142}},"tokens_in":617,"tokens_out":202,"duration_ms":2924,"temperature":1.0,"reasoning_tokens":142,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-01T08:17:48.044811+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Construct or locate a model of two-level type theory that satisfies the chosen axioms except that the inner-to-outer conversion preserves Π and Σ only up to homotopy, and check whether the boundary rule for the naive strict-fiber extension type still holds; the paper's Theorem 3.2 predicts it fails without on-the-nose preservation. Separately, any model with a path interval and a weak Glue structure but a non-univalent universe would directly contradict the paper's Theorem 5.14.","supporting_citations":[],"review_version":1}