Pith. sign in

REVIEW 2 major objections 6 minor 1 cited by

Synthetic perspectives on spaces and categories

T0 review · 2 major / 6 minor · reviewed 2026-08-04 · deepseek-v4-flash

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

Pith's one-line read Homotopy type theory and simplicial type theory make spaces and categories natively equivalence-invariant, via path induction, arrow induction, and (directed) univalence.

desk verdict A careful, honest exposition of path and arrow induction with two small genuine improvements, but the advertised directed univalent universe is deferred and Definition 7.1 is circular as written. read the letter →

arxiv 2510.15795 v2 pith:MFJZN6VP submitted 2025-10-17 math.CT math.ATmath.LO

Emily Riehl This is my paper · ORCID
classification math.CTmath.ATmath.LO MSC 18N6003B38
keywords homotopytypetheorysimplicialsynthetic∞-categoriespathinductionarrowunivalencedirectedYonedalemma
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 is an exposition of a program: use two new formal systems—homotopy type theory for spaces and simplicial type theory for categories—so that equivalence-invariance is built in rather than proven separately. Its core technical message is that two induction principles carry the weight. Path induction says a construction over all paths is determined by its values on constant paths; arrow induction says a construction over all arrows out of an object is determined by its value on the identity arrow. When these are internalized in universes, univalence identifies paths in the universe with equivalences, and directed univalence identifies arrows with functors. A sympathetic reader should care because this makes the Yoneda lemma and the category of spaces genuinely synthetic results, and it suggests a route to formalized higher category theory.

What carries the argument

Path induction is the principle that a fibration over a path space is determined by its behavior on constant paths; the paper proves it via a lifting property of the inclusion of constant paths against fibrations, with a weakening version requiring the Frobenius condition. Arrow induction is the directed analogue for covariant families over the coslice category c/C: sections are determined by the value at the identity arrow. The universes—univalent for spaces, directed univalent for categories—are the objects that internalize these principles and make them available for classifying constructions such as the category of spaces. The paper treats these induction principles and universes as the

What would settle it

Look for a covariant family of simplicial spaces over some coslice category c/C whose sections are not equivalent to the fiber over the identity arrow id_c; arrow induction predicts none exists. Finding one would invalidate the Yoneda lemma and the directed-univalent category of spaces. On the universe side, the decisive test is whether suitably structured left fibrations form a locally representable, small-groupoid-valued fibred structure; if not, the directed universe does not exist and Corollary 7.2 is unsupported.

Watch

Extended reading notes

Core claim

The paper's central claim is that the fundamental proof techniques of homotopy type theory have directed analogues in simplicial type theory, and that both are valid in concrete simplicial semantics. On the space side, Proposition 3.10 states that to define a section of a fibration over a path space, it suffices to define a partial section over the subspace of constant paths; this is path induction. On the category side, Proposition 6.7 states that to define a section of a covariant family over the coslice category c/C, it suffices to define the image of the identity arrow; this is arrow induction. The universe-level versions are univalence (paths in the universe are equivalences) and direct

Load-bearing premise

The paper's conclusion about the category of spaces rests on a cited—but not proved here—construction of a universal covariant family with directed univalence; if that construction fails, the category of spaces is unsupported, and separately the weakened form of path induction needs the Frobenius condition for the model structure.

Editorial extensions

If this is right

  • Every construction in the synthetic language is automatically equivalence-invariant; there is no separate step of proving that a construction respects equivalences of spaces or categories.
  • The Yoneda lemma for covariant families follows directly from arrow induction, and in the synthetic setting it is simpler to state and prove than its strict 1-categorical counterpart.
  • The base of the universal covariant family is a category—the category of spaces—whose points are groupoids and whose total space is the category of pointed spaces.
  • Directed univalence gives a structure homomorphism principle: arrows in classifying categories built from the universe are literally homomorphisms of the relevant structures.
  • Formalization in a proof assistant is feasible for these results, and the paper notes that formalizing earlier synthetic-category proofs has already caught a circular-reasoning error in a published proof.

