Constructive sheaf models of type theory

DOI10.1017/S0960129521000359MaRDI QIDQ5084309zbMATH OpenOpenAlexFDO

Authors Thierry Coquand, Fabian Ruch, Christian Sattler

Publication date 24 June 2022

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/1912.10407

zbMATH Keywords

constructive models of univalencedependent type theoryhomotopy type theoryleft-exact modalitiessheaf models

Mathematics Subject Classification ID

Type theory (03B38)

Recommendations

• scientific article; zbMATH DE number 2247251
• The simplicial model of univalent foundations (after Voevodsky)
• Modalities in homotopy type theory
• Towards a constructive simplicial model of Univalent Foundations
• Aspects of predicative algebraic set theory. III: Sheaves

Cites work

• A Constructive Model of Directed Univalence in Bicubical Sets
• An experimental library of formalized mathematics based on the univalent foundations
• Axioms for modelling cubical type theory in a topos
• Brouwer's fixed-point theorem in real-cohesive homotopy type theory
• Constructivism in mathematics. An introduction. Volume II
• Cubical type theory: a constructive interpretation of the univalence axiom
• Dynamic Newton-Puiseux theorem
• Homotopy limits in type theory
• Homotopy type theory. Univalent foundations of mathematics
• scientific article; zbMATH DE number 3122423 (Why is no real title available?)
• scientific article; zbMATH DE number 1241699 (Why is no real title available?)
• scientific article; zbMATH DE number 1420782 (Why is no real title available?)
• scientific article; zbMATH DE number 3222098 (Why is no real title available?)
• scientific article; zbMATH DE number 4189687 (Why is no real title available?)
• Internal type theory
• Lawvere-Tierney sheafification in Homotopy Type Theory
• Modalities in homotopy type theory
• On higher inductive types in cubical type theory
• Pointers in Recursion: Exploring the Tropics
• Quantum gauge field theory in cohesive homotopy type theory
• Reedy categories and the \(\varTheta\)-construction
• Semi-simplicial complexes and singular homology
• Stack semantics of type theory
• The univalence axiom for elegant Reedy presheaves
• Toposes without points
• Univalence for inverse diagrams and homotopy canonicity
• Éléments de géométrie algébrique. I: Le langage des schémas. II: Étude globale élémentaire de quelques classe de morphismes. III: Étude cohomologique des faisceaux cohérents (première partie)

Cited in

(8)

• Constructive Sheaf Semantics
• scientific article; zbMATH DE number 6816930 (Why is no real title available?)
• On Church’s thesis in cubical assemblies
• Constructing unprejudiced extensional type theories with choices via modalities
• Greatest HITs: higher inductive types in coinductive definitions via induction under clocks
• A foundation for synthetic algebraic geometry
• Unifying cubical and multimodal type theory
• A foundation for synthetic Stone duality

Describes a project that uses

Uses Software

• cart-cube
• cubicaltt

This page was built for publication: Constructive sheaf models of type theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5084309)