Table of Contents: :: Library Catalog

Cover Image

Saved in:

Bibliographic Details
Main Authors:	Coquand, Thierry, Höfer, Jonas, Sattler, Christian
Format:	Preprint
Published:	2026
Subjects:	Logic in Computer Science Logic
Online Access:	https://arxiv.org/abs/2605.15126
Tags:	Add Tag No Tags, Be the first to tag this record!

Table of Contents:

There have recently been several developments in synthetic mathematics using extensions of dependent type theory with univalence and higher inductive types: simplicial homotopy type theory, synthetic algebraic geometry and synthetic Stone duality. 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.