Pith. sign in

REVIEW 4 major objections 5 minor 20 references

Internal Algebraic Type Theory

T0 review · 4 major / 5 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 The thesis proves that the category of categories carries an internal dependent type theory—a universe classifying split opfibrations supports Unit, Sigma, Pi, and Hom-types, with Hom-types replacing identity types—and builds the general al

desk verdict A serious thesis that unifies exponentiability and polynomial functors in preclans and sketches an algebraic Cat model; worth refereeing, but the Cat model's Hom-elimination rests on an unproved identification. read the letter →

arxiv 2608.00095 v1 pith:HLHXN2IC submitted 2026-07-30 math.CT cs.PL

Joseph Hua This is my paper · ORCID
classification math.CTcs.PL MSC 03B3818C2018D30
keywords internaltypetheoryalgebraicpreclansR-exponentiablemorphismssplitopfibrationshom-typesdirectedpolynomialfunctors
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 central claim is that the category of categories supports an internal dependent type theory: take split opfibrations over a base category as the types in context, let covariant and contravariant types interact in Pi-types, and replace the identity types of Martin-Löf type theory with Hom-types that have two elimination rules (left and right). Concretely, Theorem 5.4.2 states that there is an algebraic categorical model based in Cat with a universe classifying split opfibrations, admitting Unit-types, Sigma-types, Pi-types, and Hom-types, and dually for split fibrations. The point of the 'algebraic' packaging is that type formers are captured by pullback squares built from polynomial functors, so stability under substitution is automatic and the model is ready to be translated into a proof assistant. A sympathetic reader should care because this is a step toward computer-checked type-theoretic reasoning inside categories such as Cat, groupoids, and cubical sets, and toward a directed type theory in which the type of morphisms between two objects is primitive.

What carries the argument

