Pith. sign in

REVIEW 3 major objections 6 minor 45 references

Fibred sets within a predicative and constructive effective topos

T0 review · 3 major / 6 minor · reviewed 2026-08-12 · deepseek-v4-flash

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

Pith's one-line read The paper establishes that the predicative effective topos pEff carries two fibrations whose fibres are locally cartesian closed list-arithmetic pretoposes, a small-subobjects classifier Ω, and formal Church's thesis, making it a fibred…

desk verdict A serious fibred predicative topos construction with a real but repairable gap in the base-change lemma; worth refereeing. read the letter →

arxiv 2411.19239 v2 pith:VZ3NYZZP submitted 2024-11-28 math.LO

Cipriano Junior Cioffo , Maria Emilia Maietti , Samuele Maschio This is my paper · ORCID
classification math.LO MSC 03G3003F50
keywords predicativetoposeffectivefibrationofsetsrealizabilityformalChurch'sthesiselementaryquotientcompletionMinimalistFoundationconstructivesettheory
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 paper sets out to show that the predicative effective topos $\mathbf{pEff}$, previously built inside the classical predicative theory of non-iterative fixpoints $\widehat{ID_1}$, carries a full fibred structure of sets. Its central result is that $\mathbf{pEff}$ is equipped with two fibrations, one for collections and one for sets, whose fibres are locally cartesian closed list-arithmetic pretoposes, together with a small-subobjects classifier and the formal Church's thesis. If this result is right, the full subcategory of discrete objects inside Hyland's Effective Topos already contains a fibred predicative topos, even when both are formalized in a constructive metatheory. The structure is aimed at modelling both levels of the Minimalist Foundation, so that $\mathbf{pEff}$ would serve as a computational realizability model for a constructive and predicative foundation extended with inductive and coinductive predicates.

What carries the argument

The load-bearing object is the subfibration $\mathbf{pEff}_{\mathrm{set}} \to \mathbf{pEff}$ of the codomain fibration, which sends each object to its slice category and is here presented via extensional dependent sets $(B,[S],\sigma)$. Here $B$ is a realized family of sets over a base $A$, $[S]$ is a small fibred equivalence relation on $B$, and $\sigma$ moves elements of $B(a)$ to $B(a')$ along realizers of the equivalence relation $R$ on $A$, respecting identity and composition; the functor $K$ sends such a triple to an arrow $(\Sigma(A,B), \exists_{d_R}(\mathrm{Prop}_r^{t_\sigma}([S]))) \to (A,[R])$ in $\mathbf{pEff}$. Smallness of $B$ and $[S]$ is what separates the set-fibration from the collection-fibration, and Proposition 8.3 identifies small subobjects with the small-proposition doctrine, so Theorem 8.4 can supply the classifier $\Omega$. Around this, the proofs use the presentation of $\mathbf{pEff}$ as the exact completion of $\mathbf{Cr}$ and descent theory for internal groupoids.

What would settle it

Find an arrow $[p]:(A',[R'])\to(A,[R])$ in $\mathbf{pEff}$ and an extensional dependent set $(B,[S],\sigma)$ over $(A,[R])$ such that the pullback $[p]^*K(B,[S],\sigma)$ is not isomorphic to $K$ of any extensional dependent set over $(A',[R'])$. Concretely, try to construct $R'$ as a realized proposition not representable by a small proposition in $\mathbf{Prop}_r^s(A'\times A')$ while $R$ is small, and check whether the chosen representative $[g]:R'\to R$ can exist in $\mathbf{Prop}_r^s(A\times A)$. If no such $[g]$ can be supplied in general, the proof of Lemma 7.1 fails and the fibration is not well-defined.

Watch

Extended reading notes

Core claim

The paper's central claim is that the indexed structure of realized sets and small propositions on the category $\mathbf{Cr}$ lifts to a subfibration of the codomain fibration on $\mathbf{pEff}$. For each object $(A,[R])$ it forms the category of extensional dependent collections: a realized family $B$ over $A$, a fibred equivalence relation $[S]$ on $B$, and a transport action $\sigma$ along realizers of $R$ satisfying identity and composition laws; a subset of these, where $B$ is a realized set family and $[S]$ is small, gives the extensional dependent sets. The functor $K$ embeds these categories into the slice $\mathbf{pEff}/(A,[R])$, and the paper proves that the set-fibres are locally cartesian closed list-arithmetic pretoposes whose structure is preserved by pullback along every arrow of $\mathbf{pEff}$. It then shows that small subobjects are classified by an object $\Omega$ and that formal Church's thesis holds, concluding that $\mathbf{pEff}$ is a fibred predicative variant of Hyland's Effective Topos and that the discrete objects of $\mathbf{Eff}$ already contain such a structure in a constructive metatheory.