Reading between the lines

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

  • If directed univalence is proved in the intended generality—simplicial objects in any ∞-topos—the same synthetic language should apply not only to spaces but also to sheaves and stacks, giving a uniform internal way to develop derived algebraic geometry.
  • Arrow induction is one instance of a broader pattern: any initial object in a categorical setting should generate a section-induction principle for covariant families; the paper does not explore this generalization, but it is a natural next step.
  • The gap between the universe construction sketched here and the cited forthcoming proof is the critical missing brick; until that proof appears, the category of spaces should be read as conditional rather than established.
  • A shared synthetic language for spaces and categories may eventually let mathematicians transfer theorems between homotopy theory and category theory without translation, because both are governed by the same pair of induction principles and 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

2 major / 6 minor

Summary. This note presents a synthetic perspective on spaces and categories, developed in parallel through homotopy type theory and simplicial type theory. The author derives path induction from the Quillen model structure on simplicial sets (§3), constructs univalent universes via Shulman's fibred-structure framework (§4), and then introduces arrow induction as a synthetic form of the Yoneda lemma for precategories (§6). The final section sketches directed univalent universes for covariant families, from which the author claims a 'category of spaces' (§7). The exposition is clear and the proofs of path induction and arrow induction are elegant and standard. However, the central new claim—directed univalence—is deferred to a forthcoming paper [17] and the presentation of Definition 7.1 contains a potential circular dependency on the category structure of S.

Significance. If the deferred directed-univalence construction in [17] succeeds, this note would offer a valuable synthetic foundation for ∞-category theory, complementing existing analytic approaches. The paper's explicit use of machine-checked formalization, especially the Rzk library and the formalized Yoneda lemma [42], is a significant strength: it provides independent verification of the arrow-induction principles and catches earlier proof errors. The exposition of path induction and arrow induction is pedagogically useful and could serve as a compact reference. However, because the paper's most novel assertion—Corollary 7.2 and the directed univalent universe—rests entirely on an in-preparation citation, the significance is conditional. The paper is best viewed as a survey of existing techniques plus a preview of ongoing work, not as a self-contained proof of directed univalence.

major comments (2)
  1. [§7.1, Corollary 7.2] The central construction of §7 is not proved in this paper. The text states 'See [17] for more details and a proof that the universal covariant family ϱ:S* ↠ S is directed univalent', and [17] is listed as 'in preparation, 2025'. Corollary 7.2 then asserts that the base S is a category, which is the main application of directed univalence. As written, this is an unverified assertion, not a result of the present note. If the paper is intended as a survey, Corollary 7.2 should be explicitly labelled as a theorem from forthcoming work, and the dependence on [17] should be highlighted in the abstract and introduction. This is load-bearing because all applications in §7.2 depend on it.
  2. [§7.1, Definition 7.1] Definition 7.1 defines directed univalence using 'arr-to-fun := arrow-ind(id↦id)', appealing to Proposition 6.7. That proposition is stated for a category C, and the introduction to §6 says the results apply to precategories. At the point of Definition 7.1, the base S of the universal covariant family has not yet been shown to be a precategory; Corollary 7.2, which states that S is a category, is derived later from directed univalence. This creates a circular dependency in the presentation. The paper should either prove (or cite a proof) that S is a precategory before using arrow induction, or clarify that a version of arrow induction not requiring the base to be a precategory is being used. As written, the definition presupposes the structure it is meant to establish.
minor comments (6)
  1. [§4.1, after Construction 4.1] The text says 'By Theorem 3.11' but the reference should be to Remark 3.11. There is no Theorem 3.11 in the paper.
  2. [§4.1, Lemma 4.2] The phrase 'if and only if and only if' contains a duplicated 'and only if'.
  3. [§7, first paragraph] The name 'Voevdosky' should be 'Voevodsky'.
  4. [§1.1, Abstract] The word 'prospective' appears to be a typo for 'perspective' in the abstract and in §1.1. Also 'prospective' in the abstract: 'provide a prospective on spaces'.
  5. [§4.3, Examples 4.8–4.10] The headings 'Theorem 4.8' and 'Theorem 4.9' are mismatched with their content; these are examples, not theorems, and should be labelled consistently (e.g., 'Example').
  6. [§6.1, Lemma 6.6] The footnote about the original published proof error in [55] is informative, but the wording 'had an error of circular reasoning' could be softened to 'contained a circular argument' for a more neutral tone.

Circularity Check

2 steps flagged · score 5.0 of 10

