Pith. sign in

REVIEW 4 major objections 7 minor 9 references

Master Thesis Impredicative Encodings of Inductive and Coinductive Types

T0 review · 4 major / 7 minor · reviewed 2026-08-15 · deepseek-v4-flash

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

Pith's one-line read W-types and M-types defined impredicatively with induction and bisimulation principles

desk verdict 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. read the letter →

arxiv 2505.13495 v1 pith:VILRX56W submitted 2025-05-15 cs.LO

Steven Bronsveld , Herman Geuvers , Niels van der Weide This is my paper · ORCID
classification cs.LO
keywords impredicativeencodingsW-typesM-typesinductionprinciplecoinductionbisimulationetarulesquotienttypes
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

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

  • 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.

Reading between the lines

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

  • 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.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

4 major / 7 minor

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.

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 (4)
  1. [Sec. 6.1 / Axiom 6.1.4] 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.
  2. [Definition 9.5.1] 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.
  3. [Theorems 6.5.4 and 9.5.4] 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.
  4. [Lemma 9.4.6] 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.
minor comments (7)
  1. [Lemma 6.4.11] 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.
  2. [Lemma 5.3.6] 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.
  3. [Definition 6.4.7] The line 'hd := hd∗ := recq E hd∗ EqHd' overloads hd∗; please use distinct names for the original head function and its quotient lift.
  4. [Example 8.2.3] The name '1W∗' is introduced twice in the example; the third definition is presumably meant to be '2W∗'.
  5. [Theorem 8.5.5] Steps 5 and 6 of the proof refer to 'idList' in the W-type context, where the intended term is idWAB.
  6. [Section 5.4] The section title contains a typo: 'priciple' should be 'principle'.
  7. [Definition 3.2.2] Two inference rules are labelled 'Σ-form1'; the second should presumably be 'Σ-form2'.

Circularity Check

5 steps flagged · score 6.0 of 10

The eta-rules for List, quot, W, Stream, and M are written into the subtype/quotient definitions, so the (co)induction principles follow by projection rather than from an independent derivation; the coinductive half additionally depends on the paper's own unproved ExistsId axiom.

  1. self definitional [Section 4.3, Definition 4.3.2; Lemma 4.3.8; Theorem 4.3.9]
    "List := X(l : List∗). LimList l … LimList (l : List∗) := Y X,Y :U … (MorphList X x g Y y h f) =⇒ f(rec∗l X x g l) = rec∗l Y y h l … By looking at (p := pr2 l), which has type LimList(pr1 l), we obtain the following equation: f (rec∗l List nil cons (pr1 l)) = rec∗l X x g(pr1 l)."

    The uniqueness/eta-rule concluded in Theorem 4.3.9 is exactly the predicate LimList used to carve out the subtype List. Every element l of List carries a proof component p : LimList(pr1 l), so the theorem is obtained by applying that proof component, not by deriving initiality from the System F encoding. The genuine constructive content is that nil and cons inhabit the subtype; the eta-rule itself is true by construction of the subtype.

  2. self definitional [Section 5.3, Definition 5.3.1; Lemma 5.3.6; Theorem 5.3.7]
    "quot (D :U) (R :D→D→U ) := X(q : quot∗ D R).LimQuot q … LimQuot (q : quot∗ D R) := … (H : (EqCls g R))∧(H′ : (EqCls g′ R))∧f◦g =g′ =⇒ f (rec∗q E g H q) = rec∗q E g′ H′ q … By Lemma 5.3.6 we have that cls = idD/R."

    The quotient eta-rule of Theorem 5.3.7 is the LimQuot condition written into the sigma-type defining quot. Lemma 5.3.6 (cls = id) is proved from the same proof component, and the general eta-rule then follows by applying p : LimQuot(pr1 q). Thus the uniqueness principle is part of the definition, not an independent consequence of the impredicative quotient encoding.