Load-bearing premise

The whole fibred structure depends on Lemma 7.1: pulling back a small family over $(A,[R])$ along any arrow $(A',[R'])\to(A,[R])$ must again be a small family. The proof needs a representative $[g]:R'\to R$ that is itself a small realized proposition, while $R'$ and $R$ are only arbitrary realized propositions; if that small representative cannot always be found, the set-fibration is not known to exist and Theorem 8.5 does not follow.

Editorial extensions

If this is right

  • If Theorem 8.5 is correct, the discrete objects of Hyland's Effective Topos contain a fibred predicative topos that validates formal Church's thesis, formalized in a constructive metatheory.
  • For every base object $(A,[R])$, the fibre over it is a locally cartesian closed list-arithmetic pretopos, so the sets over any fixed base form a full categorical universe.
  • Pullback along any arrow of $\mathbf{pEff}$ preserves the locally cartesian closed list-arithmetic pretopos structure, so substitution in the dependent type theory is interpreted by structure-preserving functors.
  • The object $\Omega$ classifies small subobjects in $\mathbf{pEff}$, giving a predicative analogue of the subobject classifier of an ordinary topos.
  • The fibred structure is designed to interpret the extensional level of the Minimalist Foundation, with inductive and coinductive predicates, inside $\mathbf{pEff}$.

Reading between the lines

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

  • Editorial inference: The construction gives a concrete template for a general notion of fibred predicative topos and a predicative tripos-to-topos construction, the two notions the paper names as future goals.
  • Editorial inference: A full fibred comparison with the predicative realizability categories of algebraic set theory, which the paper leaves to future work, would show whether the set-fibration here coincides with the small-map fibration on the common subcategory.
  • Editorial inference: A proof-assistant formalization of Lemma 7.1 would test the base-change smallness step directly and would make the constructive metatheory explicit enough to extract programs from the interpretation.
  • Editorial inference: If the interpretation of the extensional level goes through, one would expect $\mathbf{pEff}$ to yield a computational model for the classical version of the Minimalist Foundation via the equiconsistency result cited in the paper.
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

3 major / 6 minor

Summary. This paper continues the authors' earlier work [MM21] on the predicative effective topos pEff, a predicative and constructive variant of Hyland's Effective Topos. The paper defines, for each object (A,[R]) of pEff, categories DeppEff(A,R) and DeppEff_set(A,R) of extensional dependent collections and sets, and constructs a functor K from these to the slice category pEff/(A,[R]). The main structural claim, Theorem 8.5, is that pEff carries two fibrations, pEff_set and the codomain fibration, whose fibres are locally cartesian closed list-arithmetic pretoposes, that there is a small-subobject classifier Omega, and that formal Church's thesis holds, so that pEff is 'a fibred predicative variant of Hyland's Effective Topos'. The paper also sketches, in Section 9, how this structure could support a direct interpretation of the extensional level emTT of the Minimalist Foundation, and compares the base category pEff with van den Berg--Moerdijk's predicative realizability categories in Section 10.

Significance. If Theorem 8.5 is correct, the paper delivers a substantial result: the full subcategory of discrete objects of Hyland's Effective Topos contains a fibred predicative topos that validates formal Church's thesis in a constructive metatheory. This is a natural next step after [MM21] and connects the fibrational approach to the Minimalist Foundation with realizability semantics. The paper is constructive and predicative throughout, building on Feferman's ID_1 and extensions of CZF. The authors are explicit about relying on prior published work for the basic definitions of pEff, which is a normal dependency. The main weakness is that the construction of the central fibration contains a proof gap: Lemma 7.1, which is required to ensure that pullback preserves small families, is not proved as written. The issue appears repairable, but until a correct proof is supplied, the well-definedness of pEff_set and hence Theorem 8.5 are not established.

