Pith. sign in

REVIEW 1 major objections 8 minor 47 references

Setoids in Intensional Type Theory

T0 review · 1 major / 8 minor · reviewed 2026-07-30 · grok-4.5

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

Pith's one-line read A simple notion of displayed setoids inside intensional type theory supplies a full semantics for extensional type theory with universes and proves its consistency.

desk verdict Pitts finishes the unfinished Palmgren program: a complete, Agda-checked setoid semantics of ETU inside IRU, with a relative consistency corollary. read the letter →

arxiv 2607.23671 v2 pith:WPW3FV4W submitted 2026-07-26 cs.LO

Andrew M. Pitts This is my paper · ORCID
classification cs.LO MSC 03B1503F5068V15
keywords setoidsdisplayedintensionaltypetheoryextensionaluniversesinductive-recursivedefinitionsrelativeconsistencyAgda
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

The paper constructs, inside a strictly intensional meta-theory, a model of full extensional Martin-Löf type theory with a hierarchy of universes. The meta-theory is safe Agda without axiom K, equipped with a universe closed under inductive-recursive definitions. Object-theory syntax is given extrinsically via a well-scoped locally nameless representation; its meaning is given by type-valued semantic relations on raw terms that are proved total and single-valued precisely on the well-formed judgments. The model uses a deliberately simple notion of displayed setoid (a family equipped with a heterogeneous equivalence plus coercion maps). As a corollary one obtains a machine-checked proof that the extensional theory is consistent relative to the intensional one. A reader cares because the result shows how much classical extensional reasoning can be recovered, and verified, without ever leaving a purely intensional foundation.

What carries the argument

Displayed setoids: families of types over a base setoid carrying a heterogeneous equivalence relation together with coercion and coherence operations. Combined with an inductively-recursively defined hierarchy of setoid universes of codes, they interpret contexts, types, terms and definitional equality.

What would settle it

Exhibit a well-typed IRU term of type “there exists a raw term a such that the empty context derives a : Emp”, or show that the Agda formalization of totality or single-valuedness fails to type-check.

Watch

Extended reading notes

Core claim

Inside IRU (safe Agda), the displayed-setoid model interprets every well-formed judgment of extensional type theory with universes soundly for definitional equality; consequently there exists an IRU term proving that the empty type is uninhabited in the empty context of the extensional theory.

Load-bearing premise

The whole consistency claim is only relative to the meta-theory; it stands only if safe Agda with inductive-recursive definitions is itself consistent and faithfully represents the intended intensional type theory.

Editorial extensions

If this is right

  • Extensional type theory with universes is consistent relative to intensional type theory plus induction-recursion.
  • The simple displayed-setoid notion is strong enough to interpret a full cumulative hierarchy of universes without proof-irrelevant propositions.
  • Further relative-consistency results about extensionality principles can now be attempted inside a machine-checked intensional setting.
  • Semantic constructions that classically rely on extensional equality become candidates for fully formal intensional development.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The same infrastructure supplies a foundation for intensional versions of gluing or normalization-by-evaluation arguments for dependent type theories.
  • The displayed-setoid universes can likely host other extensional features (function extensionality plus uniqueness of identity proofs) without leaving the meta-theory.
  • Because every definition and proof is machine-checked, the development can serve as a reference for comparing competing notions of setoid in the literature.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

1 major / 8 minor

Summary. The paper constructs, inside intensional type theory with a universe closed under inductive-recursive definitions (IRU, realized as Agda with --safe --without-K), a setoid-based model of extensional type theory with a countable hierarchy of universes (ETU). The syntax of ETU is given extrinsically using a well-scoped locally nameless representation. The semantics uses a simplified notion of displayed setoid (Definition 3.2): a type-valued heterogeneous equivalence relation over a base equivalence, with cartesian rather than path-over products in comprehension, plus coe/coh operations. Inductive-recursive definitions supply setoid universes of codes for types (§4.1–4.2) and a novel setoid universe of codes for contexts (§4.3). Because IRU cannot express partial functions directly, the semantics is given via type-valued input-output relations, proved single-valued (Theorem 6.5) and total and sound for definitional equality (Theorem 6.7), from which proof-irrelevant semantic functions are extracted (§6.5). As a corollary, consistency of ETU is proved within IRU (Theorem 6.8). The entire development is machine-checked in Agda 2.8.0 and publicly available.

