Pith. sign in

REVIEW 4 major objections 5 minor 31 references

A Model of Type Theory in Groupoid Assemblies

T0 review · 4 major / 5 minor · reviewed 2026-08-06 · deepseek-v4-flash

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

Pith's one-line read This paper establishes that Grpd(Asm(A)) is a π-tribe and a model of type theory, with univalent universes and a homotopy category recovering RT[A].

desk verdict A credible and genuinely new groupoidal realizability construction, but the central quotient step in §4.2 is unproven and the visible preliminaries contain real typos; deserves peer review but needs heavy revision. read the letter →

arxiv 2507.16062 v1 pith:QRXRSCRT submitted 2025-07-21 math.CT

Anthony Agwu This is my paper · ORCID
classification math.CT MSC 03B1503G3018B25
keywords groupoidassembliesrealizabilitypartialcombinatoryalgebradependenttypetheoryW-typeswithreductionsnormalisofibrationsunivalentuniversetopos
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 claims that the category of groupoid assemblies over any partial combinatory algebra A—internal groupoids in the realizability category Asm(A)—carries the structure of a π-tribe, a fibration-theoretic model of dependent type theory. The paper constructs an algebraic weak factorization system whose right maps are normal isofibrations, shows dependent products exist along these fibrations and satisfy the Frobenius property, and builds W-types with reductions that yield a model structure and localization modalities. It also exhibits a univalent object classifier for assemblies and a univalent, impredicative classifier for modest assemblies. The final section identifies the homotopy category of the 0-types of partitioned groupoid assemblies with RT[A], the realizability topos of A.

What carries the argument

The load-bearing object is the category Grpd(Asm(A)) of internal groupoids in assemblies on a partial combinatory algebra A, equipped with the interval groupoid I and the class of normal isofibrations. These are functors with a specified section for squares against ∂0 : 1 → I, satisfying a normality condition; they play the role of fibrations and support dependent products via an iso-comma construction. A second named mechanism is W-types with reductions, the initial algebras for polynomial functors with an extra reduction map, constructed by quotienting a tree assembly by a fibred partial equivalence relation; despite Asm(A) not being exact, the quotient is taken in underlying sets. These W-types drive a uniform small-object argument, and the π-tribe condition packages the resulting structure as a model of type theory.

What would settle it

Take the quotient construction of Lemma 4.2.7 in a concrete partial combinatory algebra such as the natural numbers with a pairing of partial recursive functions, and compute the fibred partial equivalence relation on the well-founded trees: if two trees are related but their composites or inverses are not related, the groupoid operations fail to descend and the small-object argument collapses. More directly, checking whether every congruence arising in the quotient is a kernel pair in Asm(A) would settle the point, since Asm(A) is not exact and exactness of Set is doing the work.

Watch

Extended reading notes

Core claim

The central claim is that the two-dimensional realizability structure Grpd(Asm(A)) is rich enough to interpret Martin-Löf type theory with univalence, and that its truncated part recovers ordinary realizability. The proof proceeds by making the right class of an algebraic weak factorization system be the normal isofibrations—internal functors with a uniform lifting property against the interval groupoid and a normality condition—and showing that this class is exponentiable, Frobenius, and closed under dependent product. W-types with reductions, built from a fibred partial equivalence relation on a decorated tree assembly, give the paper a small-object argument that produces the model structure. The universe of modest assemblies classifies precisely the maps whose fibers are modest assemblies and is shown to be both univalent and impredicative. On the 0-types of partitioned groupoid assemblies, inverting categorical equivalences yields a category equivalent to RT[A].

Load-bearing premise

The argument depends on the quotient used to build W-types-with-reductions actually respecting composition, identities, and inverses, a step where the paper invokes exactness of ordinary sets because the category of assemblies is not itself exact.

Editorial extensions

If this is right

  • Dependent type theory with Π, Σ, identity types, W-types and univalence is interpretable in Grpd(Asm(A)) for every partial combinatory algebra A.
  • The modest-assemblies classifier is at once univalent and impredicative, so the model has a universe closed under dependent products in the sense relevant to impredicative encodings.
  • The W-types-with-reductions produce an algebraic model structure, so homotopy-theoretic constructions such as localizations, truncations, the circle, and suspensions exist inside groupoid assemblies.
  • The homotopy category of 0-types of partitioned groupoid assemblies is RT[A], so the classical realizability topos is the 0-truncation of this groupoidal model.
  • Because the model is built from a partial combinatory algebra, its type-theoretic computations are realized by combinators, giving an effective and computational interpretation.

