pith. sign in

arxiv: 2602.18921 · v2 · submitted 2026-02-21 · 💻 cs.LO

Constructing (Co)inductive Types via Large Sizes

Bastiaan Laarakker , Dani\"el Otten , Benno van den Berg This is my paper

Pith reviewed 2026-05-15 21:04 UTC · model grok-4.3

classification 💻 cs.LO
keywords sized typesinductive typescoinductive typesintensional type theoryrealisability modelparametric quantifiersterminationproductivity
0
0 comments X

The pith

Inductive and coinductive types can be constructed in intensional type theory by adding a large type of sizes and parametric quantifiers over sizes.

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

The paper extends intensional type theory with a large type of sizes and parametric quantifiers. This extension supports the construction of both inductive and coinductive types, going beyond earlier work limited to finitely-branching inductive types. Size annotations combined with well-founded induction on sizes establish termination of recursive functions and productivity of corecursive functions. The method replaces restrictive syntactic checks with type-based reasoning in proof assistants. Consistency follows from an impredicative realisability model that interprets the type of sizes as an uncountable ordinal.

Core claim

Inductive and coinductive types can be constructed in this theory, which improves on earlier work where this was only possible for the finitely-branching inductive types. The consistency of the theory is justified by an impredicative realisability model, which interprets the type of sizes as an uncountable ordinal.

What carries the argument

The large type of sizes together with parametric quantifiers over sizes. These provide annotations for (co)inductive types and support well-founded induction to prove termination and productivity.

Load-bearing premise

The consistency of the extended theory rests on the existence and soundness of an impredicative realisability model that interprets the type of sizes as an uncountable ordinal.

What would settle it

Constructing or exhibiting an inconsistency in the theory that the realisability model cannot validate, or showing that no sound impredicative realisability model exists interpreting sizes as an uncountable ordinal.

read the original abstract

To ensure decidability and consistency of its type theory, a proof assistant should only accept terminating recursive functions and productive corecursive functions. Most proof assistants enforce this through syntactic conditions, which can be restrictive and non-modular. Sized types are a type-based alternative where (co)inductive types are annotated with additional size information. Well-founded induction on sizes can then be used to prove termination and productivity. An implementation of sized types exists in Agda, but it is currently inconsistent due to the addition of a largest size. We investigate an alternative approach, where intensional type theory is extended with a large type of sizes and parametric quantifiers over sizes. We show that inductive and coinductive types can be constructed in this theory, which improves on earlier work where this was only possible for the finitely-branching inductive types. The consistency of the theory is justified by an impredicative realisability model, which interprets the type of sizes as an uncountable ordinal.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

3 major / 3 minor

Summary. The manuscript extends intensional type theory with a large type of sizes and parametric quantifiers over sizes. It shows that both inductive and coinductive types, including infinitely branching variants, can be constructed internally in this theory, improving on prior work restricted to finitely-branching inductive types. Consistency of the extension is justified by exhibiting an impredicative realisability model in which the type of sizes is interpreted as an uncountable ordinal.

Significance. If the construction and model hold, the result offers a modular, type-based alternative to syntactic termination checks, enabling more general (co)inductive definitions in proof assistants. The semantic consistency argument via realisability model is a clear strength, providing an external justification without self-referential definitions, though the lack of syntactic normalization or machine-checked verification limits immediate usability.

major comments (3)
  1. [§4.2] §4.2, Model Definition 4.5: The interpretation of parametric quantifiers ∀^p over the large size type (as an uncountable ordinal) is only sketched; the proof that this preserves soundness for coinductive encodings must be expanded, as any gap here would undermine the consistency claim for infinitely-branching cases.
  2. [§3.3] §3.3, Construction 3.12: The encoding of infinitely-branching coinductive types relies on the interaction between the large size type and parametric quantification, but it is unclear whether the productivity condition is enforced without additional well-foundedness assumptions on the ordinal interpretation.
  3. [§5] §5, Theorem 5.3: The claim that the realisability model validates the full extended theory (including size polymorphism) lacks a detailed case analysis for the coinductive constructors; this is load-bearing for the central consistency argument.
minor comments (3)
  1. [§2.1] Notation for the parametric quantifier ∀^p is introduced without an explicit comparison to standard ∀ in §2.1; a small table contrasting the two would improve readability.
  2. [§4.1] The abstract mentions an 'uncountable ordinal' for sizes, but the precise ordinal (e.g., ω_1 or larger) is not stated until §4.1; move this clarification earlier.
  3. [Introduction] Reference to Agda's inconsistent largest-size implementation is given, but no citation to the specific Agda issue or paper is provided in the introduction.

Simulated Author's Rebuttal

3 responses · 0 unresolved

We thank the referee for their thorough review and constructive comments. We address each major comment below and will revise the manuscript accordingly to expand the relevant proofs and clarifications.