3 more flagged steps
  1. self definitional [Section 8.4, Definition 8.4.2; Lemma 8.4.7; Theorem 8.4.8]
    "W(a : A).B(a) := X(w : W∗(a : A).B(a)).LimW w … LimW w := Y(X,Y :U) … (MorphW X g Y g′ f) =⇒ f(rec∗W X g w) = rec∗W Y g′ w … By looking at (p := pr2 w), which has type LimW(pr1 w), we obtain the following equation: …"

    The W-type's eta-rule is precisely the LimW predicate defining the embedding W ↪ W∗. Theorem 8.4.8 derives f = recW X g by applying the proof component pr2 w, and Lemma 8.4.7 is proved in the same way. The claimed W-induction principle therefore rests on a uniqueness property installed in the definition by the predicate LimW.

  2. self definitional [Section 7.2; Definitions 6.4.2 and 6.4.7; Theorem 6.4.14]
    "For Stream we wanted to guarantee the uniqueness of (corecs X h t). We ensured this by requiring that the following equality holds for S-morphisms f: (corecs Y h′ t′)◦f = corecs X h t … To obtain the final object of S-CoAlg, we take the coequalizer of the two morphisms corecs Y h′ t′◦f and corecs X h t, which is ⟨Stream, cls⟩."

    The final-coalgebra property, and hence the eta-rule proved as Theorem 6.4.14, is installed by quotienting Stream∗ by CoLimStr, a relation defined as the existence of an S-coalgebra morphism connecting the two corecursive streams. The theorem is the universal property of that quotient by construction. The bisimulation theorem 6.5.4 is then derived from this built-in eta-rule, so the coinduction principle is a consequence of the defining quotient rather than of the System F stream encoding alone.

  3. self definitional [Section 9.4, Definitions 9.4.2 and 9.4.4; Theorem 9.4.14]
    "M(a : A).B(a) := quot (M∗(a : A).B(a)) CoLimM … CoLimM m n := ∃(X,Y :U).∃g :X→P(a:A).B(a)→X g′ :Y→P(a:A).B(a)→Y.∃(f :X→Y).∃(x :X). (MorphM X g Y g′ f)∧ m = corec∗M X g x∧ n = corec∗M Y g′ (f x) … MorphM X g MAB elimM f =⇒ f = corecM X g"

    As with Stream, the M-type eta-rule in Theorem 9.4.14 is the coequalizer universal property encoded in the quotient by CoLimM. The coinduction principle Theorem 9.5.4 is then proved from that built-in eta-rule. Thus the generic coinductive claim, like the generic inductive W-claim, reduces the uniqueness principle to the defining relation of the type.

full rationale

Score 6: partial circularity, because several central 'predictions' are built into the definitions. List, quot, and W are defined as sigma-subtypes whose second components are exactly the uniqueness/eta equations later proved as theorems; Stream and M are defined as quotients by relations whose universal property is exactly the final-coalgebra eta-rule. The paper itself summarizes the method in Section 7.3: 'we encode the (co)limit/uniqueness/(co)induction principles within the definition of the type.' So Theorems 4.3.9, 5.3.7, 8.4.8, 6.4.14, and 9.4.14 follow by projecting proof components or by the defining equality of the quotient. There is still independent content: the constructors are checked to inhabit the subtypes/quotients, and the beta-rules are proved from the underlying System F definitions. No fitted-data circularity and no load-bearing self-citation chain is present; AFS18 and Speight are prior work by non-overlapping authors. A separate, explicitly acknowledged limitation is Axiom 6.1.4 (ExistsId: rec∃(∃X.P) pack = id∃X.P), used in Lemmas 6.4.12 and 9.4.12; Appendix D concedes that 'without ExistsId, we are unable to prove that σ = corecs X h t x'. This makes the stream and M-type results conditional on an unproved axiom, which is a load-bearing assumption rather than a circularity, but it reinforces that the coinductive half is not fully first-principles.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

The paper introduces no fitted parameters and no new postulated entities beyond the data types it constructs. The main additional assumption beyond standard MLTT plus FunExt and UIP is the ExistsId axiom, which is specific to this work and is needed for the coinductive encodings.