The load-bearing machinery is a pair of interacting classes of maps in Cat: split opfibrations and split fibrations, which form a preclan pair (a 4-preclan). The general theory of preclans (classes of maps stable under pullback, containing isomorphisms, closed under composition) and R-exponentiability (a Beck–Chevalley condition on all pullbacks, equivalent to the pushforward being a preclan morphism in presheaves) is what lets the thesis do type theory internally, without local cartesian closure. Polynomial functors are then built from R-exponentiable signatures. For Hom-types specifically, the key object is the twisted arrow category TwA of a category A (morphisms of A as objects, with pai

What would settle it

Take A to be the walking arrow (two objects and one non-identity morphism) and explicitly compute the right-twisted arrow category rtw(A) and the AWFS factorisation Kδ of the diagonal map core(A) → core(A) × A. Check whether the comparison map rtw(A) → Kδ is an isomorphism over core(A) × A and whether rfl: core(A) → rtw(A) is a lari with right adjoint given by src. A failure of the isomorphism or of the lari property in this small example would falsify the load-bearing step for Hom elimination in Cat.

Watch

Extended reading notes

Core claim

The central discovery is Theorem 5.4.2: there is an algebraic categorical model (Definition 5.2.12) based in Cat with a universe (5.2.21) classifying split opfibrations, with Unit-types, Sigma-types, Pi-types, and Hom-types (5.2.24, 5.2.27, 5.2.37); dually, the same holds for the universe classifying split fibrations. The model is 'algebraic' in the sense of natural models and algebraic type theory: a single map u• : U• → U, the universal small split opfibration, plays the role of the universe, and each type former is a pullback square expressing a universal construction—the Grothendieck construction for Sigma, a pushforward/sections construction for Pi, and a twisted path object for Hom. Ho

Load-bearing premise

Hom-type elimination in the Cat model depends on the asserted equivalence between the right-twisted arrow construction and the factorisation of the right diagonal given by the algebraic weak factorisation system (Proposition 5.1.24); the thesis states this equivalence with a sketch rather than a full proof, and if it fails, the lari property of rfl—and hence the diagonal filler for Hom elimination—is unsupported.

Editorial extensions

If this is right

  • If the theorem is right, the groupoid model of Martin-Löf type theory becomes a degenerate case (both variances equal, Hom-types collapse to Id-types), and Cat gives the first internal algebraic model with genuinely two-variance types.
  • The model yields an internal language for category theory: contexts are categories, types are split opfibrations, and the Yoneda lemma emerges from Hom-type elimination (Section 5.5), so categorical reasoning can be carried out inside a dependent type theory.
  • The general framework of preclans and R-exponentiable maps covers other settings—topological spaces with open or closed embeddings and étale maps, simplicial sets with Kan fibrations, cubical sets with cubical fibrations—so internal type theory may extend beyond Cat.
  • The algebraic-to-unalgebraic correspondence (Theorem 5.3.3) means the Cat model can be translated into a syntax-oriented, CwF-style model suitable for formalisation in a proof assistant.

Reading between the lines

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

  • A directed type theory with two Hom-eliminators suggests a synthetic account of profunctors and of the two naturality directions of natural transformations; the thesis only gestures at this, but it is a natural next layer to make explicit.
  • The model leaves univalence (or directed univalence) entirely untouched, which the author notes as a challenge; whether the Hom-type classifying universe satisfies any directed analogue of univalence would determine if the syntax is homotopically meaningful or purely categorical.
  • The R-exponentiability framework could plausibly be applied to variance pairs other than opfibration/fibration (for instance, discrete versus codiscrete maps in toposes), yielding new models of directed type theory and new instances of the polynomial machinery.
  • The proof gap in Proposition 5.1.24 (the asserted equivalence rtwX ≅ Kδ) is a concrete place to stress-test the model: formalising that equivalence in a proof assistant would either certify or undermine the Hom-elimination structure.
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 is a PhD thesis presenting an internal, algebraic approach to dependent type theory, with the category of categories as the main model. Chapter 1 introduces preclans and R-exponentiable maps, proving Theorem 1.3.1, an equivalence between a pullback-stable Beck–Chevalley condition and preservation of R-maps by pushforwards in presheaves. Chapter 2 develops polynomial functors in this setting. Chapter 3 reports on the HoTTLean formalisation of the Hofmann–Streicher groupoid model, contrasting unalgebraic and algebraic presentations. Chapter 4 gives a path-type construction of identity types. Chapter 5 proposes algebraic categorical models (ACMs), with two variances (op- and fibrations), Σ- and Π-types, and Hom-types, and in Theorem 5.4.2 claims that the category of categories, with the universe of small split opfibrations, is an ACM with Unit-, Σ-, Π-, and Hom-types. The paper carefully separates general axioms from the Cat model, but the verification of Hom-types relies on a key unproved identification.

Significance. If the missing piece in §5.1 is supplied, the contribution is significant: it gives a systematic, algebraic semantics for directed dependent type theory based on the category of categories, with two variance types and hom-types rather than identity types; it offers a route to formalisation in HoTTLean; and the general preclan/polynomial theory subsumes existing notions of exponentiability and σ-clans. Strengths: Theorem 1.3.1 is proved in the text with explicit Beck–Chevalley formulations; the axioms for ACMs are stated cleanly; external theorems are largely identified. The Cat model is concrete and checkable. The main weakness is that Theorem 5.4.2 is conditional on Proposition 5.1.24, and parts of the general polynomial framework rest on unpublished joint work. I do not see circularity or definitional tautology; the central issue is a missing proof, not a methodological one.

major comments (4)
  1. [§5.1, Proposition 5.1.24] This proposition identifies the right-twisted arrow construction rtwXA with the AWFS factorisation Kδ of δ=(id,inc): coreXA → coreXA ×_X A. The proof consists of asserting that the pointwise equivalence K(id,inc) ≃ rtwX 'extends as a 2-functor' and that 'whiskering provides' the relative version. No explicit 2-natural equivalence is constructed, and no verification is given that the equivalence commutes with rfl and (src,trg) or preserves the AWFS algebra/coalgebra structures. This matters because in Example 5.4.2, Axiom 5.2.36 is verified by invoking Proposition 5.1.24 to make rfl: coreLA → rtwLA a lari map, so that the AWFS supplies the Hom-elimination diagonal filler. I therefore cannot certify Theorem 5.4.2's Hom-types component as written.
  2. [§5.2, Axiom 5.2.36 / Example 5.4.2] Even assuming the underlying equivalence of Proposition 5.1.24, the verification in Example 5.4.2 jumps from 'rfl is lari' to 'the AWFS provides a lift j'. Axiom 5.2.36 requires one of the structures in Proposition 5.2.35, i.e. a chosen diagonal filler or a section of p, stable under pullback. Existence of a lift, or of an arbitrary equivalence with the AWFS factorisation, is not by itself enough; the algebraic structure must be transferred along the equivalence. The short paragraph in Example 5.4.2 does not supply this transfer. This should be filled in or the axiom should be weakened/restated.
  3. [§1.3, Lemmas 1.3.14–1.3.15] The proofs of these lemmas are deferred to [BH26], an unpublished joint preprint. The lemmas are used in Lemma 1.3.16 and then in Chapter 2's polynomial functor theory, and therefore underpin the general statements in Section 5.2. I acknowledge that Theorem 1.3.1's own proof does not use them; however, the polynomial machinery on which the abstract ACM framework relies cannot be fully checked from the present text. Please include self-contained proofs or replace the references by a publicly available version with proofs.
  4. [§5.1, Proposition 5.1.14] The proof that opfibrations and fibrations form the combined exponentiability structure in Cat says that 'one can extend the cited construction to produce a split opfibration (F∗G;l)' after citing [Vid18, Proposition 1.5.1]. Because Axiom 5.2.6 (via Example 5.4.2) and Axiom 5.2.26 (via Theorem 5.2.25) depend on this, the split structure of the pushforward should be given explicitly, or a precise statement in the literature should be quoted.
minor comments (5)
  1. [§3.1, Definition 3.1.5(2)] The stability equation for Π-types appears to be misprinted: 'ΠA◦σ(B ◦ σ̃) = B ◦ σ' should presumably read 'ΠAB ◦ σ = Π_{A◦σ}(B ◦ σ̃)' or similar. As written, the two sides do not have the same type.
  2. [§1.2, Proposition 1.2.5] The proof refers to 'Condition (1)' and 'condition (3)' although the proposition statement does not number conditions; renumber or cross-reference the displayed isomorphism.
  3. [§5.2, Theorem 5.2.25(5)] Part (5) says '(Cat; OU; FV) is a ㅠ-clan'; since OU and FV are preclans rather than clans, this should presumably be the corresponding preclan variant.
  4. [§5.2, Notation] The many universes (u•, u•, u∼, v•, v•, v∼) are easy to confuse; a table or a diagram of their relations would improve readability.
  5. [Title page] There are typographical errors ('T uesday', 'P A') on the title page; also the thesis/paper conventions are mixed. These are cosmetic but should be cleaned up.

Circularity Check

0 steps flagged · score 2.0 of 10

No material circularity: the Cat model is checked against external AWFS and straightening results; the self-citations are dependencies rather than definitional reductions.

full rationale

The paper contains no fitted parameters, no quantity predicted from the same data, and no axiom that is definitional in terms of its own theorem. The central claim (Theorem 5.4.2) is verified in Example 5.4.2 using independently established results: the AWFS on Cat is quoted from [Gar08, 2.13] (Theorem 5.1.5), straightening/unstraightening is proved in Theorem 5.1.8, and the Pi-type exponentiability rests on Conduché fibrations via [Gir64, Vid18] (Proposition 5.1.14). The thesis explicitly says Chapter 5 'is not necessarily to prove something new about the model, but rather to reformulate existing results', so the algebraic categorical model is a repackaging of external content rather than a self-referential derivation. The self-citations that occur—[BH26] for Lemmas 1.3.14 and 1.3.15, [AH26] for path types, and [HAC+25] for HoTTLean—are dependencies: the cited lemmas are standard Beck–Chevalley/adjunction facts, and the path-type proof is reworked in Chapter 4 rather than merely assumed. No quoted equation makes a theorem equal to its own input. The load-bearing Hom-elimination step does rest on Proposition 5.1.24, whose proof asserts that 'whiskering provides' a 2-natural equivalence K ≃ rtw without giving the construction; this is an omitted proof and a correctness risk, not a circular reduction, because rtwXA and Kδ are independently defined categories and the proposition is not used to define Axiom 5.2.36. The 'Challenges and limitations' passage admits the axiomatisation is incomplete, and Remark 5.1.15 identifies places where the theory of exponentiability is inadequate; these are acknowledged gaps, not hidden circularities. Hence the score is 2: minor self-citation and an unproved bridge, but no demonstrated circular derivation.

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

The central claims rest on standard categorical background (presheaf LCC structure, straightening/unstraightening, Garner's AWFS), the paper's own preclan definitions, and several axioms/postulates (5.2.17, 5.2.28-5.2.36) that are checked only for the Cat instance. Some load-bearing lemmas are quoted from unpublished joint work [BH26]. No free parameters or invented entities appear; the framework is definitional.

assumptions (6)
  • domain assumption (C,R) is a preclan: R stable under pullback, contains isomorphisms, closed under composition.
    Definition 1.1.1 is assumed throughout; it is the setting for all R-exponentiability and polynomial-functor theorems.
  • standard math Presheaf categories are locally Cartesian closed and R(X) ~= bR(X) via Yoneda.
    Used in Proposition 1.2.2, Lemma 1.3.9, and the proof of Theorem 1.3.1 to reduce partial right adjoints to pushforwards in bC.
  • ad hoc to paper Lemmas 1.13/1.14 of the unpublished preprint [BH26] (pushforward decompositions in preclans).
    Lemmas 1.3.14 and 1.3.15 defer to this unpublished joint work; these decompositions feed the polynomial functor theory.
  • standard math Garner's AWFS on Cat: the comonad/monad (L,R) whose right maps are split opfibrations and left maps are lari (Theorem 5.1.5).
    Cited to [Gar08, 2.13] and not proved in the thesis; used to obtain Hom-type elimination lifts in Proposition 5.2.35 / Axiom 5.2.36.
  • domain assumption Axiom 5.2.17: every small opfibration has a chosen classifying map.
    Needed to turn pullbacks of the universe into algebraic data; the paper notes this uses the axiom of choice in Cat and leaves a constructive reformulation to future work.
  • ad hoc to paper Twisted/core axioms 5.2.28-5.2.36: core, tw, smallness of (src,trg), pullback L, and section j.
    For general algebraic categorical models these are postulates; for Cat they are verified via Propositions 5.1.21/5.1.24 and Theorem 5.1.5, which is why the Cat instance is the central case.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Internal Algebraic Type Theory." pith.science (2026). https://pith.science/paper/HLHXN2IC

@misc{pith2026260800095,
  author       = {Pith},
  title        = {Pith review of: Internal Algebraic Type Theory},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/HLHXN2IC}},
  note         = {Machine review of arXiv:2608.00095}
}
read the original abstract