Reading between the lines

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

  • Inference: if the main theorem holds, the quotient method for W-types-with-reductions is a candidate template for constructing W-types in other non-exact categories that still have enough exactness at the level of underlying sets.
  • Inference: the 0-type identification suggests RT[A] embeds into the homotopy category of groupoid assemblies; one could test whether this embedding preserves dependent products, which would make realizability toposes retracts of the groupoidal model.
  • Inference: the paper's own suggested future work points toward an elementary 2-topos notion, and the normal isofibration structure is a natural candidate for the fibrational part of such a definition.
  • Inference: a testable extension is to ask whether the univalent impredicative classifier for modest assemblies remains a classifier after passing to the homotopy category, which would connect this model to known non-trivial models of HoTT with impredicative universes.
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

4 major / 5 minor

Summary. The manuscript claims that Grpd(Asm(A)), the category of groupoids internal to assemblies over a partial combinatory algebra A, carries the structure of a π-tribe and hence models dependent type theory; that it has W-types with reductions, a univalent object classifier for assemblies, and an impredicative univalent object classifier for modest assemblies; and that the resulting model structure has a homotopy category whose 0-types in the partitioned variant recover the realizability topos RT[A]. The visible portion develops the realizability-tripos background, assemblies, W-types with and without reductions, a fibrant algebraic weak factorization system on Grpd(Asm(A)), dependent products along fibrations, and begins the W-types-with-reductions construction that feeds the small object argument. The central claims depend on a quotient-by-PER construction in §4.2 and on the preliminary combinatorics of Section 2.1.

Significance. If the main theorem is correct, it would provide a new, explicit realizability-based model of homotopy type theory with a univalent impredicative universe, and a bridge between groupoid assemblies and the realizability topos RT[A] via 0-types. The paper is constructive in ambition: it gives explicit realizers, explicit comma-category factorizations, and explicit W-type carriers. These strengths are real, even though the paper does not ship machine-checked proofs or reproducible code. However, the current version does not deliver the verification needed at the key quotient step, and several concrete errors in the basic combinators make the realizer computations unreliable. The final claim is therefore plausible but not yet established to the standard of a journal proof.

major comments (4)
  1. [§2.1] Section 2.1 is internally inconsistent. The line 'k = ⟨x,y⟩y = k·ι' together with Definition 2.1.1(i) would require (k·x)·y to be both x and y, and the two displayed terms for p0 and p1 are identical despite being intended as different projections. The pairing and projection realizers in Lemma 2.2.6 and throughout the rest of the paper are built from exactly these terms, so all concrete realizer calculations would have to be re-checked once the definitions are corrected. This is a load-bearing error in the foundations of the realizability structure.
  2. [§4.2, definition of ∼ and Lemmas 4.2.6–4.2.10] The quotient by ∼ is the load-bearing step for the W-type-with-reductions groupoid U, and hence for §4.3, §4.4, and §5. The relation ∼ is defined as a 'partial equivalence relation generated by' a list whose first clause is transitivity and whose remaining clauses are not explicitly closed under symmetry; Definition 4.2.3 defines 'functorial' and 'natural' using ∼ itself, and the second generating clause of ∼ uses those notions as a premise. This mutually recursive definition needs a fixed-point justification before it can support proofs. Lemma 4.2.10 then proves uniqueness by induction on ∼′ without a symmetry case, and Lemma 4.2.7 asserts that the groupoid operations descend 'well defined by definition of ∼ and Remark 4.2.5' without a direct verification that composition, inverses, and the algebra maps in Lemma 4.2.9 are independent of representatives. Because Asm(A) is not exact (Example 2.6.7), descent is not automatic, and this gap is load-bearing.
  3. [§2.6, around Lemma 2.6.8] In the W-types-with-reductions construction for Asm(A), the paper states that the construction requires Asm(A) to be exact, then notes in Example 2.6.7 that it is not exact, and proposes to use exactness of Set instead. The step 'Since Set is an exact category then t′(j) ∼′ t′′(j′)' in Lemma 2.6.8 is only valid if the relation ∼′ is already known to be the kernel pair of the quotient map s′; the text does not establish that. The same missing symmetry/closure issue from §4.2 appears here, and this construction is the Asm(A)-level precursor of the groupoid W-types, so the gap propagates.
  4. [§2.8, Lemma 2.8.4] In the proof of coequalizers in Grpd(Asm(A)), composition on mor CoEq[f,g] is not shown to be well-defined. For quotient morphisms t,t′ with dom(t′) = cod(t), one chooses representatives p,p′ with dom(p′) = cod(p); but for arbitrary representatives q,q′ with r(q)=t and r(q′)=t′, the assertion that q·q′ exists requires dom(q′) = cod(q) as elements of the object set, not merely up to the object quotient. The text then uses exactness of Set to conclude q ∼ p and q′ ∼ p′, but it does not verify that concatenation is compatible with the generating relation ∼ before concluding q·q′ ∼ p·p′. This needs repair because the coequalizer construction is part of finite colimits, which are used throughout the paper.