Significance. If the development checks as claimed — and the paper ships the complete machine-checked artifact (Pitts 2026a), which is a major strength — this closes a real gap: Palmgren (2022) gave setoid closure constructions but not the semantic functions or the soundness proof. The paper delivers a fully formalized Streicher-style semantics with the hard parts (single-valuedness of proof-relevant relations, totality, soundness for definitional equality) actually carried out in a bare-bones intensional meta-theory, plus a machine-checked relative consistency corollary. The simplified displayed setoid (Definition 3.2, replacing path-over products with cartesian products plus coe/coh) and the setoid universe of context codes (§4.3) appear to be genuinely new and reusable. The foundational point — that extensionality can be modelled inside a very weak intensional system — is of clear interest to the type-theory and formalized-metatheory communities, independent of applications.

major comments (1)
  1. The main corollary is stated as 'a proof within IRU of the consistency of ETU' (also Theorem 6.8 and the abstract). IRU is defined as Safe Agda with --without-K, plus a manual exclusion of coinductive types and proof-irrelevance annotations, which --safe itself permits (footnote 1). The internal mathematics is fully machine-checked, but the identification of the checked artifact with the advertised fragment IRU currently rests on an unmechanized, by-hand assurance. There is no textual evidence that forbidden features are used, and the fix is small: please (a) state explicitly that Semantics.Consistency and its transitive dependency closure contain no coinductive records, no Prop/@irrelevant annotations, and no module-level OPTIONS pragmas weakening --safe/--without-K, and ideally (b) ship a small script in the artifact that checks this mechanically. This is the only point touching the *
minor comments (8)
  1. [Abstract/§1] Terminology: the title and most of the text use 'intensional', but the abstract and several passages (e.g., p. 2, 'intentional type theory is logically quite weak') use 'intentional'. If the latter is a deliberate echo of Martin-Löf, please say so once; otherwise unify.
  2. [Definition 3.2, Eq. (15)] The type of coh is printed as (y : ∥B∥), but ∥B∥ : |A| → Set, so this is ill-formed as printed; it should be (y : ∥B∥ x). The Agda code presumably has the correct type.
  3. [§4.2, Eqs. (59)–(60)] Clauses (59) and (60) are copied from §4.1 without updating subscripts: they read Eq0 ... ∼0 and Pi+ ... ∼0, but should be Eq+ ... ∼+ and Pi+ ... ∼+. Similarly clause (43) omits the subscript on ≈0, and the html anchor 'SucessorUniverse' is misspelled.
  4. [§5/§6.2] The Agda-style universe rule for Π-types (Γ ⊢ Π_{l,l'} A B : U_{max l l'}) is first stated in §6.2 during the semantics; it belongs with the other formation rules in §5 (or at least a forward reference should be given).
  5. [Various] Typos: 'Defintion' (first line of §4); 'Foreward' → 'Foreword' (§1); duplicated 'can can' in Notation 2.1; 'transporing' → 'transporting' (§4.3); stray closing quote in 'engineering formal meta-theory"' (Conclusion).
  6. [References] The text cites 'Brunerie and de Boer (2020)' but the bibliography lists only 'M. de Boer, A Proof and Formalization of the Initiality Conjecture...' — please reconcile the citation (presumably G. Brunerie and M. de Boer).
  7. [§5, Figure 2] The cofinite-quantification notation ∀x y x#y#S ... used in Figure 2 could be glossed inline before first use; readers unfamiliar with the WSLN library may not parse x#y#S.
  8. [§3, after Definition 3.5] The remark that Π-structure on the strict CwF of displayed setoids satisfies η only up to setoid equality (and similarly for identity types) is important motivation for the universe-oriented approach of §6.1; a pointer to where in the artifact this limitation manifests (or a one-line example) would help readers.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: classic relative-consistency via an independently constructed setoid model in IRU.

