Pith. sign in

REVIEW 3 cited by

Notes on Clans and Tribes

Not yet reviewed by Pith; the record is open.

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

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 1710.10238 v1 pith:A3QSQIO6 submitted 2017-10-27 math.CT math.ATmath.LO

Andre Joyal This is my paper · ORCID
classification math.CTmath.ATmath.LO
keywords notestribesalwaysanalysisbettercategoricalchapterclans
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
read the original abstract

The purpose of these notes is to give a categorical presentation/analysis of homotopy type theory. The notes are incomplete as they stand (October 2017). The chapter on univalent tribes is missing. The references are not always connected to the text. A better version is in preparation.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 3 Pith papers

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.

  2. Elementary $\infty$-toposes from type theory

    math.CT 2025-12 unverdicted novelty 7.0 of 10

    Categorical models of univalent type theory localise to elementary ∞-toposes, and such ∞-toposes automatically have small subobject classifiers.

  3. A Model of Type Theory in Groupoid Assemblies

    math.CT 2025-07 conditional novelty 7.0 of 10

    Groupoids internal to assemblies on a partial combinatory algebra form a pi-tribe, hence a model of dependent type theory, with a model structure, W-types, a univalent impredicative universe, and 0-type homotopy categ...

Pith tools