minor comments (5)
  1. [§2.2, Lemma 2.2.9] The composition formula for [G]∘[F] is displayed as ∃y(F(x,y) ∧ G(x,y)) with a repeated variable x; it should quantify a middle object and use G(y,z), and the subsequent fiber-product notation should be checked.
  2. [§2.5, Lemma 2.5.5] In the coproduct of partitioned assemblies, the realizer description writes {[k,rx] | a ∈ ϕ(x)} although the set should be a singleton and no use is made of a; this appears to be a copy-paste error.
  3. [§3.2, Lemma 3.2.2] The proof says '(I → X) → X×X is a normal isomorphism' where the claim and surrounding terminology require 'normal isofibration'; this typo is confusing in a section that defines that notion.
  4. [§4.1] The W-type construction repeatedly defers key groupoid and initiality arguments to [29] with phrases such as 'can be replicated in the internal language of Asm(A)' and 'the argument stated in Proposition 6.1.2 of [29]' without stating the exact hypotheses; these statements should be made explicit so the W-type construction is self-contained.
  5. [§2.1] The boolean/if-then-else realizer says 'setting k as true and k as false'; after correcting the combinators, the paper should use distinct terms for true and false (for example k and k·ι) consistently throughout.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the paper's main constructions reduce to external theorems and to an independently defined realizability topos, not to their own conclusions.

full rationale

The paper is a pure mathematics thesis with no fitted parameters and no empirical predictions, and its central benchmarks are externally anchored. RT[A] is defined in Section 2.2 via the tripos-to-topos construction from the independently given tripos P(A), before any groupoid-assembly theorem is stated; the later identification of the homotopy category of 0-types of pGrpd(Asm(A)) with RT[A] is therefore not definitionally circular. The W-type constructions in Sections 2.4 and 4.1 adapt classical Set-based W-type arguments and explicitly invoke external sources ([4], [8], [12], [19], [29]) for the parts imported rather than deriving those parts from the claims being proven. The W-types-with-reductions machinery in Sections 2.6 and 4.2 likewise follows the cited construction of [27], with the paper filling in realizability-specific details. The algebraic weak factorization system of Section 3 is verified by proving the monad laws and by citing an external theorem ([22, Theorem 2.24]); it is not obtained by assuming the model structure it is later used to build. The quotient step in Section 4.2 is the most delicate point: Asm(A) is not exact (Example 2.6.7), and the paper argues that one can nevertheless quotient in Set and use image factorization, asserting in Lemma 4.2.7 that the groupoid operations descend. If that descent proof is incomplete, the construction may fail, but a proof gap is not the same as a circular derivation. There is no self-citation chain carrying a load-bearing premise, no fitted input renamed as a prediction, and no result whose statement is identical to an assumption by construction. The close fit between the chosen normal isofibrations and the desired dependent products is a modeling design choice, not an equation that feeds back into itself. Accordingly, the appropriate circularity score is 0.

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

This is pure mathematics: there are no fitted parameters, and the only inputs are the PCA A and a Grothendieck universe U, both treated as data from the start. The axioms are the metatheory (ZFC, AC, WISC in Set), the size assumption (universes), the realizability semantics itself, and the soundness of heavy cited machinery ([8], [10], [22], [27], [29]). No invented entities in the sense of a postulated particle, force, or dimension appear: the interval groupoid I and the iso-comma fibrant replacement of Definition 3.2.5 are standard constructions, and the 'uniform normalized small object argument' of Section 4.3 is new machinery but is assembled from standard inputs. The most fragile assumption by far is the transfer of exactness into the non-exact category Asm(A) during the W-types-with-reductions quotient, because the paper itself flags non-exactness in Example 2.6.7.