This thesis brings us closer to applying computer-assisted, internal, type-theoretic reasoning to a category, with examples in the category of cubical sets, the category of groupoids, and the category of categories. The steps we make towards this general goal are both in furthering the type theoretic analysis of these examples, as well as implementing computer-assisted syntax-semantic reasoning as part of the HoTTLean project. One key component of this work is the consideration of new exponentiability conditions with respect to a class of maps in a category, and the development of polynomial functors for these maps, making the methods of "algebraic type theory" possible in this very general setting.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

20 extracted references · 5 linked inside Pith

  1. [1]

    Path types in algebraic type theory

    [AH26] Steve Awodey and Joseph Hua. Path types in algebraic type theory. arXiv:2601.06567,

    arXiv

  2. [4]

    Théorie des T opos et Cohomologie Etale des Schémas I

    [Bou72] Nicolas Bourbaki. Théorie des T opos et Cohomologie Etale des Schémas I. Séminaire de Géométrie Algébrique du Bois-Marie 1963-1964 (SGA 4): T ome 3 . Springer,

    1963

  3. [7]

    Ho TTLean: Formalizing the Meta-Theory of Ho TT in Lean

    [HAC+25] Joseph Hua, Steve Awodey , Mario Carneiro, Sina Hazratpour, Wojciech Nawrocki, Spencer Woolfson, and Yiming Xu. Ho TTLean: Formalizing the Meta-Theory of Ho TT in Lean. TYPES 2025,

    2025

  4. [9]

    [Hes07] Kathryn Hess

    [Accessed 09-06-2026]. [Hes07] Kathryn Hess. Bundle Theory for Categories. https://ncatlab.org/nlab/ files/HessLackBundCat.pdf,

    2026

  5. [16]

    Fibrations and homotopy colimits of simplicial sheaves

    [Rez98] Charles Rezk. Fibrations and homotopy colimits of simplicial sheaves. arXiv:math/9811038,

    arXiv

  6. [17]

    Synthetic perspectives on spaces and categories

    [Rie25] Emily Riehl. Synthetic perspectives on spaces and categories. arXiv:2510.15795,

    arXiv

  7. [18]

    Directed type theory , with a twist

    [RN26] Fernando Rafael Chu Rivera and Paige Randall North. Directed type theory , with a twist. arXiv:2602.17480,

    arXiv

  8. [19]

    T owards an internalization of the groupoid model of type theory

    [ST14] Matthieu Sozeau and Nicolas Tabareau. T owards an internalization of the groupoid model of type theory. TYPES 2014,

    2014

