pith. sign in

arxiv: 1906.09435 · v1 · pith:OC6FT2U6new · submitted 2019-06-22 · 🧮 math.LO

Classifying Types

Egbert Rijke This is my paper

Pith reviewed 2026-05-25 17:58 UTC · model grok-4.3

classification 🧮 math.LO
keywords synthetic homotopy theoryhomotopy type theoryunivalencehigher inductive typestype theory
0
0 comments X

The pith

Homotopy theory can be developed synthetically inside the language of homotopy type theory.

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

The thesis develops synthetic homotopy theory within homotopy type theory. It shows how phenomena from homotopy can be expressed and reasoned about using the internal primitives of paths, higher paths, and univalence. This is done without first passing through set-theoretic or categorical models. A sympathetic reader would care because the approach yields a computational and univalent foundation in which many classical homotopy results become provable directly as type-theoretic statements.

Core claim

Homotopy-theoretic phenomena can be faithfully captured and developed synthetically inside the language of homotopy type theory without requiring external set-theoretic or categorical semantics for the core results.

What carries the argument

The internal language of homotopy type theory, used to formalize spaces, paths, and homotopies directly.

If this is right

  • Classical homotopy results become provable as internal type-theoretic statements.
  • Formalized libraries of mathematics can incorporate homotopy constructions synthetically.
  • Questions in type theory can be motivated directly by homotopy-theoretic considerations.
  • Computational semantics of type theory can be used to extract programs from homotopy proofs.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same synthetic style might extend to other areas such as algebraic geometry or higher category theory.
  • Proof assistants based on homotopy type theory could verify topological theorems without separate model-checking steps.
  • Discrepancies between synthetic and classical results would highlight which homotopy facts depend on set-theoretic choice principles.

Load-bearing premise

Homotopy-theoretic phenomena can be faithfully captured and developed inside homotopy type theory without external semantics.

What would settle it

A standard result from classical homotopy theory that cannot be stated or proved using only the rules and axioms of homotopy type theory.

read the original abstract

