Pith Number

pith:4D77BGG2

pith:2026:4D77BGG26C5FDEOJTXBEOQZWQB

not attested not anchored not stored refs resolved

Constructive higher sheaf models with applications to synthetic mathematics

Christian Sattler, Jonas H\"ofer, Thierry Coquand

Higher sheaf models of type theory with univalence and higher inductive types can be built in a constructive metatheory.

arxiv:2605.15126 v1 · 2026-05-14 · cs.LO · math.LO

Open paper page JSON Open Graph Bundle Merged state What is a Pith Number?

Add to your LaTeX paper

\usepackage{pith}
\pithnumber{4D77BGG26C5FDEOJTXBEOQZWQB}

Prints a linked badge after your title and injects PDF metadata. Compiles on arXiv. Learn more

Record completeness

1 Bitcoin timestamp

2 Internet Archive

3 Author claim open · sign in to claim

4 Citations open

5 Replications open

✓ Portable graph bundle live · download bundle · merged state

The bundle contains the canonical record plus signed events. A mirror can host it anywhere and recompute the same current state with the deterministic merge algorithm.

Claims

C1strongest claim

We provide a foundation of higher sheaf models of type theory in a constructive metatheory and, in particular, build constructive models of these formal systems.

C2weakest assumption

That higher sheaf models can be constructed constructively for type theories extended with univalence and higher inductive types without requiring additional non-constructive assumptions in the metatheory.

C3one line summary

Constructive higher sheaf models of type theory with univalence and higher inductive types are constructed to underpin synthetic mathematics.

References

41 extracted · 41 resolved · 4 Pith anchors

[1] On Relating Type Theories and Set Theories 1998

[2] Two-level type theory and applications 2023 · doi:10.1017/s0960129523000130

[3] M. Artin, A. Grothendieck, and J. L. Verdier. Th \'e orie de Topos et Cohomologie Etale des Sch \'e mas. Tome 1: Th\'eorie des topos, S\'eminaire de G\'eom\'etrie Alg\'ebrique du Bois-Marie 1963--1964 1963

[4] https://doi.org/10.1017/s0960129516000268 2018 · doi:10.1017/s0960129516000268

[5] Non-Constructivity in Kan Simplicial Sets 2015 · doi:10.4230/lipics.tlca.2015.92

Formal links

2 machine-checked theorem links

Receipt and verification

First computed	2026-05-17T21:40:25.660571Z
Last reissued	2026-05-17T21:57:18.984308Z
Builder	pith-number-builder-2026-05-17-v1
Signature	unsigned_v0
Schema	pith-number/v1.0

Canonical hash

e0fff098daf0ba5191c99dc2474336804cf0cee0ada17715fe834eb89415d670

Aliases

arxiv: 2605.15126 · arxiv_version: 2605.15126v1 · pith_short_12: 4D77BGG26C5F · pith_short_16: 4D77BGG26C5FDEOJ · pith_short_8: 4D77BGG2

Agent API

Resolver JSON Graph JSON Events JSON Schema Signing key

Verify this Pith Number yourself

curl -sH 'Accept: application/ld+json' https://pith.science/pith/4D77BGG26C5FDEOJTXBEOQZWQB \
  | jq -c '.canonical_record' \
  | python3 -c "import sys,json,hashlib; b=json.dumps(json.loads(sys.stdin.read()), sort_keys=True, separators=(',',':'), ensure_ascii=False).encode(); print(hashlib.sha256(b).hexdigest())"
# expect: e0fff098daf0ba5191c99dc2474336804cf0cee0ada17715fe834eb89415d670

Canonical record JSON

{
  "metadata": {
    "abstract_canon_sha256": "e45b8bdc03e3b1ab5e0546b20e85e7e3763a2eb55b928c572cf1a0d752b08589",
    "cross_cats_sorted": [
      "math.LO"
    ],
    "license": "http://arxiv.org/licenses/nonexclusive-distrib/1.0/",
    "primary_cat": "cs.LO",
    "submitted_at": "2026-05-14T17:37:19Z",
    "title_canon_sha256": "22a254bfdf9c0d64ac51e0f87318454465b9c9c739b444aaa85812cde61abe5f"
  },
  "schema_version": "1.0",
  "source": {
    "id": "2605.15126",
    "kind": "arxiv",
    "version": 1
  }
}