{"id":"e408e19a-8fca-41fd-85a3-9341ca2caf3a","arxiv_id":"2505.13495","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Impredicative encodings of W-types and M-types are proven to satisfy the eta rules and induction and coinduction, extending AFS18.","lead":"This thesis extends a known trick for making System F style data types satisfy induction and bisimulation, and applies it to W-types and M-types. It shows that impredicative encodings can carry full induction and coinduction if one builds the uniqueness rules into the type definitions.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Unproven ExistsId axiom is load-bearing for the coinductive half: without it, Lemmas 6.4.12 and 9.4.12 fail, so the M-type eta rule and bisimulation theorem are conditional.","rationale":"The reader identified ExistsId as the weakest assumption, and the stress-test agrees. The coinductive theorems in Sections 9.4 and 9.5 are the paper's headline novelty, and they depend on the axiom in a place that cannot be patched by β-reduction or by the quotient machinery. The W-type induction results are independent and are supported by a plausible initial-algebra argument, so the overall thesis is best read as conditional rather than rejected. The reader's verdict of CONDITIONAL with moderate confidence is the appropriate assessment. I also considered whether the non-equivalence of CoLimStr/CoLimM or the omitted well-definedness proofs in the bisimulation theorems might be more damaging. Those are genuine technical gaps, but they appear repairable: the quotient construction intentionally works with non-equivalence relations, and the omitted proofs are routine consequences of EqCls2 and the relevant β-rules. The unproved ExistsId axiom is the single most load-bearing concern because it is an explicit logical assumption that the central coinductive result silently imports. A successful proof or a failed countermodel for ExistsId would directly determine whether the coinductive contribution is a theorem or a conditional construction.","tokens_in":51768,"tokens_out":13636,"duration_ms":143821,"concrete_test":"Formalize the system of Appendix C in a proof assistant (e.g. Coq or Agda) with the given Π, Σ, identity types, FunExt, and UIP, but without adding Axiom 6.1.4, and attempt to prove ExistsId. If the goal cannot be closed, construct a PER/parametricity model of the impredicative system in which the interpretation of Axiom 6.1.4 fails; such a model would settle that ExistsId is an independent axiom and hence that the Stream and M-type eta/bisimulation theorems are conditional on a genuine extra postulate.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central coinductive claim—that impredicative Streams and M-types satisfy their eta rules and hence bisimulation—rests on Axiom 6.1.4 (ExistsId), which is asserted but not proved. The axiom states that rec∃ (∃X.P) pack = id∃X.P. This is used in Lemma 6.4.12 to relate an arbitrary existential stream to the stream obtained by re-packing its unpacked components, and in Lemma 9.4.12 to do the same for M-types. From there Lemma 9.4.13 (corecM MAB elimM = idMAB), Theorem 9.4.14 (eta rule), and Theorem 9.5.4 (coinduction/bisimulation) all follow. Without ExistsId, the chain breaks: the proof that corec and the identity are related by CoLim fails, so the eta rules for Stream and M-types are not established. The issue is not merely cosmetic: the system's existential type is an impredicative Church encoding, and ExistsId is an extensional eta principle for that encoding, not a β-rule. For an arbitrary e : ∃X.P, the equation e(∃X.P) pack = e does not follow by β-reduction and is not obviously derivable from FunExt and UIP. The thesis itself acknowledges the axiom is unproven. Since the paper's stated contribution is to construct rather than postulate the relevant principles, the unproved status of ExistsId is a real gap in the coinductive half. The inductive W-type results do not depend on this axiom and appear to be on much firmer ground.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The manuscript, a formatted master's thesis, extends the Awodey–Frey–Speight (AFS18) technique for impredicative encodings of inductive types to a wider class of inductive and coinductive types. Working in an intensional type theory with an impredicative universe, Σ-types, identity types, function extensionality, and UIP, it defines impredicative encodings of lists, quotients, W-types, streams, and M-types, and proves the corresponding η-rules and (co)induction principles. The inductive half (lists, quotients, W-types) is developed in detail with explicit proof terms. The coinductive half (streams, M-types) uses a dual quotient construction, but its central theorems rest on an unproved axiom ExistsId (Axiom 6.1.4), and the M-type bisimulation definition contains a well-formedness defect.","tokens_in":52109,"tokens_out":17380,"duration_ms":150221,"significance":"The inductive half of the paper is a substantive and largely self-contained extension of AFS18: the W-type construction with its induction principle (Theorems 8.4.8 and 8.5.5) is a genuine generalization, and the list and quotient chapters provide clear, reusable templates. The paper is also notably transparent: it names ExistsId as an axiom, discusses the non-equivalence of CoLimStr, and flags omitted proofs. If the coinductive gaps are repaired, or the claims are explicitly made conditional, the stream and M-type constructions would be a valuable contribution to the study of impredicative encodings. As it stands, however, the coinductive half is not self-contained: the central theorems depend on an unproved extensionality axiom, and the M-type bisimulation definition is ill-formed.","major_comments":[{"comment":"The unproved axiom ExistsId is load-bearing for the coinductive results. It is first used in Lemma 6.4.12 to decompose an arbitrary σ : Stream∗ as corec∗s X h t x, and again in Lemma 9.4.12 for M∗AB; Lemmas 6.4.13, 9.4.13, Theorems 6.4.14, 9.4.14, and the coinduction theorems 6.5.4 and 9.5.4 all depend on these decompositions. The axiom is an η-rule for the Church-encoded existential type, not a β-rule, and no derivation from FunExt and UIP is provided. Since Chapter 3 identifies the paper's goal as defining rather than postulating, this makes the coinductive half conditional. The authors should either prove ExistsId or restate the stream and M-type theorems as conditional on it and adjust the abstract and conclusion accordingly.","section":"Sec. 6.1 / Axiom 6.1.4"},{"comment":"The predicate IsBisimM as written contains an unbound variable b in the conjunct R ((pr2 (elimM m)) b) ((pr2 (elimM n)) b). No binder for b, and no equality between the labels pr1 (elimM m) and pr1 (elimM n), is supplied, so the definition is not well-formed. Consequently Theorem 9.5.4, which builds on this definition, is not a well-typed statement. The definition needs a dependent reformulation, for example by transporting the second projection along the label equality and quantifying over the appropriate B-type.","section":"Definition 9.5.1"},{"comment":"The coinduction proofs omit the well-definedness proofs for the maps they lift to quotients: Theorem 6.5.4 states that the proofs for hd and cls∼∘tl are omitted, and Theorem 9.5.4 states that the well-definedness of elimX is 'almost identitcal' to Lemmas 9.4.5 and 9.4.6 and is omitted. These maps are load-bearing: without them, corecs (Stream/∼) hd cls∼∘tl and corecM (MAB/∼) elimX are not defined, and the commuting diagrams in the proofs do not type-check. Please provide these proofs in full.","section":"Theorems 6.5.4 and 9.5.4"},{"comment":"The statement of Lemma 9.4.6 compares cls (pr2 (elimM∗ m)) and cls (pr2 (elimM∗ n)) without accounting for the fact that these functions have domains B(pr1 (elimM∗ m)) and B(pr1 (elimM∗ n)). Under m≡n, Lemma 9.4.5 gives an equality of the labels, but the lemma and the subsequent definition of elimM require explicit transport of the second projection along that equality, or a formulation that first pairs the labels. As stated, the equality in Lemma 9.4.6 is not well-typed.","section":"Lemma 9.4.6"}],"minor_comments":[{"comment":"The prose says '(corec∗s Stream∗ hd∗ tl∗ (cls σ)) and (corec∗s Stream hd tl σ)' are related, but equation (6.14) states a relation between (corec∗s Stream∗ hd∗ tl∗ σ) and (corec∗s Stream hd tl (cls σ)); these do not match.","section":"Lemma 6.4.11"},{"comment":"The lemma and surrounding text use cls for both the class map D→D/R and its lift D/R→D/R, so the statement 'cls = idD/R' is type-ambiguous; please use separate notations for the two maps.","section":"Lemma 5.3.6"},{"comment":"The line 'hd := hd∗ := recq E hd∗ EqHd' overloads hd∗; please use distinct names for the original head function and its quotient lift.","section":"Definition 6.4.7"},{"comment":"The name '1W∗' is introduced twice in the example; the third definition is presumably meant to be '2W∗'.","section":"Example 8.2.3"},{"comment":"Steps 5 and 6 of the proof refer to 'idList' in the W-type context, where the intended term is idWAB.","section":"Theorem 8.5.5"},{"comment":"The section title contains a typo: 'priciple' should be 'principle'.","section":"Section 5.4"},{"comment":"Two inference rules are labelled 'Σ-form1'; the second should presumably be 'Σ-form2'.","section":"Definition 3.2.2"}],"recommendation":"major_revision","confidential_remarks":null},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"I mostly agree with the reader's take, and the stress-test note is accurate. What is actually new: the thesis extends Awodey–Frey–Speight to W-types, answering an open question from Speight's thesis, and it dualizes the construction to streams and M-types via a quotient. The inductive side — lists, quotients, W-types — is worked out in enough detail that I believe it is correct. The W-induction theorem (8.5.5) goes through with FunExt and UIP, and it does not depend on the problematic axiom. That is a solid contribution.\n\nThe soft spot is exactly where the stress-test puts it: Axiom 6.1.4 (ExistsId) is asserted, not proved, and it is load-bearing for the entire coinductive half. It appears in Lemma 6.4.12 and Lemma 9.4.12, and from there in the eta rules and the bisimulation theorems for Stream and M. The authors are honest — they flag it and even suggest it might be provable for a better existential type — but as it stands, the headline claims about streams and M-types are conditional on an unproven postulate. The omitted well-definedness proofs in Theorems 6.5.4 and 9.5.4 are a smaller issue, but real: those are not cosmetic steps, and since the rest of the thesis is so detailed, the omission stands out.\n\nI would also note that the coinductive relation CoLimStr is not an equivalence relation (Appendix D confirms this), and reflexivity itself already requires ExistsId. The quotient construction depending on Note 5.1.8 is fine in principle, but it is worth a referee asking whether the quotient hides any extra assumptions beyond what is stated.\n\nNo machine-checked formalization is provided. That is not a flaw by itself, but given the axiom and the omitted proofs, formalizing the inductive half would be a quick way to raise confidence.\n\nBottom line: this deserves a serious referee. The inductive results are likely correct and worth publishing; the coinductive results should be clearly presented as conditional on ExistsId, or the author should prove or circumvent the axiom. I would send it to peer review and let the referees ask for either a proof of ExistsId or a softened statement of the coinductive theorems.","headline":"The inductive half (W-types, lists, quotients) is a genuinely useful extension of AFS18 and appears sound; the coinductive half (streams, M-types) is a real advance but currently rests on an unproven ExistsId axiom, so the bisimulation results are conditional.","tokens_in":52648,"tokens_out":1692,"would_cite":true,"duration_ms":19317,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"W-types and M-types defined impredicatively with induction and bisimulation principles","keywords":["impredicative encodings","W-types","M-types","induction principle","coinduction","bisimulation","eta rules","quotient types"],"falsifier":"Build a model of the type system in which all rules hold except ExistsId, with some $P$ and some $t:\\exists X.P$ for which $\\mathrm{rec}_{\\exists}(\\exists X.P)\\,\\mathrm{pack}\\, t \\neq t$; in that model Lemma 9.4.12 would fail, so the M-type corecursor identity and the coinduction theorem would fail as well.","tokens_in":1817,"feed_emoji":"","tokens_out":2540,"duration_ms":98651,"temperature":0.7,"pith_summary":"This thesis tries to close a known gap in impredicative type theory: the usual System F encodings of data types satisfy computation rules but not the uniqueness (eta) rules that would deliver induction and coinduction principles. It extends a 2018 technique in which the eta rule is built into the type by carving out a subtype for inductive types, and applies that construction to lists and quotients, then to W-types, establishing an induction principle for the generic inductive form. It then dualises the technique, using quotients instead of subtypes, to streams and to M-types, establishing a coinduction (bisimulation) principle for the generic coinductive form. A fair reader would take the central claim to be that the same encoding recipe works on both halves of the inductive/coinductive duality, at the cost of one auxiliary axiom about existential types.","feed_headline":"W-types and M-types gain induction and bisimulation principles","feed_subtitle":"Encoding uniqueness into the type definitions makes W-types and M-types proper initial and final algebras.","key_machinery":"The machinery is the pair of encodings. For inductive types, the impredicative W-type $W^{*}(a:A).B(a) := \\Pi(X:U).(\\Pi(a:A).(B(a)\\to X)\\to X)\\to X$ is restricted to a subtype by the predicate $\\mathrm{LimW}$, which requires all W-algebra morphisms to commute with the recursor. For coinductive types, the impredicative M-type $M^{*}(a:A).B(a) := \\exists(X:U).\\, X \\times (X \\to \\Sigma(a:A).\\, B(a)\\to X)$ is quotiented by $\\mathrm{CoLimM}$, the relation of being connected by an M-coalgebra morphism to a repacked version. The quotient construction carries the stream and M-type side, and the load-bearing axiom ExistsId — that unpacking an existential type and repacking the extracted data is the identity — is what allows the proof that unpacking and repacking an existential is invisible. The same recipe also produces List and quotient types as warm-ups; the W-type half needs function extensionality, uniqueness of identity proofs, and the subtype construction, while the M-type half needs the existential axiom.","core_discovery":"The central claim is that the 2018 impredicative encoding strategy is not limited to the simple inductive types treated in the original paper. By pairing each impredicative W-type with a proof that every algebra morphism commutes with the recursor, the paper defines a subtype $W(a:A).B(a)$ that is the initial algebra of the W-functor, hence satisfies the eta rule, and from that eta rule derives an induction principle (Theorem 8.5.5). Dualising, the paper forms $M(a:A).B(a)$ as a quotient of the impredicative M-type by the relation “one M-type is carried to the other by a coalgebra morphism,” and proves the quotient is the final coalgebra; the resulting eta rule yields a coinduction principle, also called bisimulation, for M-types (Theorem 9.5.4), with streams as the special case $A=E$, $B=\\lambda e.1$. In both halves the encoding works by forcing the uniqueness property of the (co)limit into the definition itself, rather than postulating an induction or coinduction axiom.","pith_inferences":["A natural next step the paper leaves open is to formalise the encodings in a proof assistant; such a formalisation would either prove ExistsId from the other rules or show exactly where it is needed.","If ExistsId is provable for a better-behaved existential type, the coinductive half would become axiom-free; one test is to replace the impredicative existential with a version whose equality is computed from the packed witness.","The same limit/colimit recipe suggests that higher inductive and higher coinductive types could be encoded by dropping uniqueness of identity proofs and using a notion of set, since the subtype and quotient constructions need the uniqueness principles rather than strict proof irrelevance.","Because the relation CoLimStr is neither symmetric nor transitive, the quotient side relies on quotient equality only observing the equivalence closure; a reader wanting to reuse the construction for other relations should check this point explicitly."],"forward_implications":["Every inductive type expressible as a W-type—natural numbers, lists, well-founded trees—inherits a constructed induction principle rather than requiring induction as an axiom.","Every coinductive type expressible as an M-type—streams, possibly infinite lists, non-well-founded trees—inherits a bisimulation principle, so two inhabitants with matching destructor behaviour are propositionally equal.","The quotient-type encoding yields a surjective class map and an induction principle for quotients, so the technique handles quotient constructions inside the same system.","The stream case is a corollary of M-types, since Stream is $M(e:E).1$, so the earlier stream construction is subsumed by the generic M-type construction.","Because W-types and M-types are the generic forms of inductive and coinductive types, the result transfers the encoding recipe from individual examples to a general schema for positive functors."],"supporting_citations":[{"why":"Supplies the subtype-based impredicative encoding technique that this thesis extends, and the categorical reading of the encodings as initial algebras.","marker":"[AFS18]"},{"why":"Poses the W-type and M-type questions and details the type-theoretic system of universes, sigma types, equality types, and axioms used throughout.","marker":"[Spe17]"},{"why":"Provides System F and the representation of free structures that give the base impredicative definitions of lists and other data types.","marker":"[GTL93]"},{"why":"Shows induction is not derivable for System F style inductive types, motivating the need for the eta-rule encodings.","marker":"[Geu01]"},{"why":"Supplies the categorical algebra/coalgebra and bisimulation framework used to identify the initial algebra and final coalgebra that the encodings mimic.","marker":"[JR12]"},{"why":"Introduces W-types as wellorderings and supplies the inductive construction that is generalised in the W-type chapter.","marker":"[MS84]"},{"why":"Supplies M-types and their bisimulation treatment, the coinductive counterpart that is generalised in the M-type chapter.","marker":"[Ott20]"},{"why":"Provides the identity types, sigma types, universe hierarchy, and W-type background on which the presentation relies.","marker":"[HOT13]"}],"fun_headline_variants":["Impredicative encodings gain uniqueness for W and M types","Subtypes and quotients make impredicative types initial and final","W-type induction and M-type bisimulation via subtype and quotient","Eta rules for impredicative W and M types from uniqueness"],"cache_read_input_tokens":54656,"weakest_assumption_plain":"The load-bearing premise is the unproved ExistsId axiom—that unpacking an existential type and repacking the extracted data returns the original—because without it the proofs that streams and M-types satisfy their uniqueness rules collapse.","fun_headline_variants_meta":{"raw":{"variants":["Impredicative encodings gain uniqueness for W and M types","Subtypes and quotients make impredicative types initial and final","W-type induction and M-type bisimulation via subtype and quotient","Eta rules for impredicative W and M types from uniqueness"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.00017,"raw_usage":{"total_tokens":1301,"prompt_tokens":1013,"completion_tokens":288,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":629,"completion_tokens_details":{"reasoning_tokens":211}},"tokens_in":629,"tokens_out":288,"duration_ms":3171,"temperature":1.0,"reasoning_tokens":211,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T21:14:40.848643+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Build a model of the type system in which all rules hold except ExistsId, with some $P$ and some $t:\\exists X.P$ for which $\\mathrm{rec}_{\\exists}(\\exists X.P)\\,\\mathrm{pack}\\, t \\neq t$; in that model Lemma 9.4.12 would fail, so the M-type corecursor identity and the coinduction theorem would fail as well.","supporting_citations":[],"review_version":1}