full rationale

The paper’s central claim is a relative consistency result: ETU is interpreted in IRU via displayed setoids, and emptiness of Emp in the model yields an IRU term of type ¬(Σ[a∈Tm](⋄⊢a:₀ Emp)) (Theorem 6.8). The model (Sections 3–4, 6.1) is built from setoids, inductive-recursive universes, and semantic relations on raw syntax; it is not defined in terms of ETU derivability or consistency. Totality and soundness (Theorems 6.5–6.7) are proved by induction on judgments, then consistency follows because the interpretation of Emp is the empty type ∅. Self-citations (WSLN syntax library, accompanying Agda code) supply infrastructure only. No equation reduces the consistency statement to a fitted parameter, a self-justifying uniqueness theorem, or a renaming of the target. This is a standard, non-circular model-theoretic relative-consistency argument.

Assumptions & free parameters 0 free parameters · 5 assumptions · 2 invented entities

The result is a relative consistency theorem inside a fixed meta-theory. No numerical free parameters. Load-bearing background is standard Martin-Löf type theory with induction-recursion as realized by safe Agda, plus the chosen (simplified) definition of displayed setoid and the extrinsic ETU syntax. No new physical or mathematical entities beyond definitional constructions.

assumptions (5)
  • domain assumption IRU is the type theory of Agda with --safe and --without-K, with a universe closed under inductive-recursive definitions, and without coinduction or proof-irrelevance annotations.
    Section 2 fixes the meta-theory; all constructions and the consistency corollary live inside it. Consistency of IRU itself is not proved.
  • domain assumption Inductive-recursive definitions are admitted for defining setoid universes U_ℓ, Eℓ_ℓ and the context universe C simultaneously with their decoding and equivalence relations.
    Section 4; the paper notes this can be weakened (citing Altenkirch et al. and Pujet) but retains IR for conceptual simplicity.
  • standard math Standard rules of intensional Martin-Löf type theory: dependent functions with η, record types with η, identity types without K, empty/unit/nat types.
    Section 2; background of IRU.
  • domain assumption ETU is the extrinsic, well-scoped locally nameless presentation of Martin-Löf extensional type theory with a hierarchy of universes, Π, extensional Eq, Emp, Nat, as specified by the inductive judgments in Section 5.
    The object theory being modeled; adequacy relative to informal ETU is by design of the rules (Figs. 1–2 and ETU.Rules).
  • ad hoc to paper Displayed setoids use a cartesian product (A∋x∼x')×(B∋x,y≈x',y') rather than a dependent path-over product, with explicit coe/coh (Definition 3.2).
    Chosen simplification versus Palmgren Def. 3.8; adequacy is justified by the successful soundness proof, not by an independent theorem that all alternative notions work.
invented entities (2)
  • Simplified displayed setoid (ITU heterogeneous equivalence with coe/coh, Def. 3.2) independent evidence
    purpose: Provide families of setoids adequate to interpret dependent types and conversion in ETU without Prop or heavy coherence.
    Definitional construction inside IRU, not a postulated external object; independent evidence is the machine-checked model, not an external measurement.
  • Setoid universe C of context codes with display E (Section 4.3) independent evidence
    purpose: Interpret typing contexts and context equality uniformly with type codes.
    Inductive-recursive code system; new packaging relative to prior setoid universes focused on types.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Setoids in Intensional Type Theory." pith.science (2026). https://pith.science/paper/WPW3FV4W

@misc{pith2026260723671,
  author       = {Pith},
  title        = {Pith review of: Setoids in Intensional Type Theory},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/WPW3FV4W}},
  note         = {Machine review of arXiv:2607.23671}
}
read the original abstract

