Constructive sheaf models of type theory

DOI10.1017/S0960129521000359OpenAlexW3217362411MaRDI QIDQ5084309

Fabian Ruch, Thierry Coquand, Christian Sattler

Publication date: 24 June 2022

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

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

zbMATH Keywords

homotopy type theorydependent type theorysheaf modelsconstructive models of univalenceleft-exact modalities

Mathematics Subject Classification ID

Type theory (03B38)

Related Items (1)

On Church’s thesis in cubical assemblies

Uses Software

• cubicaltt
• cart-cube

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Constructivism in mathematics. An introduction. Volume II
• Toposes without points
• Reedy categories and the \(\varTheta\)-construction
• É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)
• Semi-simplicial complexes and singular homology
• Dynamic Newton–Puiseux theorem
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• Brouwer's fixed-point theorem in real-cohesive homotopy type theory
• Internal type theory
• Quantum Gauge Field Theory in Cohesive Homotopy Type Theory
• Pointers in Recursion: Exploring the Tropics
• On Higher Inductive Types in Cubical Type Theory
• A Constructive Model of Directed Univalence in Bicubical Sets
• Lawvere-Tierney sheafification in Homotopy Type Theory
• Modalities in homotopy type theory
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Homotopy limits in type theory
• Univalence for inverse diagrams and homotopy canonicity
• An experimental library of formalized Mathematics based on the univalent foundations
• The univalence axiom for elegant Reedy presheaves

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