assumptions (4)
  • domain assumption Function extensionality (FunExt)
    Postulated in Section 3.2 (Axiom 3.2.5), used pervasively to prove equality of functions, for example in Lemma 4.3.7.
  • domain assumption Uniqueness of identity proofs (UIP)
    Axiom 3.2.6, used in Lemma 5.3.4 to identify proof fields in sigma types and in proving eta rules.
  • ad hoc to paper ExistsId: rec∃ (∃X.P) pack = id
    Axiom 6.1.4, introduced to make the impredicative existential encoding satisfy the eta rule; used in Lemma 6.4.12 and Lemma 9.4.12. The paper notes it might be provable for an improved existential type.
  • domain assumption Intensional Martin-Löf type theory with Σ, Π, identity types plus one impredicative bottom universe
    Chapter 3 defines the system; the impredicativity of the bottom universe is essential to the System F style encodings.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Master Thesis Impredicative Encodings of Inductive and Coinductive Types." pith.science (2026). https://pith.science/paper/VILRX56W

@misc{pith2026250513495,
  author       = {Pith},
  title        = {Pith review of: Master Thesis Impredicative Encodings of Inductive and Coinductive Types},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/VILRX56W}},
  note         = {Machine review of arXiv:2505.13495}
}
read the original abstract

In the impredicative type theory of System F ({\lambda}2), it is possible to create inductive data types, such as natural numbers and lists. It is also possible to create coinductive data types such as streams. They work well in the sense that their (co)recursion principles obey the expected computation rules (the \b{eta}-rules). Unfortunately, they do not yield a (co)induction principle, because the necessary uniqueness principles are missing (the {\eta}-rules). Awodey, Frey, and Speight (2018) used an extension of {\lambda}C with sigma-types, equality-types, and functional extensionality to provide System F style inductive types with an induction principle by encoding them as a well-chosen subtype, making them initial algebras. In this thesis, we extend their results. We create a list and quotient type that have the desired induction principles. We show that we can use the technique for general inductive types by defining W-types with an induction principle. We also take the dual notion of their technique and create a coinductive stream type with the desired coinduction principle (also called bisimulation). We finish by showing that this dual approach can be extended to M-types, the generic notion of coinductive types, and the dual of W-types.

Figures

Figures reproduced from arXiv: 2505.13495 by the authors.