Directed-univalence construction is deferred to an in-preparation self-citation, and Definition 7.1 applies arrow induction to S before S is shown to be a category/precategory; the path- and arrow-induction core is otherwise self-contained.

  1. self citation load bearing [§7.1 (Definition 7.1 and following paragraph); §7.2 Corollary 7.2; reference [17]]
    "See [17] for more details and a proof that the universal covariant family ϱ:S•↠S is directed univalent. ... Corollary 7.2. The base of the universal covariant family defines a category. ... [17] E. Cavallo, E. Riehl, and C. Sattler, Directed univalence for simplicial objects in an ∞-topos. in preparation, 2025."

    The central new construction of the note — a directed univalent universe whose base is a category — is not proved here. The paper states that suitably structured left fibrations 'admits a universe ϱ:S∗↠S that is univalent' and then delegates the directed-univalence proof to [17], an in-preparation paper co-authored by the present author. Corollary 7.2, the 'category of spaces', is therefore supported only by a self-citation whose proof is not available, machine-checked, or otherwise independently verified in the manuscript. This is a load-bearing self-citation: without [17] the derivation chain for Corollary 7.2 has no displayed proof.

  2. self definitional [Definition 7.1 and footnote 6, §7.1; Proposition 6.7; Corollary 7.2]
    "arr-to-fun := arrow-ind(id↦id). ... Corollary 7.2. The base of the universal covariant family defines a category. ... Here the arrow induction principle of Proposition 6.7 should be interpreted in context S, holding the variable A:S fixed."

    Definition 7.1 defines directed univalence by applying arrow induction (Proposition 6.7) to S. In the paper, Proposition 6.7 is stated as 'Fix a category C' (with §6 adding that it applies to precategories), and its semantic justification uses the initial object of the coslice category c/C. Corollary 7.2, which is supposed to follow from directed univalence, is the first statement that S is a category. The manuscript never proves that S is a precategory before Definition 7.1, so the definition's use of arrow induction appears to presuppose the structure that directed univalence is meant to establish. The paper defers the resolution to [17], which is not included; if [17] first proves S is a precategory the circularity is repaired, but the present text does not show that.

full rationale

The bulk of the note is a self-contained exposition against an external benchmark: path induction (Prop 3.10) is derived from Quillen's model structure on sSet (Thm 2.2) plus the Frobenius condition [32], and arrow induction (Prop 6.7) is justified by initiality of id_c in c/C. The Yoneda lemma (Prop 6.8) and the equivalence-invariance consequences are consequences of those derivations, not assumptions of them. The note also corrects a genuine prior circular-reasoning error by citing the machine-checked Rzk formalization [42] (footnote 5), which is independent support. The only load-bearing step that is not self-contained is §7: the existence of a directed univalent universe and Corollary 7.2 are deferred to [17], an in-preparation paper with overlapping authorship. Moreover, Definition 7.1 applies arrow induction to S before S is shown to be a category/precategory, making the definition's well-formedness depend on the very conclusion (Cor 7.2) unless [17] supplies the missing intermediate proof. Because this is the paper's advertised directed-univalence contribution and no proof or independent verification is given, it is more than a minor self-citation; however, it does not invalidate the independent path/arrow-induction core, so the circularity score is moderate.

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

All quantities here are mathematical, so there are no fitted parameters; footnote 2's regular cardinal κ is a standard size bound, not a fitted value. The axioms are the published model-category and topos-theoretic results on which the semantic proofs rest; none is invented for this paper. The directed univalent universe is the one genuinely deferred item: its existence and directed univalence (Definition 7.1, Corollary 7.2) are cited to the authors' own in-preparation manuscript [17], which a reader cannot yet check. The paper introduces no new entities: the directed interval 2 and the universe S originated in [55] and [17] respectively; this note only previews them.

