pith. sign in

arxiv: 2512.18891 · v2 · submitted 2025-12-21 · 🧮 math.CT · math.AT· math.LO

Elementary infty-toposes from type theory

Maximilian Petrowitsch This is my paper

Pith reviewed 2026-05-16 20:44 UTC · model grok-4.3

classification 🧮 math.CT math.ATmath.LO
keywords elementary ∞-toposdependent type theoryunivalent universes∞-localizationunivalent tribeunivalent fibrationlocally cartesian closedsubobject classifier
0
0 comments X

The pith

Every categorical model of dependent type theory with univalent universes becomes an elementary ∞-topos after ∞-localization.

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

The paper proves that any categorical model of dependent type theory that includes dependent sums and products, intensional identity types, and univalent universes yields an elementary ∞-topos when its ∞-localization is taken. An elementary ∞-topos is defined as a finitely complete, locally cartesian closed ∞-category that contains enough univalent universal morphisms. The argument rests on new notions of univalent tribes and univalent fibrations, which extend Joyal's tribes so that the localization functor preserves the necessary structure. It is also shown that every elementary ∞-topos admits small subobject classifiers. This establishes a direct passage from ordinary models of type theory to the higher-categorical setting.

Core claim

We prove that every categorical model of dependent type theory with dependent sums and products, intensional identity types and univalent universes presents via its ∞-localisation an elementary ∞-topos, that is, a finitely complete, locally cartesian closed ∞-category with enough univalent universal morphisms. We also show that elementary ∞-toposes have small subobject classifiers. To achieve this, we extend Joyal's theory of tribes by introducing the notion of a univalent tribe and a univalent fibration in a tribe.

What carries the argument

A univalent tribe: a tribe equipped with univalent fibrations whose ∞-localization functor preserves finite completeness, local cartesian closure, and enough univalent universal morphisms to produce an elementary ∞-topos.

If this is right

  • Categorical models of dependent type theory with the listed structure supply examples of elementary ∞-toposes.
  • Every elementary ∞-topos possesses small subobject classifiers.
  • Univalent fibrations in the tribe correspond directly to the univalent universal morphisms required in the resulting ∞-topos.
  • The localization construction transfers finite limits and dependent products from the type-theoretic model to the ∞-categorical level.

Where Pith is reading between the lines

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

  • Syntactic presentations of type theories could be used to generate new concrete examples of elementary ∞-toposes without separate higher-categorical construction.
  • Results proved in homotopy type theory for models with univalent universes might transfer to statements about elementary ∞-toposes via this correspondence.
  • The same localization technique could be tested on type theories that include higher inductive types to produce further classes of ∞-toposes.

Load-bearing premise

The ∞-localization functor applied to a univalent tribe preserves finite completeness, local cartesian closure, and the existence of enough univalent universal morphisms.

What would settle it

A specific categorical model of the given type theory whose ∞-localization is not locally cartesian closed or lacks enough univalent universal morphisms would refute the central theorem.

read the original abstract

We prove that every categorical model of dependent type theory with dependent sums and products, intensional identity types and univalent universes presents via its $\infty$-localisation an elementary $\infty$-topos, that is, a finitely complete, locally cartesian closed $\infty$-category with enough univalent universal morphisms. We also show that elementary $\infty$-toposes have small subobject classifiers. To achieve this, we extend Joyal's theory of tribes by introducing the notion of a univalent tribe and a univalent fibration in a tribe.

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

2 major / 3 minor

Summary. The manuscript proves that every categorical model of dependent type theory equipped with dependent sums and products, intensional identity types, and univalent universes yields an elementary ∞-topos upon ∞-localization. An elementary ∞-topos is defined as a finitely complete, locally cartesian closed ∞-category with enough univalent universal morphisms. The argument extends Joyal's tribes by introducing univalent tribes and univalent fibrations, and additionally shows that elementary ∞-toposes admit small subobject classifiers.