assumptions (5)
  • standard math ZFC in the metatheory, in particular the Axiom of Choice.
    AC is used in Lemma 2.5.9 to identify partitioned assemblies with the projective objects of Asm(A), and it gives WISC in Set, which the paper needs for Lemma 2.6.5. The paper never states its metatheory explicitly.
  • domain assumption WISC (Weakly Initial Set of Covers) holds in Set.
    Lemma 2.6.5 is conditional ('If WISC holds in Set, then it holds in Asm(A)'), but Section 4.2 uses WISC in Asm(A) unconditionally to construct W-types with reductions, which in turn power the small object argument of Section 4.3 and the model structure.
  • domain assumption Grothendieck universes in Set.
    Section 2.7 constructs the full and modest object classifiers from a Grothendieck universe U, and the univalent universes claimed in Section 5.1 depend on these classifiers. This is the standard size-theoretic assumption for universes.
  • standard math Realizability semantics: the tripos-to-topos construction and the internal language of Asm(A).
    Section 2.2 builds RT[A] and Asm(A) from the Set-tripos P(A)- following [21], and all later sections reason in the internal language of Asm(A). This is standard background in the field.
  • standard math Correctness of the cited technical machinery: Proposition 2.4 of [10], Theorem 2.24 of [22], W-types with reductions of [27], internal-groupoid W-types of [29], W-types via decoration of [4], and Theorem 14 of [8].
    Load-bearing steps are delegated: Lemma 2.4.16 says it 'is meant to be a citation of Theorem 14 of [8]', Corollary 3.6.1 (Frobenius property) is obtained by 'applying Proposition 2.4 of [10]', Lemma 2.6.4 says 'This is Lemma 3.6 of [27]', and Section 4.1 'expounds on the results of sections 3.1 and 6.1 of [29]'. The central claims inherit any gaps in those results.

how reviews work

0 comments
Cite this review

Pith. "Pith review of A Model of Type Theory in Groupoid Assemblies." pith.science (2026). https://pith.science/paper/QRXRSCRT

@misc{pith2026250716062,
  author       = {Pith},
  title        = {Pith review of: A Model of Type Theory in Groupoid Assemblies},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/QRXRSCRT}},
  note         = {Machine review of arXiv:2507.16062}
}
abstract

We consider the category Grpd(Asm$(A)$) of groupoids defined internally to the category of assemblies on a partial combinatory algebra $A$. In this thesis we exhibit the structure of a $\pi$-tribe on Grpd(Asm$(A)$) showing the category to be a model of type theory. We also show that Grpd(Asm$(A)$) has $W$-types with reductions and univalent object classifier for assemblies and modest assemblies, where the latter is an impredicative object classifier. Using the $W$-types with reductions, we show that Grpd(Asm$(A)$) has a model structure. Finally, we construct pGrpd(Asm$(A)$), the full subcategory of partitioned groupoid assemblies, and show that pGrpd(Asm$(A)$) has finite bilimits and bicolimits as well as showing that the homotopy category of the full subcategory of the $0$-types of pGrpd(Asm$(A)$) is RT$[A]$, the realizability topos of $A$.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