major comments (3)
  1. [Lemma 7.1] The proof of Lemma 7.1 selects a representative [g]:R'→R in Propr_s(A×A), but R and R' are arbitrary objects of Propr(A×A), not necessarily small. An arrow [p]:(A',R')→(A,R) does not give a small map R'→R; it gives a realizer e:R'→Colr_{p×p}(R) witnessing the inequality R' ≤ Propr_{p×p}(R). Consequently the pullback of a small family along [p] is not shown to land in DeppEff_set(A,R'). Since Lemma 7.1 is the only result in the paper that guarantees that the base-change operation defining pEff_set preserves the fibre of extensional dependent sets, the well-definedness of the fibration and all parts of Theorem 8.5 that use it (items 2--6) are not established as written. Please supply a direct construction of the transported action from the realizer e, verifying condition 4 of Definition 6.2, or provide an alternative proof of smallness of the pullback.
  2. [Proposition 6.8] The proof of essential surjectivity of K is incomplete: after defining B_f and [S]_f, the authors state 'Finally, we can define σ_f ... We leave this to the reader.' This is a load-bearing omission because the verification that σ_f satisfies the three conditions of Definition 6.2 is needed to conclude that (B_f,[S]_f,σ_f) is an object of DeppEff(A,R). Without this, K is not known to be essentially surjective. Remark 6.9 itself points out that the categorical consequences depend on whether one has an equivalence or merely preservation/reflection of limits. Please include the full definition of σ_f and the verification of conditions 1--3.
  3. [Theorem 7.5] The proof of Theorem 7.5 contains two 'one can check' assertions that are load-bearing. For stable finite coproducts, the text says 'One can check that these injections are mono, and that coproducts are stable under pullbacks using pullbacks constructed through the finite limits of DeppEff(A,R) and DeppEff_set(A,R) described above'; the stability under pullback is not shown. For exactness, the proof says that 'Stability and effectiveness follow from the pullback property in Lemma 7.1', but Lemma 7.1 is exactly the result whose proof is defective (see Major Comment 1), and the stability of the constructed coequalizer under pullback is not demonstrated. Since items 2 and 4 of Theorem 8.5 assert that the fibres are list-arithmetic pretoposes, these details are part of the central claim. Please provide full proofs of coproduct stability and of exactness, explicitly using a corrected Lemma 7.1.
minor comments (6)
  1. [Section 6, page 13] In Proposition 6.8, the notation tσ, dR and the arrows in the commutative diagram are not defined in the text; please define all arrows appearing in the diagram or refer to a specific equation.
  2. [Section 7, 'loose'] In the first paragraph of Section 7, 'loose their functoriality' should be 'lose their functoriality'.
  3. [Lemma 8.2] The statement 'Given an element (B,[S],σ) ∈ DeppEff (A, [R])' should read 'DeppEff(A,R)', since the category is indexed by a representative R, not an equivalence class [R].
  4. [Section 8, equation (10)] The displayed condition defining pEff_props(A,[R]) is 'Propr_{p1}([P]) ∧ [R] ≤ Propr_{p2}([P])'; it may be clearer to state explicitly that [P] is an object of Propr(A) satisfying this invariance condition with respect to [R].
  5. [Section 10, diagram] The diagram involving 'Cr /d31 /d127 i' is corrupted in the arXiv rendering; please redraw it so that the embedding of Cr and pEff into the corresponding assembly categories is readable.
  6. [Section 10, final paragraph] The sentence 'Since Cr is a full subcategory of recursive objects and pEff is the ex/lex completion of Cr we have an embedding of pEff in Disc_E[T] that extends to fibers, trivially' is too quick; please spell out how the embedding extends to the fibrations, or mark this as future work.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the fibred structure is derived from explicit constructions on the prior published base pEff; the only weakness is a possible proof gap in Lemma 7.1, which is a correctness matter, not a circular reduction.

full rationale