Significance. If the central claims hold, the work provides a direct construction of elementary ∞-toposes from standard type-theoretic models, extending Joyal's framework in a way that preserves finite limits, local cartesian closure, and univalent morphisms under localization. This supplies a concrete bridge between homotopy type theory and higher topos theory, with potential applications to the study of univalent universes and subobject classifiers in ∞-categorical settings. The introduction of univalent tribes and fibrations, together with the localization lemmas, constitutes a technical contribution that could enable new examples and comparisons with existing models.

major comments (2)
  1. [§3.4] §3.4, Lemma on preservation of pullbacks: the argument that ∞-localization commutes with the relevant pullbacks for univalent fibrations is load-bearing for local cartesian closure, but the interaction between the univalence condition and the localization functor is only sketched; an explicit verification that the localized fibration remains univalent would strengthen the step.
  2. [Theorem 4.12] Theorem 4.12: the claim that the localized structure has enough univalent universal morphisms depends on the new definition of univalent fibration; while the lemmas establish preservation, the manuscript does not include a check against a concrete model (such as the tribe of simplicial sets) to confirm the 'enough' quantifier survives localization.
minor comments (3)
  1. [§2] The notation for the ∞-localization functor is introduced without a dedicated preliminary subsection; a short paragraph recalling its universal property would improve readability for readers unfamiliar with Joyal's tribes.
  2. [Figure 1] Figure 1 (the diagram illustrating a univalent fibration) uses arrows whose direction is not labeled consistently with the surrounding text; clarifying the direction of the universal morphism would avoid ambiguity.
  3. [References] The reference list omits the original Joyal paper on tribes; adding the citation would help situate the new definitions.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their positive assessment and constructive comments on the manuscript. We address each major comment below.

read point-by-point responses

  1. Referee: [§3.4] §3.4, Lemma on preservation of pullbacks: the argument that ∞-localization commutes with the relevant pullbacks for univalent fibrations is load-bearing for local cartesian closure, but the interaction between the univalence condition and the localization functor is only sketched; an explicit verification that the localized fibration remains univalent would strengthen the step.

    Authors: We agree that an explicit verification would strengthen the presentation. In the revised manuscript we will expand the proof of the relevant lemma in §3.4 to include a direct check that the localized fibration satisfies the univalence condition, by verifying the relevant homotopy pullback squares and the preservation of the univalence data under the localization functor. revision: yes

  2. Referee: [Theorem 4.12] Theorem 4.12: the claim that the localized structure has enough univalent universal morphisms depends on the new definition of univalent fibration; while the lemmas establish preservation, the manuscript does not include a check against a concrete model (such as the tribe of simplicial sets) to confirm the 'enough' quantifier survives localization.

    Authors: The proof of Theorem 4.12 proceeds from the general definition of univalent tribes and the preservation results already established; the 'enough' quantifier is inherited directly from the type-theoretic model via the localization construction. While an explicit verification in the simplicial-sets tribe is not required for the correctness of the general argument, we will add a short illustrative remark in the revised version showing how the result specializes to that model. revision: partial

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper extends Joyal's existing theory of tribes by defining univalent tribes and univalent fibrations, then proves via lemmas (including in §3.4 and Theorem 4.12) that ∞-localization preserves finite completeness, local cartesian closure, and enough univalent universal morphisms. The central claim does not reduce to any self-definitional equation, fitted parameter renamed as prediction, or load-bearing self-citation chain; all steps rely on independent verification of the new notions interacting with localization. The manuscript is self-contained against external benchmarks from type theory and ∞-category theory.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 2 invented entities

The central claim rests on standard assumptions from dependent type theory and Joyal's tribe theory plus two newly introduced concepts whose independent evidence is limited to the paper itself.

axioms (2)
  • domain assumption Categorical models of dependent type theory include dependent sums, products, intensional identity types, and univalent universes.
    This is the class of models to which the theorem applies.
  • standard math Joyal's theory of tribes provides a framework for modeling type theory categorically.
    The paper extends this existing framework.