The study of homotopy theoretic phenomena in the language of type theory is sometimes loosely called `synthetic homotopy theory'. Homotopy theory in type theory is only one of the many aspects of homotopy type theory, which also includes the study of the set theoretic semantics (models of homotopy type theory and univalence in a meta-theory of sets or categories), type theoretic semantics (internal models of homotopy type theory), and computational semantics, as well as the study of various questions in the internal language of homotopy type theory which are not necessarily motivated by homotopy theory, or questions related to the development of formalized libraries of mathematics based on homotopy type theory. This thesis concerns the development of synthetic homotopy theory.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 0 minor

Summary. The manuscript is a PhD thesis abstract stating that it concerns the development of synthetic homotopy theory inside homotopy type theory. It distinguishes this from set-theoretic semantics (models in sets or categories), type-theoretic semantics (internal models), computational semantics, and other internal questions not motivated by homotopy theory or library development.

Significance. Synthetic homotopy theory is an active research direction in homotopy type theory. A thesis that advances it could be significant if it contains new constructions, theorems, or libraries, but the provided abstract contains no specific results, lemmas, or derivations with which to evaluate any contribution.

major comments (1)
  1. No technical content, derivations, or theorems are visible in the abstract. It is therefore impossible to assess whether any central claim is supported by mathematics or whether the work is internally consistent.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for reviewing the abstract of our PhD thesis on synthetic homotopy theory in homotopy type theory. The submission is an abstract summarizing the thesis scope, and we address the major comment below.

read point-by-point responses

  1. Referee: No technical content, derivations, or theorems are visible in the abstract. It is therefore impossible to assess whether any central claim is supported by mathematics or whether the work is internally consistent.

    Authors: The submitted text is the abstract of the thesis, whose purpose is to outline the research focus on synthetic homotopy theory and classifying types rather than to present derivations. The full thesis develops specific new constructions, theorems, and internal results in homotopy type theory that support the claims and ensure consistency. If the complete thesis manuscript is needed for evaluation, it can be provided. revision: no

Circularity Check

0 steps flagged

No significant circularity

full rationale

The provided abstract and thesis description frame the work as the development of synthetic homotopy theory inside homotopy type theory, distinguishing it from semantic and computational aspects without advancing any concrete theorem, equation, or prediction whose validity is shown to reduce to its own inputs by construction. No self-definitional steps, fitted parameters renamed as predictions, or load-bearing self-citations are identifiable in the text, so the central claim remains a statement of research scope rather than a derivation chain that collapses into its premises.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract only; no specific free parameters, axioms, or invented entities can be extracted from the provided text.

pith-pipeline@v0.9.0 · 5622 in / 1041 out tokens · 26578 ms · 2026-05-25T17:58:15.964670+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 2 Pith papers

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

  1. Delooping presented groups in homotopy type theory

    cs.LO 2024-05 unverdicted novelty 7.0

    Simpler delooping constructions for presented groups in HoTT using 2-polygraphs, Cayley graphs, and complexes, formalized in cubical Agda.

  2. Decalf: A Directed, Effectful Cost-Aware Logical Framework

    cs.PL 2023-07 unverdicted novelty 7.0

    Decalf equips types with an intrinsic preorder so that cost bounds for effectful programs become ordinary programs, extending Calf to probabilistic choice and other effects, with a model in augmented simplicial sets.

Reference graph

Works this paper leans on

39 extracted references · 39 canonical work pages · cited by 2 Pith papers · 5 internal anchors

  1. [1]

    A Gener alized Blakers-Massey Theorem

    M. Anel, G. Biedermann, E. Finster, and A. Joyal. “A Gener alized Blakers-Massey Theorem”. In: ArXiv e-prints (Mar. 2017). arXiv: 1703.09050 [math.AT]

    work page arXiv 2017

  2. [2]

    Computational Higher Type Theory I: Abstract Cubical Realizability

    C. Angiuli, R. Harper, and T. Wilson. “Computational Hig her Type Theory I: Ab- stract Cubical Realizability”. In: ArXiv e-prints (Apr. 2016). arXiv: 1604.08873 [cs.LO]

    work page internal anchor Pith review Pith/arXiv arXiv 2016

  3. [3]

    Natural models of homotopy type theory

    S. Awodey. “Natural models of homotopy type theory”. In: ArXiv e-prints (June 2014). arXiv: 1406.3219 [math.CT]

    work page internal anchor Pith review Pith/arXiv arXiv 2014

  4. [4]

    Type theory and homotopy

    Steve Awodey. “Type theory and homotopy”. In: Epistemology versus ontology . Vol. 27. Log. Epistemol. Unity Sci. Springer, Dordrecht, 20 12, pp. 183–201. doi: 10.1007/978-94-007-4435-6_9 . url: http://dx.doi.org/10.1007/978-94-007-4435-6_9

    work page doi:10.1007/978-94-007-4435-6_9

  5. [5]

    Homotopy theoretic models of identity types

    Steve Awodey and Michael A. Warren. “Homotopy theoretic models of identity types”. In: Math. Proc. Cambridge Philos. Soc. 146.1 (2009), pp. 45–55. issn: 0305-

    work page 2009

  6. [6]

    url: http://dx.doi.org/10.1017/S0305004108001783

    doi: 10.1017/S0305004108001783. url: http://dx.doi.org/10.1017/S0305004108001783

    work page doi:10.1017/s0305004108001783

  7. [7]

    The HoTT Library: A Formalizatio n of Homotopy Type Theory in Coq

    Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Mich ael Shulman, Matthieu Sozeau, and Bas Spitters. “The HoTT Library: A Formalizatio n of Homotopy Type Theory in Coq”. In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs. CPP 2017. Paris, France: ACM, 2017, pp. 164–172. isbn: 978- 1-4503-4705-1. doi: 10.1145/3018610.30186...

    work page doi:10.1145/3018610.3018615 2017

  8. [8]

    A model of type theory in cubical sets

    Marc Bezem, Thierry Coquand, and Simon Huber. “A model of type theory in cubical sets”. In: 19th International Conference on Types for Proofs and Programs . Vol. 26. LIPIcs. Leibniz Int. Proc. Inform. Schloss Dagstuh l. Leibniz-Zent. Inform., Wadern, 2014, pp. 107–128

    work page 2014

  9. [10]

    On the homotopy groups of spheres in homotopy type theory

    Guillaume Brunerie. “On the homotopy groups of spheres i n homotopy type the- ory”. In: ArXiv e-prints (June 2016). arXiv: 1606.05916 [math.AT]

    work page internal anchor Pith review Pith/arXiv arXiv 2016

  10. [11]

    Implications of large- cardinal principles in homotopical localization

    Carles Casacuberta, Dirk Scevenels, and Jeffrey H. Smith . “Implications of large- cardinal principles in homotopical localization”. In: Adv. Math. 197.1 (2005), pp. 120–

    work page 2005

  11. [12]

    Reflective subc ategories, localizations and factorization systems

    C. Cassidy, M. H´ ebert, and G. M. Kelly. “Reflective subc ategories, localizations and factorization systems”. In: J. Austral. Math. Soc. Ser. A 38.3 (1985), pp. 287–

    work page 1985

  12. [13]

    L ocalization in Homotopy Type Theory

    J. D. Christensen, M. Opie, E. Rijke, and L. Scoccola. “L ocalization in Homotopy Type Theory”. In: ArXiv e-prints (July 2018). arXiv: 1807.04155 [math.AT] . 163 164 BIBLIOGRAPHY

    work page arXiv 2018

  13. [14]

    The Coq Proof Assistant Reference Manual

    Coq Development Team. The Coq Proof Assistant Reference Manual. INRIA-Rocquencourt, 2012

    work page 2012

  14. [15]

    Identity types of sequential colimits

    F. van Doorn, E. Rijke, and K. Sojakova. “Identity types of sequential colimits”. In preparation. 2018. url: https://github.com/cmu-phil/Spectral/blob/master/co limit/seq_colim.hlean

    work page 2018

  15. [16]

    Constructing the Propositional Truncation using Non-recursive HITs

    Floris van Doorn. “Constructing the propositional tru ncation using non-recursive HITs”. In: Proceedings of the 5th ACM SIGPLAN Conference on Certified Pro- grams and Proofs . ACM. 2016, pp. 122–129. arXiv: 1512.02274

    work page internal anchor Pith review Pith/arXiv arXiv 2016

  16. [17]

    Homotopy Type The- ory in Lean

    Floris van Doorn, Jakob von Raumer, and Ulrik Buchholtz . “Homotopy Type The- ory in Lean”. In: Interactive Theorem Proving (ITP 2017) . Cham: Springer, 2017, pp. 479–495. isbn: 978-3-319-66107-0. doi: 10.1007/978-3-319-66107-0_30

    work page doi:10.1007/978-3-319-66107-0_30 2017

  17. [18]

    Mart ´ ın Escard´ o. “N/A”. 2017.url: https://www.cs.bham.ac.uk/~mhe/agda-new/UF-IdEmbedding.html

    work page 2017

  18. [19]

    Cellular spaces, null spaces and homotopy localization

    Emmanuel Dror Farjoun. Cellular spaces, null spaces and homotopy localization . Vol. 1622. Lecture Notes in Mathematics. Springer-Verlag, Berlin, 1996, pp. xiv+199. isbn: 3-540-60604-1. doi: 10.1007/BFb0094429. url: https://doi.org/10.1007/BFb0094429

    work page doi:10.1007/bfb0094429 1996

  19. [20]

    The Simplicial Mo del of Univalent Foun- dations (after Voevodsky)

    C. Kapulkin and P. LeFanu Lumsdaine. “The Simplicial Mo del of Univalent Foun- dations (after Voevodsky)”. In: ArXiv e-prints (Nov. 2012). arXiv: 1211.2851 [math.LO]

    work page arXiv 2012

  20. [21]

    Constructions with Non-Recursive Hig her Inductive Types

    Nicolai Kraus. “Constructions with Non-Recursive Hig her Inductive Types”. In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Co mputer Sci- ence. LICS ’16. New York, NY, USA: ACM, 2016, pp. 595–604. doi: 10.1145/2933575.2933586

    work page doi:10.1145/2933575.2933586 2016

  21. [22]

    Higher inductive types: a tour of the menagerie

    Peter Lefanu Lumsdaine. Higher inductive types: a tour of the menagerie . 2011. url: https://homotopytypetheory.org/2011/04/24/higher-in ductive-types-a-tour-of-the-menagerie/

    work page 2011

  22. [23]

    Reducing all HIT’s to 1-HIT’s

    Peter Lefanu Lumsdaine. Reducing all HIT’s to 1-HIT’s . 2012. url: https://homotopytypetheory.org/2012/05/07/reducing- all-hits-to-1-hits/

    work page 2012

  23. [24]

    Eilenberg-MacLane spaces in homotopy type theory

    Daniel R. Licata and Eric Finster. “Eilenberg-MacLane spaces in homotopy type theory”. In: Proceedings of the Joint Meeting of the Twenty-Third EACSL An- nual Conference on Computer Science Logic (CSL) and the Twenty-Nin th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) . ACM, New York, 2014, Article No. 66, 10

    work page 2014

  24. [25]

    Calculating the fundamental group of the circle in homotopy type theory

    Daniel R. Licata and Michael Shulman. “Calculating the fundamental group of the circle in homotopy type theory”. In: 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2013) . IEEE Computer Soc., Los Alamitos, CA, 2013, pp. 223–232

    work page 2013

  25. [26]

    Intuitionistic type theory

    Per Martin-L¨ of. Intuitionistic type theory . Vol. 1. Studies in Proof Theory. Lecture Notes. Notes by Giovanni Sambin. Bibliopolis, Naples, 1984 , pp. iv+91. isbn: 88- 7088-105-9

    work page 1984

  26. [27]

    U. Norell. Towards a practical programming language based on dependen t type the- ory. Chalmers University of Technology, 2007

    work page 2007

  27. [28]

    The join construction

    E. Rijke. “The join construction”. In: ArXiv e-prints (Jan. 2017). arXiv: 1701.07538 [math.CT]

    work page internal anchor Pith review Pith/arXiv arXiv 2017

  28. [29]

    Modalities in ho motopy type theory

    E. Rijke, M. Shulman, and B. Spitters. “Modalities in ho motopy type theory”. In: ArXiv e-prints (June 2017). arXiv: 1706.07526 [math.CT]

    work page arXiv 2017

  29. [30]

    Sets in homotopy type th eory

    Egbert Rijke and Bas Spitters. “Sets in homotopy type th eory”. In: Math. Struc- tures Comput. Sci. 25.5 (2015), pp. 1172–1202. issn: 0960-1295. doi: 10.1017/S0960129514000553. url: http://dx.doi.org/10.1017/S0960129514000553. BIBLIOGRAPHY 165

    work page doi:10.1017/s0960129514000553 2015

  30. [31]

    Brouwer’s fixed-point theorem in rea l-cohesive homotopy type theory

    Michael Shulman. “Brouwer’s fixed-point theorem in rea l-cohesive homotopy type theory”. In: Math. Structures Comput. Sci. 28.6 (2018), pp. 856–941. issn: 0960-

    work page 2018

  31. [32]

    url: https://doi.org/10.1017/S0960129517000147

    doi: 10.1017/S0960129517000147. url: https://doi.org/10.1017/S0960129517000147

    work page doi:10.1017/s0960129517000147

  32. [33]

    Homotopy Type Theory, VI

    Michael Shulman. Homotopy Type Theory, VI. https://golem.ph.utexas.edu/category/2011/04/homotopy_type_theory_vi.html. 2011

    work page 2011

  33. [34]

    The univalence axiom for elegant Ree dy presheaves

    Michael Shulman. “The univalence axiom for elegant Ree dy presheaves”. In: Ho- mology Homotopy Appl. 17.2 (2015), pp. 81–106. issn: 1532-0073. doi: 10.4310/HHA.2015.v17.n2.a6. url: http://dx.doi.org/10.4310/HHA.2015.v17.n2.a6

    work page doi:10.4310/hha.2015.v17.n2.a6 2015

  34. [35]

    Homotopy Type Theory: Univalent Founda- tions of Mathematics

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

    work page 2013

  35. [36]

    Homotopy Type Theory: Univalent Founda- tions of Mathematics

    The Univalent Foundations Program. Homotopy Type Theory: Univalent Founda- tions of Mathematics . first. http://homotopytypetheory.org/book/, 2013

    work page 2013

  36. [37]

    A C-system defined by a universe ca tegory

    Vladimir Voevodsky. “A C-system defined by a universe ca tegory”. In: Theory Appl. Categ. 30 (2015), No. 37, 1181–1215. issn: 1201-561X

    work page 2015

  37. [38]

    A very short note on homotopy λ-calculus

    Vladimir Voevodsky. “A very short note on homotopy λ-calculus”. 2006. url: http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/Hlambda_short_current.pdf

    work page 2006

  38. [39]

    Univalent Foundations Project

    Vladimir Voevodsky. “Univalent Foundations Project” . 2010. url: http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/univalent_foundations_project.pdf

    work page 2010

  39. [40]

    Cartan Geometry in Modal Homotopy Type Theo ry

    F. Wellen. “Cartan Geometry in Modal Homotopy Type Theo ry”. In: ArXiv e- prints (June 2018). arXiv: 1806.05966 [math.DG]

    work page arXiv 2018