Constructive sheaf models of type theory
From MaRDI portal
Publication:5084309
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
homotopy type theorydependent type theorysheaf modelsconstructive models of univalenceleft-exact modalities
Related Items
Uses Software
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