assumptions (6)
  • standard math Quillen's simplicial model structure on sSet: cofibrations are monomorphisms, right proper (Theorem 2.2)
    Cited to Quillen [50]; the trivial-cofibration lifting properties that drive path induction (§3) and the universe construction (§4) all come from this theorem.
  • standard math Frobenius condition: trivial cofibrations are stable under pullback along fibrations (Gambino–Sattler [32])
    Explicitly invoked before Proposition 3.5 as what extends path induction to weakening; without it the intermediate/final forms of path induction (Props 3.5, 3.10) do not follow.
  • standard math Stability of the model structure under slicing (Remark 3.11): 'all of the properties of Theorem 2.2 are stable under slicing'
    Lets path induction and univalence be stated in arbitrary contexts Γ; the paper notes the model structure is simplicial rather than cartesian-closed precisely for this reason.
  • standard math Joyal's theorem: the classifying 1-topos of the strict-interval theory is the 1-category of simplicial sets ([45, §VIII.8])
    Invoked in §5 to build the walking arrow 2 and walking composable pairs 3, linking the axiomatic directed interval to the simplicial model.
  • standard math HoTT interprets in any ∞-topos (Shulman [61]); small groupoid-valued, locally representable fibred structures admit univalent universes
    Used in §1.1 and §4.2 to claim the constructions are valid beyond sSet and to construct the univalent universe U; the proof is cited to Shulman's published paper.
  • domain assumption Suitably structured left fibrations form a small groupoid valued, locally representable fibred structure admitting a directed univalent universe ϱ: S• ↠ S (Definition 7.1, Corollary 7.2)
    The paper states this and defers the proof: 'See [17] for more details and a proof that the universal covariant family... is directed univalent', where [17] is Cavallo–Riehl–Sattler, 'in preparation, 2025'. The strongest new claim of §7 rests on unpublished work.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Synthetic perspectives on spaces and categories." pith.science (2026). https://pith.science/paper/MFJZN6VP

@misc{pith2026251015795,
  author       = {Pith},
  title        = {Pith review of: Synthetic perspectives on spaces and categories},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/MFJZN6VP}},
  note         = {Machine review of arXiv:2510.15795}
}
read the original abstract

Recently discovered domain-specific formal systems -- specifically homotopy type theory and simplicial type theory -- provide new perspectives on spaces and categories in a natively equivalence-invariant setting. In this note, we expose fundamental proof techniques from these parallel settings: describing induction principles over paths or arrows and constructions involving universes that are either univalent or directed univalent.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Internal Algebraic Type Theory

    math.CT 2026-07 conditional novelty 7.0 of 10

    Maps that are exponentiable with respect to a family of maps give polynomial functors and an algebraic model of directed type theory in the category of categories with hom-types.

Reference graph

Works this paper leans on

69 extracted references · 11 canonical work pages · cited by 1 Pith paper

  1. [17]

    Cavallo, E

    E. Cavallo, E. Riehl, and C. Sattler , Directed univalence for simplicial objects in an -topos . in preparation, 2025

    2025

  2. [55]

    Riehl and M

    E. Riehl and M. Shulman , A type theory for synthetic -categories , High. Struct., 1 (2017), pp. 147--224, https://doi.org/10.1007/s42001-017-0005-6

    doi:10.1007/s42001-017-0005-6 2017

  3. [42]

    Kudasov, E

    N. Kudasov, E. Riehl, and J. Weinberger , Formalizing the -categorical yoneda lemma , in Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, New York, NY, USA, 2024, Association for Computing Machinery, p. 274–290, https://doi.org/10.1145/3636501.3636945

    arXiv 2024

  4. [1]

    A. A. Abounegm, F. Bakke, C. B. Mart\' i nez, J. Campbell, R. Carlier, T. Chatzidiamantis-Christoforidis, A. Ergus, M. Hutzler, N. Kudasov, K. Maillard, D. M. Carpena, S. Pradal, N. Rasekh, E. Riehl, F. Verity, T. Walde, and J. Weinberger , Simplicial H o TT and synthetic -categories , https://github.com/rzk-lang/rzk. a formalization library

  5. [3]

    Altenkirch, Y

    T. Altenkirch, Y. Chamoun, A. Kaposi, and M. Shulman , Internal parametricity, without an interval , Proc. ACM Program. Lang., 8 (2024), https://doi.org/10.1145/3632920

    work page doi:10.1145/3632920 2024

  6. [4]

    Antol\'in Camarena , A whirlwind tour of the world of ( ,1) -categories , in Mexican mathematicians abroad: recent contributions, vol

    O. Antol\'in Camarena , A whirlwind tour of the world of ( ,1) -categories , in Mexican mathematicians abroad: recent contributions, vol. 657 of Contemp. Math., Amer. Math. Soc., Providence, RI, 2016, pp. 15--61, https://doi.org/10.1090/conm/657/13088

    work page doi:10.1090/conm/657/13088 2016

  7. [5]

    Awodey, E

    S. Awodey, E. Cavallo, T. Coquand, E. Riehl, and C. Sattler , The equivariant model structure on cartesian cubical sets , 2025, https://arxiv.org/abs/2406.18497

    arXiv 2025

  8. [6]

    Awodey and M

    S. Awodey and M. A. Warren , Homotopy theoretic models of identity types , Math. Proc. Cambridge Philos. Soc., 146 (2009), pp. 45--55, https://doi.org/10.1017/S0305004108001783

    doi:10.1017/s0305004108001783 2009