After walking the derivation chain, I find no circular step. The paper's load-bearing new results (Lemma 7.1, Theorem 7.5, Theorem 8.5) are not obtained by fitting a parameter to the target conclusion or by defining the output in terms of itself. The base category pEff, the categories Cr, Setr, Propr, Propr_s, and the formal Church's thesis result are imported from the authors' earlier published work [MM21, IMMS18, MMR21, MMR22]; this is ordinary background dependency, not circularity, since those results are stated with their own assumptions and are not re-derived from the fibred structure claimed here. The only concerning passage is Lemma 7.1: its proof selects a representative [g]: R' to R in Propr_s(A×A) although R and R' are arbitrary realized propositions and Propr_s contains only small propositions, so the existence of such a small map is not immediate; if this is a real gap it is a correctness defect in the base-change construction, not a reduction of the theorem to its inputs. The typographical proof line '2. follows from Theorem 8.1' in Theorem 8.5 should presumably refer to Theorem 7.5 and does not indicate circularity. Accordingly, the circularity score is 0.

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

No numerical free parameters appear: the paper is a structural categorical analysis. The central claim depends on the background metatheories (ID_hat_1 or CZF extensions) and on the previously established construction of pEff as the elementary quotient completion of Propr, plus the universe of realized sets from [IMMS18, MMR21]. All new categorical structures, such as extensional dependent collections and the fibration pEff_set, are constructed explicitly rather than postulated.

assumptions (6)
  • domain assumption T is one of ID_hat_1, CZF+REA, or CZF+RDC+Union-REA
    The whole paper is formalized in one of these metatheories (Section 2); the existence and properties of pEff and the fibred structure depend on them.
  • domain assumption pEff is equivalent to the exact completion (Cr)ex/lex and is a locally cartesian closed list-arithmetic pretopos
    Invoked in Section 6 and Theorem 7.5; taken from [MM21, Theorem 5.5].
  • domain assumption There is a universe US of realized sets closed under codes for Sigma and Pi types
    Defined as a fixed point in ID_hat_1 or via Set(x) in CZF (Section 3.3), used in Lemmas 3.9 and 3.10; taken from [IMMS18, MMR21].
  • domain assumption The doctrine Propr is a first-order hyperdoctrine and pEff_prop is equivalent to SubpEff
    Used in Lemma 7.3 and Theorem 8.1; follows from [MM21, Theorem 4.19 and Theorem 5.7].
  • domain assumption The metatheory supports countable choice when needed for the equivalence in Remark 6.9
    The authors note they only get preservation and reflection of limits, colimits and exponentials without it; with CZF+RDC this assumption is available.
  • domain assumption The metatheory T has the numerical existence property for the comparison in Proposition 10.1
    Used to make the comparison functor i from Cr to Asm_E[T] full and faithful; known for CZF, CZF+REA, and CZF+RDC+Union-REA via [Rat05, Rat08].

how reviews work

0 comments
Cite this review

Pith. "Pith review of Fibred sets within a predicative and constructive effective topos." pith.science (2026). https://pith.science/paper/VZ3NYZZP

@misc{pith2026241119239,
  author       = {Pith},
  title        = {Pith review of: Fibred sets within a predicative and constructive effective topos},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/VZ3NYZZP}},
  note         = {Machine review of arXiv:2411.19239}
}
abstract

We describe the fibrational structure of sets within the predicative variant $\mathbf{pEff}$ of Hyland's Effective Topos $\mathbf{Eff}$ previously introduced in Feferman's predicative theory of non-iterative fixpoints $\widehat{ID_1}$. Our structural analysis can be carried out in constructive and predicative variants of $\mathbf{Eff}$ within extensions of Aczel's Constructive Zermelo-Fraenkel Set Theory. All this shows that the full subcategory of discrete objects of Hyland's Effective topos $\mathbf{Eff}$ contains already a fibred predicative topos validating the formal Church's thesis, even when both are formalized in a constructive metatheory.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