31 extracted references · 21 canonical work pages

  1. [10]

    The Frobenius condition, right properness, and uniform fi- brations

    Nicola Gambino and Christian Sattler. “The Frobenius condition, right properness, and uniform fi- brations”. In: Journal of Pure and Applied Algebra 221.12 (2017), pp. 3027–3068. issn: 0022-4049. doi: https://doi.org/10.1016/j.jpaa.2017.02.013 . url: https://www.sciencedirect.com/ science/article/pii/S0022404917300385. 198

    doi:10.1016/j.jpaa.2017.02.013 2017

  2. [27]

    W-Types with Reductions and the Small Object Argument

    Andrew Swan. W-Types with Reductions and the Small Object Argument . 2018. arXiv: 1802.07588 [math.CT]

    work page Pith review arXiv 2018

  3. [29]

    Polynomial functors and W-types for groupoids

    Jakob Vidmar. “Polynomial functors and W-types for groupoids”. Sept. 2018. url: https://etheses. whiterose.ac.uk/22517/

    work page 2018

  4. [1]

    A cubical model of homotopy type theory

    Steve Awodey. A cubical model of homotopy type theory . Logic Colloquium 2015. 2018. doi: https: //doi.org/10.1016/j.apal.2018.08.002 . url: https://www.sciencedirect.com/science/ article/pii/S0168007218300861

    work page doi:10.1016/j.apal.2018.08.002 2015

  5. [2]

    Toward the effective 2-topos

    Steve Awodey and Jacopo Emmenegger. Toward the effective 2-topos . Mar. 2025. doi: 10 . 48550 / arXiv.2503.24279

    work page doi:10.48550/arxiv.2503.24279 2025

  6. [3]

    Homotopy theoretic models of identity types

    Steve Awodey and Michael A. Warren. “Homotopy theoretic models of identity types”. In: Mathemat- ical Proceedings of the Cambridge Philosophical Society 146.1 (Jan. 2009), pp. 45–55. issn: 1469-8064. doi: 10.1017/s0305004108001783. url: http://dx.doi.org/10.1017/S0305004108001783

    doi:10.1017/s0305004108001783 2009

  7. [4]

    Predicative topos theory and models for constructive set theory

    Benno van den Berg. “Predicative topos theory and models for constructive set theory”. In: 2006. url: https://api.semanticscholar.org/CorpusID:123268594

    work page 2006

  8. [5]

    Words, free algebras, and coequalizers

    Andreas Blass. “Words, free algebras, and coequalizers”. eng. In: Fundamenta Mathematicae 117.2 (1983), pp. 117–160. url: http://eudml.org/doc/211359

    work page 1983