Show all 69 references
  1. [7]

    Bardomiano Mart\' i nez , Limits and colimits of synthetic -categories , 2024, https://arxiv.org/abs/2202.12386

    C. Bardomiano Mart\' i nez , Limits and colimits of synthetic -categories , 2024, https://arxiv.org/abs/2202.12386

    2024

  2. [8]

    J. E. Bergner , The homotopy theory of ( , 1) -categories , vol. 90 of London Mathematical Society Student Texts, Cambridge University Press, Cambridge, 2018

    2018

  3. [9]

    Bezem, U

    M. Bezem, U. Buchholtz, P. Cagne, B. I. Dundas, and D. R. Grayson , Symmetry . https://github.com/UniMath/SymmetryBook

  4. [10]

    Blechschmidt , Using the internal language of toposes in algebraic geometry , PhD thesis, Universit\" a t Augsberg, 2017

    I. Blechschmidt , Using the internal language of toposes in algebraic geometry , PhD thesis, Universit\" a t Augsberg, 2017

    2017

  5. [11]

    J. M. Boardman and R. M. Vogt , Homotopy invariant algebraic structures on topological spaces , vol. 347 of Lecture Notes in Mathematics, Springer, 1973, https://doi.org/10.1007/BFb0068547

    1973 doi

  6. [12]

    Brunerie , The J ames construction and _4( S ^3) in homotopy type theory , J

    G. Brunerie , The J ames construction and _4( S ^3) in homotopy type theory , J. Automat. Reason., 63 (2019), pp. 255--284, https://doi.org/10.1007/s10817-018-9468-2

    2019 doi

  7. [13]

    Buchholtz, J

    U. Buchholtz, J. D. Christensen, J. G. T. Flaten, and E. Rijke , Central h-spaces and banded types , Journal of Pure and Applied Algebra, 229 (2025), p. 107963, https://doi.org/https://doi.org/10.1016/j.jpaa.2025.107963, https://www.sciencedirect.com/science/article/pii/S00224...

    2025

  8. [14]

    Buchholtz, F

    U. Buchholtz, F. van Doorn, and E. Rijke , Higher groups in homotopy type theory , in Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '18, New York, NY, USA, 2018, Association for Computing Machinery, p. 205–214, https://doi.org/10.1145/320...

    2018

  9. [15]

    Buchholtz and J

    U. Buchholtz and J. Weinberger , Synthetic fibered ( ,1) -category theory , High. Struct., 7 (2023), pp. 74--165

    2023

  10. [16]

    Cavallo, A

    E. Cavallo, A. M \"o rtberg, and A. W. Swan , Unifying Cubical Models of Univalent Type Theory , in 28th EACSL Annual Conference on Computer Science Logic (CSL 2020), M. Fern \'a ndez and A. Muscholl, eds., vol. 152 of Leibniz International Proceedings in Informatics (LIPIcs),...

    2020 doi

  11. [18]

    Cavallo and C

    E. Cavallo and C. Sattler , Relative elegance and cartesian cubes with one connection , Canadian Journal of Mathematics, (2025), p. 1–64, https://doi.org/10.4153/S0008414X25101466

    2025 doi

  12. [19]

    K. e. C esnavi c ius and P. Scholze , Purity for flat cohomology , Ann. of Math. (2), 199 (2024), pp. 51--180, https://doi.org/10.4007/annals.2024.199.1.2

    2024 doi

  13. [20]

    Cherubini, T

    F. Cherubini, T. Coquand, F. Geerligs, and H. Moeneclaey , A Foundation for Synthetic Stone Duality , in 30th International Conference on Types for Proofs and Programs (TYPES 2024), R. E. M gelberg and B. van den Berg, eds., vol. 336 of Leibniz International Proceedings in Inf...

    2024 doi

  14. [21]

    Cherubini, T

    F. Cherubini, T. Coquand, and M. Hutzler , A foundation for synthetic algebraic geometry , Mathematical Structures in Computer Science, 34 (2024), p. 1008–1053, https://doi.org/10.1017/S0960129524000239

    2024 doi

  15. [22]

    Cisinski , Higher categories and homotopical algebra , vol

    D.-C. Cisinski , Higher categories and homotopical algebra , vol. 180 of Cambridge Studies in Advanced Mathematics, Cambridge University Press, Cambridge, 2019, https://doi.org/10.1017/9781108588737

    2019 doi

  16. [23]

    Cisinski, B

    D.-C. Cisinski, B. Cnossen, K. Nguyen, and T. Walde , Formalization of higher categories . Book in progress, https://drive.google.com/file/d/1lKaq7watGGl3xvjqw9qHjm6SDPFJ2-0o

  17. [24]

    Cisinski and H

    D.-C. Cisinski and H. K. Nguyen , The universal cocartesian fibration , 2022, https://arxiv.org/abs/2210.08945

    2022 arXiv

  18. [25]

    Clausen and P

    D. Clausen and P. Scholze , Lectures on analytic geometry . lecture notes for course WS 19/20, 2020, https://people.mpim-bonn.mpg.de/scholze/Analytic.pdf

    2020

  19. [26]

    Coquand and N

    T. Coquand and N. A. Danielsson , Isomorphism is equality , Indagationes Mathematicae, 24 (2013), pp. 1105--1120, https://doi.org/https://doi.org/10.1016/j.indag.2013.09.002. In memory of N.G. (Dick) de Bruijn (1918–2012)

    2013 doi

  20. [27]

    W. G. Dwyer, P. S. Hirschhorn, D. M. Kan, and J. H. Smith , Homotopy limit functors on model categories and homotopical categories , vol. 113 of Mathematical Surveys and Monographs, American Mathematical Society, Providence, RI, 2004, https://doi.org/10.1090/surv/113

    2004 doi

  21. [28]

    Eilenberg and J

    S. Eilenberg and J. A. Zilber , Semi-simplicial complexes and singular homology , Ann. of Math. (2), 51 (1950), pp. 499--513, https://doi.org/10.2307/1969364

    1950 doi

  22. [29]

    P. Freyd , Properties invariant within equivalence types of categories , in Algebra, topology, and category theory (a collection of papers in honor of S amuel E ilenberg), Academic Press, New York-London, 1976, pp. 55--61

    1976

  23. [30]

    Gabriel and M

    P. Gabriel and M. Zisman , Calculus of fractions and homotopy theory , vol. Band 35 of Ergebnisse der Mathematik und ihrer Grenzgebiete [Results in Mathematics and Related Areas], Springer-Verlag New York, Inc., New York, 1967

    1967

  24. [31]

    Gambino and R

    N. Gambino and R. Garner , The identity type weak factorisation system , Theoret. Comput. Sci., 409 (2008), pp. 94--109, https://doi.org/10.1016/j.tcs.2008.08.030

    2008 doi

  25. [32]

    Gambino and C

    N. Gambino and C. Sattler , The F robenius condition, right properness, and uniform fibrations , J. Pure Appl. Algebra, 221 (2017), pp. 3027--3068, https://doi.org/10.1016/j.jpaa.2017.02.013

    2017 doi

  26. [33]

    Gratzer, J

    D. Gratzer, J. Weinberger, and U. Buchholtz , Directed univalence in simplicial homotopy type theory , 2024, https://arxiv.org/abs/2407.09146

    2024

  27. [34]

    Gratzer, J

    D. Gratzer, J. Weinberger, and U. Buchholtz , The Y oneda embedding in simplicial type theory , 2025, https://arxiv.org/abs/2501.13229

    2025

  28. [35]

    Grothendieck , Sur quelques points d'alg\`ebre homologique , Tohoku Math

    A. Grothendieck , Sur quelques points d'alg\`ebre homologique , Tohoku Math. J. (2), 9 (1957), pp. 119--221, https://doi.org/10.2748/tmj/1178244839

    1957

  29. [36]

    Grothendieck , Pursuing stacks (\`a la poursuite des champs)

    A. Grothendieck , Pursuing stacks (\`a la poursuite des champs). V ol. I , vol. 20 of Documents Math\'ematiques (Paris) [Mathematical Documents (Paris)], Soci\'et\'e Math\'ematique de France, Paris, [2022] 2022

    2022

  30. [37]

    Joyal , Quasi-categories and K an complexes , vol

    A. Joyal , Quasi-categories and K an complexes , vol. 175, 2002, pp. 207--222, https://doi.org/10.1016/S0022-4049(02)00135-4. Special volume celebrating the 70th birthday of Professor Max Kelly

    2002 doi

  31. [38]

    D. M. Kan , On c. s. s. complexes , Amer. J. Math., 79 (1957), pp. 449--476, https://doi.org/10.2307/2372558

    1957 doi

  32. [39]

    Kapulkin and P

    K. Kapulkin and P. L. Lumsdaine , The simplicial model of univalent foundations (after V oevodsky) , J. Eur. Math. Soc. (JEMS), 23 (2021), pp. 2071--2126, https://doi.org/10.4171/JEMS/1050

    2021 doi

  33. [40]

    Kazhdan and Y

    D. Kazhdan and Y. Varshavsky , The Y oneda lemma for complete S egal spaces , Funktsional. Anal. i Prilozhen., 48 (2014), pp. 3--38, https://doi.org/10.1007/s10688-014-0050-3

    2014 doi

  34. [41]

    Kudasov , Rzk , https://github.com/rzk-lang/rzk

    N. Kudasov , Rzk , https://github.com/rzk-lang/rzk. An experimental proof assistant based on a type theory for synthetic -categories

  35. [43]

    om and A. M\

    A. Ljungstr\"om and A. M\"ortberg , Formalizing _4( S^3) Z/2 Z and computing a B runerie number in cubical A gda , in 2023 38th A nnual ACM / IEEE S ymposium on L ogic in C omputer S cience ( LICS ), IEEE Comput. Soc. Press, Los Alamitos, CA, [2023] 2023, p. 13

    2023

  36. [44]

    Lurie , Higher topos theory , vol

    J. Lurie , Higher topos theory , vol. 170 of Annals of Mathematics Studies, Princeton University Press, Princeton, NJ, 2009, https://doi.org/10.1515/9781400830558

    2009 doi

  37. [45]

    Mac Lane and I

    S. Mac Lane and I. Moerdijk , Sheaves in geometry and logic , Universitext, Springer-Verlag, New York, 1994. A first introduction to topos theory, Corrected reprint of the 1992 edition

    1994

  38. [46]

    Makkai , First order logic with dependent sorts, with applications to category theory

    M. Makkai , First order logic with dependent sorts, with applications to category theory . www.math.mcgill.ca/makkai/, 1995

    1995

  39. [47]

    Martini , Yoneda's lemma for internal higher categories , 2022, https://arxiv.org/abs/2103.17141

    L. Martini , Yoneda's lemma for internal higher categories , 2022, https://arxiv.org/abs/2103.17141

    2022 arXiv

  40. [48]

    Martini and S

    L. Martini and S. Wolf , Colimits and cocompletions in internal higher category theory , High. Struct., 8 (2024), pp. 97--192

    2024

  41. [49]

    J. P. Nichols-Barrer , On Quasi-Categories as a Foundation for Higher Algebraic Stacks , PhD thesis, Massachusetts Institute of Technology, 2007, https://arxiv.org/abs/1721.1/39088

    2007

  42. [50]

    D. G. Quillen , Homotopical algebra , vol. No. 43 of Lecture Notes in Mathematics, Springer-Verlag, Berlin-New York, 1967

    1967

  43. [51]

    Rasekh , Simplicial H omotopy T ype T heory is not just S implicial: W hat are - C ategories? , 2025, https://arxiv.org/abs/2508.07737

    N. Rasekh , Simplicial H omotopy T ype T heory is not just S implicial: W hat are - C ategories? , 2025, https://arxiv.org/abs/2508.07737

    2025 arXiv

  44. [52]

    Rezk , Toposes and homotopy toposes

    C. Rezk , Toposes and homotopy toposes . notes based on lectures at UIUC in Fall 2005, 2005, https://rezk.web.illinois.edu/homotopy-topos-sketch.pdf

    2005

  45. [53]

    Riehl , Could -category theory be taught to undergraduates? , Notices Amer

    E. Riehl , Could -category theory be taught to undergraduates? , Notices Amer. Math. Soc., 70 (2023), pp. 727--736, https://www.ams.org/journals/notices/202305/noti2692/noti2692.html

    2023

  46. [54]

    Riehl , On the -topos semantics of homotopy type theory , Bull

    E. Riehl , On the -topos semantics of homotopy type theory , Bull. Lond. Math. Soc., 56 (2024), pp. 461--517, https://doi.org/10.1112/blms.12997

    2024 doi

  47. [56]

    Riehl and D

    E. Riehl and D. Verity , Fibrations and Y oneda's lemma in an -cosmos , J. Pure Appl. Algebra, 221 (2017), pp. 499--564, https://doi.org/10.1016/j.jpaa.2016.07.003

    2017 doi

  48. [57]

    Riehl and D

    E. Riehl and D. Verity , Elements of -Category Theory , Cambridge Studies in Advanced Mathematics, Cambridge University Press, 2022, https://doi.org/10.1017/9781108936880

    2022 doi

  49. [58]

    Rijke , Introduction to Homotopy Type Theory , Cambridge Studies in Advanced Mathematics, Cambridge University Press, 2025, https://arxiv.org/abs/2212.11082

    E. Rijke , Introduction to Homotopy Type Theory , Cambridge Studies in Advanced Mathematics, Cambridge University Press, 2025, https://arxiv.org/abs/2212.11082

    2025 arXiv

  50. [59]

    Shulman , The univalence axiom for elegant R eedy presheaves , Homology Homotopy Appl., 17 (2015), pp

    M. Shulman , The univalence axiom for elegant R eedy presheaves , Homology Homotopy Appl., 17 (2015), pp. 81--106, https://doi.org/10.4310/HHA.2015.v17.n2.a6

    2015 doi

  51. [60]

    Shulman , Homotopy type theory: a synthetic approach to higher equalities , in Categories for the working philosopher, Oxford Univ

    M. Shulman , Homotopy type theory: a synthetic approach to higher equalities , in Categories for the working philosopher, Oxford Univ. Press, Oxford, 2017, pp. 36--57

    2017

  52. [61]

    Shulman , All ( ,1) -toposes have strict univalent universes , 2019, https://arxiv.org/abs/1904.07004

    M. Shulman , All ( ,1) -toposes have strict univalent universes , 2019, https://arxiv.org/abs/1904.07004

    2019 arXiv

  53. [62]

    Shulman , Strange new universes: proof assistants and synthetic foundations , Bull

    M. Shulman , Strange new universes: proof assistants and synthetic foundations , Bull. Amer. Math. Soc. (N.S.), 61 (2024), pp. 257--270, https://doi.org/10.1090/bull/1830

    2024 doi

  54. [63]

    N. E. Steenrod , A convenient category of topological spaces , Michigan Math. J., 14 (1967), pp. 133--152, http://projecteuclid.org/euclid.mmj/1028999711

    1967

  55. [64]

    Stenzel , On univalence, Rezk completeness, and presentable quasi-categories , PhD thesis, University of Leeds, 2019

    R. Stenzel , On univalence, Rezk completeness, and presentable quasi-categories , PhD thesis, University of Leeds, 2019

    2019

  56. [65]

    Street , Fibrations in bicategories , Cahiers Topologie G\'eom

    R. Street , Fibrations in bicategories , Cahiers Topologie G\'eom. Diff\'erentielle, 21 (1980), pp. 111--160

    1980

  57. [66]

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

    2013

  58. [67]

    Verdier , Des cat\'egories d\'eriv\'ees des cat\'egories ab\'eliennes , Ast\'erisque, (1996), pp

    J.-L. Verdier , Des cat\'egories d\'eriv\'ees des cat\'egories ab\'eliennes , Ast\'erisque, (1996), pp. xii+253. With a preface by Luc Illusie, Edited and with a note by Georges Maltsiniotis

    1996

  59. [68]

    M. Z. Weaver and D. R. Licata , A constructive model of directed univalence in bicubical sets , in Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '20, New York, NY, USA, 2020, Association for Computing Machinery, p. 915–928, https://doi.or...

    2020

  60. [69]

    Weinberger , Strict stability of extension types , 2022, https://arxiv.org/abs/2203.07194

    J. Weinberger , Strict stability of extension types , 2022, https://arxiv.org/abs/2203.07194

    2022 arXiv

  61. [70]

    Weinberger , Two-sided cartesian fibrations of synthetic ( ,1) -categories , J

    J. Weinberger , Two-sided cartesian fibrations of synthetic ( ,1) -categories , J. Homotopy Relat. Struct., 19 (2024), pp. 297--378, https://doi.org/10.1007/s40062-024-00348-3

    2024 doi

Pith tools

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