45 extracted references · 44 canonical work pages

  1. [1]

    Aczel and M

    P. Aczel and M. Rathjen . Notes on constructive set theory. Mittag-Leffler Technical Report No.40, 2001

    work page 2001

  2. [2]

    Natural models of homotopy type theory

    Steve Awodey. Natural models of homotopy type theory. Mathematical Structures in Computer Science , 28(2):241--286, 2018

    work page 2018

  3. [3]

    van den B erg and I

    B. van den B erg and I. Moerdijk . Aspects of predicative algebraic set theory I : Exact completion. Annals of Pure and Applied Logic, , 156(1):123--159, 2008

    work page 2008

  4. [4]

    van den Berg and I

    B. van den Berg and I. Moerdijk . Aspects of predicative algebraic set theory II : Realizability. Theoretical Computer Science , 412:1916--1940, 2011

    work page 1916

  5. [5]

    A. Carboni. Some free constructions in realizability and proof theory. Journal of Pure and Applied Algebra , 103:117--148, 1995

    work page 1995

  6. [6]

    C. J. Cioffo. Biased elementary doctrines and quotient completions. arXiv preprint arXiv:2304.03066 , 2023

    arXiv 2023

  7. [7]

    Carboni, S

    A. Carboni, S. Lack, and R. F. C. Walters. Introduction to extensive and distributive categories. Journal of Pure and Applied Algebra , 84(2):145--158, 1993

    work page 1993

  8. [8]

    Carboni and R

    A. Carboni and R. Celia Magno. The free exact category on a left exact one. J. Austral. Math. Soc. Ser. A , 33(3):295--301, 1982

    work page 1982