read point-by-point responses

  1. Referee: [§4.2] §4.2, Model Definition 4.5: The interpretation of parametric quantifiers ∀^p over the large size type (as an uncountable ordinal) is only sketched; the proof that this preserves soundness for coinductive encodings must be expanded, as any gap here would undermine the consistency claim for infinitely-branching cases.

    Authors: We agree that the interpretation of parametric quantifiers in Definition 4.5 is presented concisely and requires a fuller proof. In the revised manuscript we will expand this section with a detailed argument showing that the uncountable ordinal interpretation preserves the required soundness properties, with explicit verification for coinductive encodings in the infinitely-branching case. revision: yes

  2. Referee: [§3.3] §3.3, Construction 3.12: The encoding of infinitely-branching coinductive types relies on the interaction between the large size type and parametric quantification, but it is unclear whether the productivity condition is enforced without additional well-foundedness assumptions on the ordinal interpretation.

    Authors: Productivity is enforced directly by the parametric quantifiers ranging over the large size type; the model’s interpretation of sizes as an uncountable ordinal already supplies the necessary well-foundedness. We will revise Section 3.3 to spell out this interaction explicitly, making clear that no further assumptions are introduced. revision: yes

  3. Referee: [§5] §5, Theorem 5.3: The claim that the realisability model validates the full extended theory (including size polymorphism) lacks a detailed case analysis for the coinductive constructors; this is load-bearing for the central consistency argument.

    Authors: We acknowledge that the proof of Theorem 5.3 would benefit from an expanded case analysis for the coinductive constructors. The revised manuscript will include this detailed case-by-case verification under size polymorphism, thereby completing the consistency argument. revision: yes

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper extends intensional type theory with a large type of sizes and parametric quantifiers, then constructs inductive and coinductive types (including infinitely branching) inside this theory. Consistency is justified by exhibiting an impredicative realisability model that interprets the size type as an uncountable ordinal. This is an independent semantic argument supplied for the extended theory rather than a self-referential definition, fitted parameter renamed as prediction, or load-bearing self-citation chain. No equation or step reduces by construction to its own inputs, and the derivation remains self-contained against the provided model.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The central claim rests on the addition of a large type of sizes and the soundness of an impredicative realisability model; no free parameters are mentioned.

axioms (1)
  • domain assumption An impredicative realisability model exists that interprets the type of sizes as an uncountable ordinal and establishes consistency of the extended theory.
    Invoked to justify consistency of the new type theory.
invented entities (1)
  • Large type of sizes no independent evidence
    purpose: To provide size annotations for (co)inductive types enabling well-founded induction proofs of termination and productivity.
    New primitive introduced in the type theory extension.

pith-pipeline@v0.9.0 · 5471 in / 1232 out tokens · 20184 ms · 2026-05-15T21:04:32.230042+00:00 · methodology

discussion (0)

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

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