invented entities (2)
  • univalent tribe no independent evidence
    purpose: An extension of Joyal's tribes that incorporates univalent universes.
    New notion introduced to enable the localization proof.
  • univalent fibration no independent evidence
    purpose: A fibration inside a tribe that respects univalence.
    New notion introduced to handle univalent structures within the tribe framework.

pith-pipeline@v0.9.0 · 5374 in / 1642 out tokens · 30201 ms · 2026-05-16T20:44:54.460336+00:00 · methodology

discussion (0)

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

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

7 extracted references · 7 canonical work pages · 2 internal anchors

  1. [1]

    Abstract Homotopy Theory and Generalized Sheaf Cohomology

    [Bro73] Ken Brown. “Abstract Homotopy Theory and Generalized Sheaf Cohomology”. In: Trans- actions of the American Mathematical Society 186 (1973), pp. 419–458. [Car86] John Cartmell. “Generalised algebraic theories and contextual categories”. In:Annals of Pure and Applied Logic32 (1986), pp. 209–243. 35 [Cis19] Denis-Charles Cisinski.Higher Categories an...

    work page 1973

  2. [2]

    Univalence in locally cartesian closed infinity-categories

    [FR22] Jonas Frey and Nima Rasekh.Constructing Coproducts in locally Cartesian closed infinity- Categories. 2022.url:http://arxiv.org/abs/2108.11304. [GK17] David Gepner and Joachim Kock. “Univalence in locally cartesian closed infinity-categories”. In:Forum Mathematicum29.3 (2017). [Joh02] Peter Johnstone.Sketches of an elephant: a topos theory compendiu...

    work page arXiv 2022

  3. [3]

    Notes on Clans and Tribes

    [Joy11] Andre Joyal. “Remarks on homotopical logic”. In:Mini-Workshop: The Homotopy Interpre- tation of Constructive Type Theory8.1 (2011), pp. 609–638. [Joy17] Andre Joyal.Notes on Clans and Tribes. 2017.url:http://arxiv.org/abs/1710.10238. [Kap17] Krzysztof Kapulkin. “Locally cartesian closed quasi-categories from type theory”. In: Journal of Topology10...

    work page internal anchor Pith review Pith/arXiv arXiv 2011

  4. [4]

    In:Selecta Mathematica25.2 (2019), p

    -categories”. In:Selecta Mathematica25.2 (2019), p

    work page 2019

  5. [5]

    2022.url:http://arxiv

    [NU22] Hoang Kim Nguyen and Taichi Uemura.infinity-type theories. 2022.url:http://arxiv. org/abs/2205.00798. [Ras21] Nima Rasekh.Univalence in Higher Category Theory. 2021.url:http://arxiv.org/abs/ 2103.12762. [Ras22a] Nima Rasekh.A Theory of Elementary Higher Toposes. 2022.url:http://arxiv.org/abs/ 1805.03805. [Ras22b] Nima Rasekh.Elementary infinity-Top...

    work page arXiv 2022

  6. [6]

    Univalence for inverse diagrams and homotopy canonicity

    [Rij22] Egbert Rijke.Introduction to Homotopy Type Theory. 2022.url:http://arxiv.org/abs/ 2212.11082. [Shu15] Michael Shulman. “Univalence for inverse diagrams and homotopy canonicity”. In:Math- ematical Structures in Computer Science25.5 (2015), pp. 1203–1277. [Shu18] Michael Shulman.Towards elementary infinity-toposes. Vladimir Voevodsky Memorial Con- f...

    work page arXiv 2022

  7. [7]

    All $(\infty,1)$-toposes have strict univalent universes

    [Shu19] Michael Shulman.All (infinity,1)-toposes have strict univalent universes. 2019.url:http : //arxiv.org/abs/1904.07004. [Str91] Thomas Streicher.Semantics of Type Theory. Boston, MA: Birkh ¨auser Boston,

    work page internal anchor Pith review Pith/arXiv arXiv 2019