Show all 31 references
  1. [6]

    Regular and exact completions

    A. Carboni and E.M. Vitale. “Regular and exact completions”. In: Journal of Pure and Applied Algebra 125.1 (1998), pp. 79–116. issn: 0022-4049. doi: https://doi.org/10.1016/S0022-4049(96)00115-6. url: https://www.sciencedirect.com/science/article/pii/S0022404996001156

    1998 doi

  2. [7]

    Categories of partial equivalence relations as localizations

    Jonas Frey. Categories of partial equivalence relations as localizations . 2023. doi: https://doi.org/ 10.1016/j.jpaa.2022.107115 . url: https://www.sciencedirect.com/science/article/pii/ S0022404922001116

    2023

  3. [8]

    Wellfounded Trees and Dependent Polynomial Functors

    Nicola Gambino and Martin Hyland. “Wellfounded Trees and Dependent Polynomial Functors”. In: vol. 3085. Apr. 2003. isbn: 978-3-540-22164-7. doi: 10.1007/978-3-540-24849-1_14

    2003 doi

  4. [9]

    Models of Martin-L¨ of Type Theory From Algebraic Weak Factorisation Systems

    Nicola Gambino and Marco Federico Larrea. “Models of Martin-L¨ of Type Theory From Algebraic Weak Factorisation Systems”. In: Journal of Symbolic Logic 88.1 (2023), pp. 242–289. doi: 10.1017/ jsl.2021.39

    2023

  5. [11]

    Understanding the Small Object Argument

    Richard Garner. “Understanding the Small Object Argument”. In: Applied Categorical Structures 17.3 (Apr. 2008), pp. 247–285. issn: 1572-9095. doi: 10.1007/s10485-008-9137-4 . url: http://dx.doi. org/10.1007/s10485-008-9137-4

    2008 doi

  6. [12]

    Well-foundedness in Realizability

    M. Hofmann, J. van Oosten, and T. Streicher. “Well-foundedness in Realizability”. In: Archive for Mathematical Logic 45.7 (2006), pp. 795–805. doi: 10 . 1007 / s00153 - 006 - 0003 - 5. url: https : //doi.org/10.1007/s00153-006-0003-5

    2006 doi

  7. [13]

    The groupoid interpretation of type theory

    Martin Hofmann and Thomas Streicher. “The groupoid interpretation of type theory”. In: Twenty-five years of constructive type theory (Venice, 1995) . Vol. 36. Oxford Logic Guides. Oxford Univ. Press, New York, 1998, pp. 83–111. isbn: 0-19-850127-7

    1995

  8. [14]

    The algebraic internal groupoid model of Martin-L¨ of type theory

    Calum Hughes. The algebraic internal groupoid model of Martin-L¨ of type theory . Mar. 2025. doi: 10.48550/arXiv.2503.17319

    2025 doi arXiv

  9. [15]

    Notes on Clans and Tribes

    Andre Joyal. Notes on Clans and Tribes . 2017. arXiv: 1710.10238 [math.CT]. url: https://arxiv. org/abs/1710.10238

    2017 arXiv

  10. [16]

    Realizability: a retrospective survey

    S. C. Kleene. “Realizability: a retrospective survey”. In: Cambridge Summer School in Mathematical Logic (Cambridge, 1971) . Vol. Vol. 337. Lecture Notes in Math. Springer, Berlin-New York, 1973, pp. 95–112

    1971

  11. [17]

    A 2-Categories Companion

    Stephen Lack. “A 2-Categories Companion”. In: Towards Higher Categories. Springer New York, Sept. 2009, pp. 105–191. isbn: 9781441915245. doi: 10.1007/978- 1- 4419- 1524- 5_4. url: http://dx. doi.org/10.1007/978-1-4419-1524-5_4

    2009 doi

  12. [18]

    Basic Bicategories

    Tom Leinster. Basic Bicategories. 1998. arXiv: math/9810017 [math.CT]. url: https://arxiv.org/ abs/math/9810017

    1998 arXiv

  13. [19]

    Wellfounded trees in categories

    Ieke Moerdijk and Erik Palmgren. “Wellfounded trees in categories”. In: Annals of Pure and Applied Logic 104.1 (2000), pp. 189–218. issn: 0168-0072. doi: https://doi.org/10.1016/S0168-0072(00) 00012-9. url: https://www.sciencedirect.com/science/article/pii/S0168007200000129

    2000 doi

  14. [20]

    Basic category theory

    Jaap van Oosten. “Basic category theory”. In: BRICS Lecture Series LS-95-01. Aarhus Universitet., 1995, pp. 83

    1995

  15. [21]

    Realizability: an introduction to its categorical side

    Jaap van Oosten. Realizability: an introduction to its categorical side. Vol. 152. Studies in Logic and the Foundations of Mathematics. Elsevier B. V., Amsterdam, 2008, pp. xvi+310. isbn: 978-0-444-51584-1

    2008

  16. [22]

    Algebraic model structures

    Emily Riehl. “Algebraic model structures.” eng. In: The New York Journal of Mathematics [electronic only] 17 (2011), pp. 173–231. url: http://eudml.org/doc/226868

    2011

  17. [23]

    Categorical Homotopy Theory

    Emily Riehl. Categorical Homotopy Theory . New Mathematical Monographs. Cambridge University Press, 2014. 199

    2014

  18. [24]

    Modalities in homotopy type theory

    Egbert Rijke, Michael Shulman, and Bas Spitters. “Modalities in homotopy type theory”. In: Logical Methods in Computer Science Volume 16, Issue 1 (Jan. 2020). issn: 1860-5974. doi: 10.23638/lmcs- 16(1:2)2020. url: http://dx.doi.org/10.23638/LMCS-16(1:2)2020

    2020 doi

  19. [25]

    All (∞, 1)-toposes have strict univalent universes

    Michael Shulman. All (∞, 1)-toposes have strict univalent universes. 2019. arXiv: 1904.07004 [math.AT]

    2019 arXiv

  20. [26]

    Fibrations in bicategories

    Ross Street. “Fibrations in bicategories”. en. In: Cahiers de topologie et g´ eom´ etrie diff´ erentielle21.2 (1980), pp. 111–160. url: https://www.numdam.org/item/CTGDC_1980__21_2_111_0/

    1980

  21. [28]

    Cubical Assemblies, a Univalent and Impredicative Universe and a Failure of Proposi- tional Resizing

    Taichi Uemura. “Cubical Assemblies, a Univalent and Impredicative Universe and a Failure of Proposi- tional Resizing”. In: 24th International Conference on Types for Proofs and Programs (TYPES 2018) . Ed. by Peter Dybjer, Jos´ e Esp ´ ırito Santo, and Lu ´ ıs Pinto. Vol. 130. ...

    2018 doi

  22. [30]

    The Origins and Motivations of Univalent Foundations: A Personal Mission to Develop Computer Proof Verification to Avoid Mathematical Mistakes

    Vladimir Voevodsky. “The Origins and Motivations of Univalent Foundations: A Personal Mission to Develop Computer Proof Verification to Avoid Mathematical Mistakes”. The Institute Letter Summer

  23. [2014]

    url: https://www.ias.edu/ideas/2014/voevodsky-origins

    2014. url: https://www.ias.edu/ideas/2014/voevodsky-origins. Email address: aagwu1@jh.edu Department of Mathematics, Johns Hopkins University, Baltimore, MD 21218 200

    2014

Pith tools

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