15 extracted references · 15 canonical work pages · 1 internal anchor

  1. [1]

    2 Andreas Abel.Type-based termination: a polymorphic lambda-calculus with sized higher-order types

    Applied Semantics: Selected Topics.doi:10.1016/j.tcs.2005.06.002. 2 Andreas Abel.Type-based termination: a polymorphic lambda-calculus with sized higher-order types. PhD thesis, Ludwig-Maximilians-Universität München,

    work page doi:10.1016/j.tcs.2005.06.002 2005

  2. [2]

    Semi-continuous sized types and termination.Log

    3 Andreas Abel. Semi-continuous sized types and termination.Log. Methods Comput. Sci., 4(2), 2008.doi:10.2168/LMCS-4(2:3)2008. 4 Andreas Abel. Miniagda: Integrating sized and dependent types. InPartiality and Recursion in Interactive Theorem Provers, PAR@ITP 2010, Edinburgh, UK, July 15, 2010, EPiC Series, pages 18–33. EasyChair, 2010.doi:10.29007/322Q. 1...

    work page doi:10.2168/lmcs-4(2:3)2008 2008

  3. [3]

    6 Andreas Abel

    doi:10.4204/EPTCS.77.1. 6 Andreas Abel. Compositional coinduction with sized types. InCoalgebraic Methods in Computer Science, Lecture Notes in Computer Science, pages 5–10. Springer, 2016.doi: 10.1007/978-3-319-40370-0\_2. 7 Andreas Abel, Andrea Vezzosi, and Théo Winterhalter. Normalization by evaluation for sized dependent types.Proc. ACM Program. Lang....

    work page doi:10.4204/eptcs.77.1 2016

  4. [4]

    13 Gilles Barthe, Benjamin Gregoire, and Fernando Pastawski

    doi:10.1017/S0960129503004122. 13 Gilles Barthe, Benjamin Gregoire, and Fernando Pastawski. CIC.: Type-based termination of recursive definitions in the calculus of inductive constructions. InMath. Struct. in Comp. Science, pages 257–271, 11 2006.doi:10.1007/11916277_18. 14 Lars Birkedal, Ales Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, a...

    work page doi:10.1017/s0960129503004122 2006

  5. [5]

    [GLL23] Cinzia Di Giusto, Laetitia Laversa, and ´Etienne Lozes

    23 Marcelo P. Fiore, Andrew M. Pitts, and S. C. Steenkamp. Constructing infinitary quotient- inductive types. InFoundations of Software Science and Computation Structures - 23rd International Conference, Proceedings, Lecture Notes in Computer Science, pages 257–276. Springer, 2020.doi:10.1007/978-3-030-45231-5\_14. 24 Healfdene Goguen, Conor McBride, and ...

    work page doi:10.1007/978-3-030-45231-5 2020

  6. [6]

    doi:10.1007/11780274_27

    Series Title: Lecture Notes in Computer Science. doi:10.1007/11780274_27. 25 Martin Hofmann.Syntax and Semantics of Dependent Types, page 79–130. Publications of the Newton Institute. Cambridge University Press,

    work page doi:10.1007/11780274_27

  7. [7]

    Jones, and Amir M

    28 Chin Soon Lee, Neil D. Jones, and Amir M. Ben-Amram. The size-change principle for program termination. InConference Record of POPL 2001: The 28th ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages, London, UK, January 17-19, 2001, pages 81–92. ACM, 2001.doi:10.1145/360204.360210. 29 Xavier Leroy. Well-founded recursion done right. In...

    work page doi:10.1145/360204.360210 2001

  8. [8]

    Equations for Hereditary Substitution in Leivant's Predicative System F: A Case Study

    ACM. 30 Cyprien Mangin and Matthieu Sozeau. Equations for hereditary substitution in leivant’s predicative System F: A case study.CoRR, abs/1508.00455, 2015.arXiv:1508.00455. 31 Rasmus Ejlers Møgelberg. A type theory for productive coprogramming via guarded recursion. InProceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Comput...

    work page internal anchor Pith review Pith/arXiv arXiv 2015

  9. [9]

    Association for Computing Machinery.doi:10.1145/2603088.2603132. 32 H. Nakano. A modality for recursion. InProceedings Fifteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No.99CB36332), pages 255–266, 2000.doi:10.1109/LICS. 2000.855774. 33 Andreas Nuyts and Dominique Devriese. Degrees of relatedness: A unified framework for parametricity, i...

    work page doi:10.1145/2603088.2603132 2000

  10. [10]

    35 Bernhard Reus

    doi:10.1145/3110276. 35 Bernhard Reus. Realizability models for type theories.Electronic Notes in Theoretical Computer Science, 23(1):128–158,

    work page doi:10.1145/3110276

  11. [11]

    37 Jorge Luis Sacchini

    North-Holland. 37 Jorge Luis Sacchini. Type-based productivity of stream definitions in the calculus of construc- tions. In2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 233–242, 2013.doi:10.1109/LICS.2013.29. 20 Constructing (Co)inductive Types via Large Sizes 38 Jorge Luis Sacchini. Linear sized types in the calculus of construc...

    work page doi:10.1109/lics.2013.29 2013

  12. [12]

    40 Matthieu Sozeau and Cyprien Mangin

    Series Title: Lecture Notes in Computer Science.doi:10.1007/978-3-642-14052-5_29. 40 Matthieu Sozeau and Cyprien Mangin. Equations reloaded: High-level dependently-typed functional programming and proving in Coq.Proceedings of the ACM on Programming Languages, 3(ICFP):1–29,

    work page doi:10.1007/978-3-642-14052-5_29

  13. [13]

    Cubical assemblies, a univalent and impredicative universe and a failure of propositional resizing

    42 Taichi Uemura. Cubical assemblies, a univalent and impredicative universe and a failure of propositional resizing. In24th International Conference on Types for Proofs and Programs, TYPES 2018, Braga, Portugal, June 18-21, 2018, LIPIcs, pages 7:1–7:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.doi:10.4230/LIPICS.TYPES.2018.7. 43 The Unival...

    work page doi:10.4230/lipics.types.2018.7 2018

  14. [14]

    46 Antoine Van Muylder, Andreas Nuyts, and Dominique Devriese

    Agda GitHub repository, Issue #3026. 46 Antoine Van Muylder, Andreas Nuyts, and Dominique Devriese. Internal and observational parametricity for cubical Agda.Proc. ACM Program. Lang., 8(POPL), January 2024.doi: 10.1145/3632850. 47 Jaap van Oosten.Realizability, Volume 152: An Introduction to its Categorical Side. Elsevier Science, San Diego, CA, USA,

    work page doi:10.1145/3632850 2024

  15. [15]

    Guarded Recursion in Agda via Sized Types

    48 Niccolò Veltri and Niels van der Weide. Guarded Recursion in Agda via Sized Types. In4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), volume 131 ofLeibniz International Proceedings in Informatics (LIPIcs), pages 32:1–32:19, Dagstuhl, Germany,

    work page 2019