Show all 45 references
  1. [9]

    Contente and M.E

    M. Contente and M.E. Maietti. The compatibility of the minimalist foundation with homotopy type theory. Theoretical Computer Science , 991:114421, 2024

    2024

  2. [10]

    Carboni and E

    A. Carboni and E. M. Vitale. Regular and exact completions. Journal of Pure and Applied Algebra , 125(1-3):79--116, 1998

    1998

  3. [11]

    P. Dybjer. Internal type theory. In Types for proofs and programs ( T orino, 1995) , volume 1158 of Lecture Notes in Comput. Sci. , pages 120--134. Springer, Berlin, 1996

    1995

  4. [12]

    Feferman

    S. Feferman. Iterated inductive fixed-point theories: application to hancock's conjecture. In Studies in Logic and the Foundations of Mathematics , volume 109, pages 171--196. Elsevier, 1982

    1982

  5. [13]

    J. M. E. H yland, P. T. J ohnstone, and A. M. P itts. Tripos theory. Bulletin of the Australian Mathematical Society , 88:205--232, 1980

    1980

  6. [14]

    P. J. Hofstra. Relative completions. Journal of Pure and Applied Algebra , 192(1-3):129--148, 2004

    2004

  7. [15]

    J. M. E. Hyland, E. P. Robinson, and G. Rosolini. The discrete objects in the effective topos. Proc. London Math. Soc. (3) , 60(1):1--36, 1990

    1990

  8. [16]

    J. M. E. Hyland . The effective topos. In The L.E.J. Brouwer Centenary Symposium (Noordwijkerhout, 1981) , volume 110 of Stud. Logic Foundations Math. , pages 165--216. North-Holland, Amsterdam-New York,, 1982

    1981

  9. [17]

    Ishihara, M

    H. Ishihara, M. E. Maietti, S. Maschio, and T. Streicher. Consistency of the intensional level of the minimalist foundation with church’s thesis and axiom of choice. Archive for Mathematical Logic , 57(7-8):873--888, 2018

    2018

  10. [18]

    B. Jacobs. Categorical logic and type theory , volume 141 of Studies in Logic and the Foundations of Mathematics . North-Holland Publishing Co., Amsterdam, 1999

    1999

  11. [19]

    Janelidze and W

    G. Janelidze and W. Tholen. Facets of descent. I . Applied Categorical Structures , 2(3):245--281, 1994

    1994

  12. [20]

    M. E. Maietti. Modular correspondence between dependent type theories and categories including pretopoi and topoi. Math. Structures Comput. Sci. , 15(6):1089--1149, 2005

    2005

  13. [21]

    M. E. Maietti . A minimalist two-level foundation for constructive mathematics. Annals of Pure and Applied Logic, , 160(3):319--354, 2009

    2009

  14. [22]

    MacLane and I

    S. MacLane and I. Moerdijk. Sheaves in geometry and logic: A first introduction to topos theory . Springer Science & Business Media, 2012

    2012

  15. [23]

    M. E. Maietti and S. Maschio. A predicative variant of a realizability tripos for the M inimalist F oundation. IfColog Journal of Logics and their Applications , 3(4):595--668, 2016

    2016

  16. [24]

    M. E. Maietti and S. Maschio. A predicative variant of H yland's effective topos. The Journal of Symbolic Logic , 86(2):433–447, 2021

    2021

  17. [25]

    M. E. Maietti, S. Maschio, and M. Rathjen. A realizability semantics for inductive formal topologies, church's thesis and axiom of choice. Logical Methods in Computer Science , 17, 2021

    2021

  18. [26]

    M. E. Maietti, S. Maschio, and M. Rathjen. Inductive and coinductive topological generation with church's thesis and the axiom of choice. Logical Methods in Computer Science , 18, 2022

    2022

  19. [27]

    Moerdijk and E

    I. Moerdijk and E. Palmgren. Type theories, toposes and constructive set theory: predicative aspects of AST . Annals of Pure and Applied Logic, , 114(1-3):155--201, 2002

    2002

  20. [28]

    M. E. Maietti and G. Rosolini. Elementary quotient completion. Theory and Applications of Categories , 27(17):445--463, 2013

    2013

  21. [29]

    M. E. Maietti and G. Rosolini . Quotient completion for the foundation of constructive mathematics. Logica Universalis , 7(3):371--402, 2013

    2013

  22. [30]

    M. E. Maietti and G. Rosolini. Unifying exact completions. Appl. Categ. Structures , 23(1):43--52, 2015

    2015

  23. [31]

    M. E. Maietti and G. Rosolini . Relating quotient completions via categorical logic. In Dieter Probst and Peter Schuster, editors, Concepts of Proof in Mathematics, Philosophy, and Computer Science , pages 229--250, 2016

    2016

  24. [32]

    M. E. Maietti and G. Sambin . Toward a minimalist foundation for constructive mathematics . In L. Crosilla and P. Schuster , editor, From Sets and Types to Topology and Analysis: Practicable Foundations for Constructive Mathematics , number 48 in Oxford Logic Guides , pages 91...

    2005

  25. [33]

    M. E. Maietti and P. Sabelli. A topological counterpart of well-founded trees in dependent type theory. In Marie Kerjean and Paul Blain Levy, editors, Proceedings of the 39th Conference on the Mathematical Foundations of Programming Semantics, MFPS XXXIX, Indiana University, B...

    2023

  26. [34]

    Maietti and P

    M.E. Maietti and P. Sabelli. Equiconsistency of the minimalist foundation with its classical version. Annals of Pure and Applied Logic, , 2024. to appear

    2024

  27. [35]

    M. E. Maietti and D. Trotta. Generalized existential completions and their regular and exact completions, 2021

    2021

  28. [36]

    M. E. Maietti and D. Trotta. A characterization of generalized existential completions. Ann. Pure Appl. Log. , 174:103234, 2022

    2022

  29. [37]

    M. Rathjen. The disjunction and related properties for constructive Z ermelo- F raenkel set theory. The Journal of Symbolic Logic , 70(4):1232--1254, 2005

    2005

  30. [38]

    M. Rathjen. Metamathematical properties of intuitionistic set theories with choice principles. In New computational paradigms , pages 287--312. Springer, New York, 2008

    2008

  31. [39]

    Rosolini

    G. Rosolini. About modest sets. volume 1, pages 341--353. 1990. Third Italian Conference on Theoretical Computer Science (Mantova, 1990)

    1990

  32. [40]

    Robinson and G

    E. Robinson and G. Rosolini. Colimit completions and the effective topos. The Journal of Symbolic Logic , 55(2):678--699, 1990

    1990

  33. [41]

    Sterling and C

    J. Sterling and C. Angiuli. Normalization for cubical type theory. In 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) , pages 1--15, 2021

    2021

  34. [42]

    P. Sabelli. Around the Minimalist FOundation: (Co)Induction and Equiconsistency . PhD thesis, Università degli Studi di Padova, 2024

    2024

  35. [43]

    van Oosten

    J. van Oosten. Axiomatizing higher order K leene realizability. Annals of Pure and Applied Logic, , 70(87-111), 1994

    1994

  36. [44]

    van Oosten

    J. van Oosten. Realizability: an introduction to its categorical side , volume 152 of Studies in Logic and Foundations of Mathematics . Elsevier, 2008

    2008

  37. [45]

    van Oosten

    J. van Oosten. A notion of homotopy for the effective topos. Math. Structures Comput. Sci. , 25(5):1132--1146, 2015

    2015

Pith tools

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