We show that a certain notion of displayed setoid (family of setoids) in intensional type theory can be used to give a semantics for extensional type theory with universes (ETU). Safe Agda serves as a machine-checkable formalization of intentional type theory augmented with a universe closed under inductive-recursive definitions (IRU). The syntax of ETU is defined in IRU in a traditional extrinsic form, using a well-scoped locally nameless representation of its terms. Giving the semantics of ETU in terms of displayed setoids is complicated by the very limited means of expression afforded by IRU. As a corollary we obtain a proof within IRU of the consistency of ETU.

Figures

Figures reproduced from arXiv: 2607.23671 by the authors.

Figure 1
Figure 1. Rules for extensional equality and the empty type [PITH_FULL_IMAGE:figures/full_fig_p017_1.png] view at source ↗
Figure 2
Figure 2. Some of the rules for the eliminator for the natural number type [PITH_FULL_IMAGE:figures/full_fig_p018_2.png] view at source ↗
Figure 3
Figure 3. Semantic relation constructors for equality types and reflexivity terms [PITH_FULL_IMAGE:figures/full_fig_p024_3.png] view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: Semantic relation constructors for the empty type and its eliminator [PITH_FULL_IMAGE:figures/full_fig_p024_4.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

47 extracted references · 2 linked inside Pith

  1. [1]

    A. Abel, J. \" O hman, and A. Vezzosi. Decidability of conversion for type theory in type theory. Proc. ACM Program. Lang. , 2 0 (POPL), December 2017

    2017

  2. [2]

    P. Aczel. The type theoretic interpretation of constructive set theory: Choice principles. In A.S. Troelstra and D. van Dalen , editors, The L. E. J. Brouwer Centenary Symposium , volume 110 of Studies in Logic and the Foundations of Mathematics , pages 1--40. Elsevier, 1982

    1982

  3. [3]

    Ahrens and P

    B. Ahrens and P. LF. Lumsdaine. Displayed categories. Logical Methods in Computer Science , Volume 15, Issue 1: 0 20:1--20:18, Mar 2019

    2019

  4. [4]

    Altenkirch

    T. Altenkirch. Extensional equality in intensional type theory. In 14th Annual Symposium on Logic in Computer Science , pages 412--420. IEEE Computer Society Press, Washington, 1999

    1999

  5. [5]

    Altenkirch, S

    T. Altenkirch, S. Boulier, A. Kaposi, C. Sattler, and F. Sestini. Constructing a universe for the setoid model. In S. Kiefer and C. Tasson, editors, Foundations of Software Science and Computation Structures (FoSSaCS 2021) , volume 12650 of Lecture Notes in Computer Science , pages 1--21. Springer, 2021

    2021

  6. [6]

    Altenkirch, S

    T. Altenkirch, S. Boulier, A. Kaposi, and N. Tabareau. Setoid type theory---a syntactic translation. In G. Hutton, editor, Mathematics of Program Construction , volume 11825 of Lecture Notes in Computer Science , pages 155--196. Springer International Publishing, 2019

    2019

  7. [7]

    Altenkirch and A

    T. Altenkirch and A. Kaposi. Type theory in type theory using quotient inductive types. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages , POPL 2016, pages 18--29, New York, NY, USA, 2016. ACM

    2016

  8. [8]

    Altenkirch, C

    T. Altenkirch, C. McBride, and W. Swierstra. Observational equality, now! In PLPV 2007: Proceedings of the 2007 Workshop on Programming Languages Meets Program Verification , pages 57--68, New York, NY, USA, 2007. ACM. ISBN 978-1-59593-677-6

    2007

Show all 47 references
  1. [9]

    Aydemir, A

    B. Aydemir, A. Chargu\' e raud, B. C. Pierce, R. Pollack, and S. Weirich. Engineering formal metatheory. In Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages , POPL '08, page 3–15, New York, NY, USA, 2008. Association for Comput...

    2008

  2. [10]

    Barras, T

    B. Barras, T. Coquand, and S. Huber. A generalization of the Takeuti–Gandy interpretation. Mathematical Structures in Computer Science , 25 0 (5): 0 1071--1099, 2015

    2015

  3. [11]

    Berry and M

    D. Berry and M. Fiore. Formal P -category theory and normalization by evaluation in Rocq . Mathematical Structures in Computer Science , 36: 0 1--30, 2026

    2026

  4. [12]

    E. Bishop. Foundations of Constructive Analysis . MacGraw-Hill, 1967. Reprinted from the original version by Ishi Press International in 2012

    1967

  5. [13]

    Capriotti and N

    P. Capriotti and N. Kraus. Univalent higher categories via complete semi- Segal types. Proc. ACM Program. Lang. , 2 0 (POPL): 0 44:1--44:29, December 2017

    2017

  6. [14]

    Cartmell

    J. Cartmell. Generalised algebraic theories and contextual categories. Annals of Pure and Applied Logic , 32 0 (0): 0 209--243, 1986

    1986

  7. [15]

    Cockx, D

    J. Cockx, D. Devriese, and F. Piessens. Pattern matching without K . In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming , ICFP 2014, pages 257--268, New York, NY, USA, 2014. ACM. ISBN 978-1-4503-2873-9. URL http://doi.acm.org/10.1145/2628...

    2014

  8. [16]

    T. Coquand. Pattern matching with dependent types. In B. Nordstr \" o m, K. Petersson, and G. D. Plotkin, editors, Proceedings of the 1992 Workshop on Types for Proofs and Programs, B stad, Sweden , pages 66--79, June 1992

    1992

  9. [17]

    T. Coquand. Canonicity and normalization for dependent type theory. Theoretical Computer Science , 777: 0 184--191, 2019. In memory of Maurice Nivat, a founding father of Theoretical Computer Science - Part I

    2019

  10. [18]

    M. de Boer . A Proof and Formalization of the Initiality Conjecture of Dependent Type Theory . Licentiate thesis, Department of Mathematics, Stockholm University, Stockholm, 2020. URL https://github.com/guillaumebrunerie/initiality

    2020

  11. [19]

    P. Dybjer. Internal type theory. In S. Berardi and M. Coppo, editors, Types for Proofs and Programs , volume 1158 of Lecture Notes in Computer Science , pages 120--134. Springer Berlin Heidelberg, 1996

    1996

  12. [20]

    P. Dybjer. A general formulation of simultaneous inductive-recursive definitions in type theory. Journal of Symbolic Logic , 65 0 (2): 0 525--549, 2000

    2000

  13. [21]

    M. Fiore. Semantic analysis of normalisation by evaluation for typed lambda calculus. Mathematical Structures in Computer Science , 32 0 (8): 0 1028--1065, September 2022

    2022

  14. [22]

    R. Gandy. On the axiom of extensionality -- Part I . Journal of Symbolic Logic , pages 36--48, 1956

    1956

  15. [23]

    Goguen, C

    H. Goguen, C. McBride, and J. McKinna. Eliminating dependent pattern matching. In K. Futatsugi, J.-P. Jouannaud, and J. Meseguer, editors, Algebra, Meaning, and Computation: Essays dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday , pages 521--540. Springer Be...

    2006

  16. [24]

    M. Hofmann. Extensional Concepts in Intensional Type Theory . PhD thesis, University of Edinburgh, 1995

    1995

  17. [25]

    M. Hofmann. Syntax and semantics of dependent types. In A. M. Pitts and P. Dybjer, editors, Semantics and Logics of Computation , Publications of the Newton Institute, pages 79--130. Cambridge University Press, 1997

    1997

  18. [26]

    J. M. E. Hyland. The forgotten Turing . In S. B. Cooper and A. Hodges, editors, The Once and Future Turing : Computing the World , chapter 2, pages 20--33. Cambridge University Press, 2016

    2016

  19. [27]

    Kapulkin and Y

    K. Kapulkin and Y. Li. Extensional concepts in intensional type theory, revisited. Theoretical Computer Science , 1029: 0 115051, 2025

    2025

  20. [28]

    Martin-L\"of

    P. Martin-L\"of . An intuitionistic theory of types: Predicative part. In H.E. Rose and J.C. Shepherdson, editors, Logic Colloquium '73 , volume 80 of Studies in Logic and the Foundations of Mathematics , pages 73--118. Elsevier, 1975

    1975

  21. [29]

    Martin-L\"of

    P. Martin-L\"of . Intuitionistic Type Theory . Bibliopolis, Napoli, 1984

    1984

  22. [30]

    C. McBride. Dependently Typed Functional Programs and their Proofs . PhD thesis, University of Edinburgh, 1999

    1999

  23. [31]

    Palmgren

    E. Palmgren. From type theory to setoids and back. Mathematical Structures in Computer Science , 32 0 (10): 0 1283–1312, 2022

    2022

  24. [32]

    A. M. Pitts. Agda code accompanying `` Setoids in Intensional Type Theory '', 2026 a . Browsable code: https://amp12.github.io/IntensionalSetoids

    2026

  25. [33]

    A. M. Pitts. Well scoped locally nameless representation of syntax. Technical report, ArXiv e-print arXiv:2605.08990 [cs.LO] available at https://arxiv.org/abs/2605.08990, 2026 b

    2026 arXiv

  26. [34]

    R. Pollack. Dependently typed records in type theory. Formal Aspects of Computing , 13 0 (3): 0 386--402, July 2002

    2002

  27. [35]

    L. Pujet. An inductive universe for setoids. Abstract for the 31st International Conference on Types for Proofs and Programs (TYPES 2025), University of Strathclyde, Glasgow, Scotland (https://msp.cis.strath.ac.uk/types2025/TYPES2025-book-of-abstracts.pdf), June 2025

    2025

  28. [36]

    L. Pujet. Revisiting Hofmann's setoid model. Invited talk at Logic Colloquium 2026, Special Session on Type Theory, Swansea, Wales (https://github.com/loic-p/setoid-universe), June 2026

    2026

  29. [37]

    Slattery and J

    A. Slattery and J. Sterling. Bidirectional elaborators \`a la carte. Technical report, ArXiv e-print arXiv:2607.09564 [cs.PL] available at https://arxiv.org/abs/2607.09564, 2026

    2026 arXiv

  30. [38]

    Sterling

    J. Sterling. First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory . PhD thesis, Carnegie Mellon University, 2021. CMU technical report CMU-CS-21-142

    2021

  31. [39]

    Sterling, C

    J. Sterling, C. Angiuli, and D. Gratzer. A cubical language for Bishop sets. Logical Methods in Computer Science , 18: 0 43:1--43:80, March 2022

    2022

  32. [40]

    Streicher

    T. Streicher. Semantics of Type Theory . Birkh\"auser, 1991

    1991

  33. [41]

    Streicher

    T. Streicher. Investigations into Intensional Type Theory . Habilitation thesis, Ludwig Maximilian University, Munich, 1993

    1993

  34. [42]

    G. Takeuti. On a generalized logic calculus. Japanese Journal of Mathematics , 23: 0 39–96, 1953

    1953

  35. [43]

    Agda, version 2.8.0, July 2025

    The Agda Development Team . Agda, version 2.8.0, July 2025. URL https://agda.readthedocs.io/en/v2.8.0

    2025

  36. [44]

    The Rocq prover, version 9.0, March 2025

    The Rocq Development Team . The Rocq prover, version 9.0, March 2025. URL https://rocq-prover.org

    2025

  37. [45]

    T. Uemura. Abstract and Concrete Type Theories . PhD thesis, University of Amsterdam, 2021

    2021

  38. [46]

    Homotopy Type Theory: Univalent Foundations for Mathematics

    The Univalent Foundations Program . Homotopy Type Theory: Univalent Foundations for Mathematics . http://homotopytypetheory.org/book, Institute for Advanced Study, 2013

    2013

  39. [47]

    Winterhalter, M

    T. Winterhalter, M. Sozeau, and N. Tabareau. Eliminating reflection from type theory. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2019) , page 91–103, New York, NY, USA, 2019. Association for Computing Machinery

    2019

Pith tools

Reviewed July 30, 2026 · model on record in the stance chip above.