Figure 4.1
Figure 4.1. Commutative diagram of a L-morphism. If we write out this diagram in formulas we derive the following commutativity requirement: f ◦ [x, g] = [y, h] ◦ [inl,⟨e, x⟩ 7→ inr⟨e, f(x)⟩] ⇐⇒ [f ◦ x, f ◦ g] = [y, h ◦ (⟨e, x⟩ 7→ ⟨e, f(x)⟩)] ⇐⇒ f ◦ x = y ∧ f ◦ g = h ◦ (⟨e, x⟩ 7→ ⟨e, f(x)⟩) (4.2) Recall that the initial object ⟨I, γ⟩ of the category of L-algebras L-Alg has exactly one morphism [PITH_FULL_IMAGE:figures/full_fig… view at source ↗
Figure 4.3
Figure 4.3. Commutative diagram of the initial L-algebra. These L-morphisms uX should of course satisfy the commutativity requirement of Equation (4.2). Writing down the uniqueness requirement is a bit more tricky. We use requirement 2 from Proposition 2.2.7. This states that, given a morphism f : ⟨X, α⟩ → ⟨Y, β⟩  , and morphisms (uX : I → X) and (uY : I → Y ) (which all satisfy Equation (4.2)), we have that f ◦ uX = uY . This… view at source ↗
Figure 4.4
Figure 4.4. Diagram of the uniqueness requirement of an initial [PITH_FULL_IMAGE:figures/full_fig_p020_4_4.png] view at source ↗
Figures from the paper (11 more)
Figure 5.1
Figure 5.1. Figure 5.1: Commutative diagram of the β-rule for quotient types. Lemma 5.1.6. The β-rule for quotient types is satisfied. For (D : U),(R : D → D → U),(f : D → C) and (H : (EqCls f R)) we have that f ◦ cls∗ = f. In other words: (rec∗ q C f H) ◦ cls∗ = f (computation) Proof. Let …
Figure 5.2
Figure 5.2. Figure 5.2: Uniqueness rule for quotients. Just as seen before, we can give an alternative definition. Suppose we have morphisms (g : D → X) and (g ′ : D → Y ) that both satisfy the additional requirement that (EqCls g R) and (EqCls g ′ R). By the β-rule, we know that g ◦ cls∗ =…
Figure 5.3
Figure 5.3. Figure 5.3: Commutative diagram of the η-rule for quotient types. 5.3 Impredicative encoding of quotients We are now ready to define an impredicative encoding that satisfies the η-rule. Note that we follow the same approach as we did for encoding List in the previous chapter. We…
Figure 6.1
Figure 6.1. Figure 6.1: Commutative diagram of S-CoAlg morphisms. In formulas this comes down to the following: h ′ ◦ f = h ∧ t ′ ◦ f = f ◦ t The final object ⟨F,⟨hd,tl⟩⟩ of the category of S-coalgebras S-CoAlg has exectly one morphism [PITH_FULL_IMAGE:figures/full_fig_p038_6_1.png]
Figure 6.2
Figure 6.2. Figure 6.2: Diagram of the final S-coalgebra. 6.4 Impredicative encoding of streams As we saw before with lists, we shall now translate the categorical notion of final S-coalgebra back to type theory. We define a predicate that states that (f : X → Y ) forms an S-coalgebra morph…
Figure 6.1
Figure 6.1. Figure 6.1:  MorphStream X h t Y h′ t ′ f : X → Y := h ′ ◦ f = h ∧ t ′ ◦ f = f ◦ t  Let us take a moment to think about what we want to achieve. We want to define an encoding of Stream∗ that satisfies the η-rule. This η-rule is taken from the final coalgebra of S as shown in …
Figure 7.4
Figure 7.4. Figure 7.4: Diagrams of List and Stream 7.3 Alternative predicates In this thesis, we used the limit and colimit to encode the (co)inductive data types similar to [AFS18]. It is also possible to take different predicates/relations. One can for example directly encode the inducti…
Figure 8.1
Figure 8.1. Figure 8.1: Commutative diagram of W-morphisms. In formulas, a function (f : X → Y ) is a W-morphism if the following holds: f ◦ g = g ′ ◦ ⟨π1, f ◦ π2⟩ ⇐⇒ ∀(a : A),(t : B(a) → X). f ◦ g ◦ ⟨a, t⟩ = g ′ ◦ ⟨a, f ◦ t⟩ (8.2) As we saw before, we write out the uniqueness requirement o…
Figure 8.3
Figure 8.3. Figure 8.3: Uniqueness requirement of the initial W-algebra. 8.4 Impredicative encoding of W-types In this section we give an impredicative encoding of the W-type that we defined in Section 8.2. To start, we give a predicate MorphW that states that a function f is a W-morphism. …
Figure 9.1
Figure 9.1. Figure 9.1: Commutative diagram of M-morphisms. In formulas, a function (f : X → Y ) is an M-morphism, if the following holds: g ′ ◦ f = ⟨π1, f ◦ π2⟩ ◦ g ⇐⇒ ∀(x : X). g′ (f x) = ⟨π1(g x), f ◦ (π2 (g x))⟩ ⇐⇒ ∀(x : X). π1(g ′ (f x)) = π1(g x) ∧ π2(g ′ (f x)) = f ◦ (π2 (g x)) (9.2)…
Figure 9.3
Figure 9.3. Figure 9.3: Uniqueness requirement of the final M-coalgebra. 60 [PITH_FULL_IMAGE:figures/full_fig_p062_9_3.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

9 extracted references · 5 canonical work pages

  1. [10]

    The Church-Scott representation of inductive and coinductive data

    1007/3- 540- 06859- 7\_148 . url: https://doi.org/10.1007/3- 540- 06859- 7%5C_148. [Geu14a] Herman Geuvers. “The Church-Scott representation of inductive and coinductive data”. In:

    doi:10.1007/3-

  2. [19]

    Springer, 1974, pp

    Lecture Notes in Computer Science. Springer, 1974, pp. 408–423. doi:

    work page 1974

  3. [52]

    Cambridge University Press, 2012, pp

    Cambridge tracts in theoretical computer science. Cambridge University Press, 2012, pp. 38–99. [NG14] Rob Nederpelt and Herman Geuvers. Type Theory and Formal Proof: An Introduc- tion. Cambridge University Press,

    work page 2012

  4. [63]

    Towards a theory of type structure

    Studies in Logic and the Foundations of Mathematics. Elsevier, 1971, pp. 63–92. doi: https:// doi.org/10.1016/S0049-237X(08)70843-7 . url: https://www.sciencedirect. com/science/article/pii/S0049237X08708437. [Rey74] John C. Reynolds. “Towards a theory of type structure”. In: Programming Sympo- sium, Proceedings Colloque sur la Programmation, Paris, Franc...

    work page doi:10.1016/s0049-237x(08)70843-7 1971

  5. [442]

    Inductive Definitions in the system Coq - Rules and Properties

    Lecture Notes in Computer Science. Springer, 1989, pp. 209–228. doi: 10.1007/BFB0040259 . url: https://doi.org/ 10.1007/BFb0040259. [Pau93] Christine Paulin-Mohring. “Inductive Definitions in the system Coq - Rules and Properties”. In: Typed Lambda Calculi and Applications, International Conference on Typed Lambda Calculi and Applications, TLCA ’93, Utrec...

    work page doi:10.1007/bfb0040259 1989

  6. [664]

    Impredicative Encodings of (Higher) Inductive Types

    Lecture Notes in Computer Science. Springer, 1993, pp. 328–345. doi: 10.1007/BFB0037116 . url: https://doi.org/10.1007/ BFb0037116. [AFS18] Steve Awodey, Jonas Frey, and Sam Speight. “Impredicative Encodings of (Higher) Inductive Types”. In: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, ...

    arXiv 1993

  7. [1993]

    Induction is not derivable in second order dependent type theory

    [Geu01] Herman Geuvers. “Induction is not derivable in second order dependent type theory”. In: Lecture Notes in Computer Science (2001), pp. 166–181. doi: 10.1007/3-540- 45413-6_16. [Chu40] Alonzo Church. “A Formulation of the Simple Theory of Types”. In: J. Symb. Log. 5.2 (1940), pp. 56–68. doi: 10.2307/2266170 . url: https://doi.org/10.2307/ 2266170. [...

    doi:10.1007/3-540- 2001

  8. [2020]

    url: https://theses.liacs.nl/pdf/2019-2020-OttenDD.pdf. 77 Appendix F List of definitions BiSimM, 65 BiSim, 41 CoIndM, 66 CoIndStream, 42 CoLimM, 61 CoLimStr, 37 corecM, 61 corec∗ M, 59 corecs, 38 corec∗ s, 34 ElimEq1, 61 ElimEq2, 62 elimM, 63 elimM∗, 59 elimX, 66 EqCls2, 29 EqCls, 25 EqHd, 37 EqTl, 38 ExistsId, 33 HypW , 55 IdLift, 29 IndList, 22 IndW , ...

    work page 2019

Show all 9 references
  1. [2022]

    M-types and Bisimulation

    arXiv: 2212 . 11082 [math.LO]. url: https://arxiv.org/abs/2212.11082. [Ott20] Dani¨ el Otten. “M-types and Bisimulation”. Bachelor’s Thesis. Leiden University,

    arXiv

Pith tools

Reviewed August 15, 2026 · model on record in the stance chip above.