Show all 20 references
  1. [1972]

    Cu- bical T ype Theory: A Constructive Interpretation of the Univalence Axiom

    [CCHM18] Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cu- bical T ype Theory: A Constructive Interpretation of the Univalence Axiom. In Tarmo Uustalu, editor, 21st International Conference on T ypes for Proofs and Programs (TYPES 2015), volume 69 ofLeibniz I...

    2015

  2. [1982]

    The simplicial model of univalent foundations (after Voevodsky)

    [KL21] Krzysztof Kapulkin and Peter LeFanu Lumsdaine. The simplicial model of univalent foundations (after Voevodsky). Journal of the European Mathemati- cal Society, 23(6):2071–2126,

  3. [1993]

    Notes on Clans and Tribes

    122 [Joy17] Andre Joyal. Notes on Clans and Tribes. arXiv:1710.10238,

    arXiv

  4. [1997]

    [HS98] Martin Hofmann and Thomas Streicher

    www2.mathematik.tu-darmstadt.de/ ~streicher/NOTES/lift.pdf [Accessed 09-06-2026]. [HS98] Martin Hofmann and Thomas Streicher. The groupoid interpretation of type theory. In T wenty-five years of constructive type theory (Venice, 1995), volume 36 of Oxford Logic Guides, pages 83...

    2026

  5. [1998]

    Polynomial functors in -clans for the semantics of type theory

    [HX26] Joseph Hua and Yiming Xu. Polynomial functors in -clans for the semantics of type theory. arXiv:2602.05689,

  6. [2007]

    [HS97] Martin Hofmann and Thomas Streicher

    [Accessed 25-01-2026]. [HS97] Martin Hofmann and Thomas Streicher. Lifting Grothendieck Universes. Unpublished note , 1(1.2):4,

    2026

  7. [2012]

    Fibered categories à la Jean Bénabou

    [Str18] Thomas Streicher. Fibered categories à la Jean Bénabou. arXiv:1801.02927,

    arXiv

  8. [2016]

    Licata, Michael Shulman, and Mitchell Riley

    [LSR17] Daniel R. Licata, Michael Shulman, and Mitchell Riley. A Fibrational Frame- work for Substructural and Modal Logics. In Dale Miller, editor, 2nd Inter- national Conference on Formal Structures for Computation and Deduction (FSCD 2017), volume 84 of Leibniz Internationa...

    2017

  9. [2023]

    The 1-category of 1-categories in simplicial type theory

    [GWB26] Daniel Gratzer, Jonathan Weinberger, and Ulrik Buchholtz. The 1-category of 1-categories in simplicial type theory. arXiv:2602.02218,

  10. [2024]

    Algebraic T ype Theory , Part 1: Martin-Löf algebras

    [Awo25] Steve Awodey. Algebraic T ype Theory , Part 1: Martin-Löf algebras. arXiv:2505.10761,

    arXiv

  11. [2025]

    Ho TTLean: Formalizing the groupoid model of MLTT

    [HAC+26] Joseph Hua, Steve Awodey , Mario Carneiro, Sina Hazratpour, Wojciech Nawrocki, Spencer Woolfson, and Yiming Xu. Ho TTLean: Formalizing the groupoid model of MLTT. Workshop on Homotopy T ype Theory / Univalent Foundations 2026,

    2026

  12. [2026]

    Synthetic 1-categories in directed type theory

    [AN24] Thorsten Altenkirch and Jacob Neumann. Synthetic 1-categories in directed type theory. arXiv:2410.19520,

Pith tools

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