Syntax and models of Cartesian cubical type theory
From MaRDI portal
Publication:5022926
Recommendations
Cites work
- A Constructive Model of Directed Univalence in Bicubical Sets
- A cubical approach to synthetic homotopy theory
- A cubical model of homotopy type theory
- A Kripke model for simplicial sets
- A presheaf model of parametric type theory
- A type theory for synthetic -categories
- ABSTRACT HOMOTOPY
- An algebraic weak factorisation system on 01-substitution sets: a constructive proof
- Axioms for modelling cubical type theory in a topos
- Canonicity for cubical type theory
- Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
- Computational higher-dimensional type theory
- Cubical Agda: a dependently typed programming language with univalence and higher inductive types
- Cubical syntax for reflection-free extensional equality
- Cubical type theory: a constructive interpretation of the univalence axiom
- Guarded cubical type theory
- Homotopy canonicity for cubical type theory
- Homotopy type theory. Univalent foundations of mathematics
- scientific article; zbMATH DE number 6694181 (Why is no real title available?)
- scientific article; zbMATH DE number 7003193 (Why is no real title available?)
- Internal universes in models of homotopy type theory
- Meaning explanations at higher dimension
- Nominal presentation of cubical sets models of type theory
- On higher inductive types in cubical type theory
- Presheaves as models for homotopy types
- The Frobenius condition, right properness, and uniform fibrations
- The simplicial model of univalent foundations (after Voevodsky)
- The univalence axiom in cubical sets
- Unifying Cubical Models of Univalent Type Theory
- Varieties of cubical sets
Cited in
(26)- scientific article; zbMATH DE number 6694181 (Why is no real title available?)
- On the Nielsen-Schreier theorem in homotopy type theory
- Cubical methods in homotopy type theory and univalent foundations
- Naive cubical type theory
- Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
- A cubical language for Bishop sets
- Geometry of synthesis III
- Simplicial sets inside cubical sets
- A formal logic for formal category theory
- Kripke-Joyal forcing for type theory and uniform fibrations
- A 2-categorical proof of Frobenius for fibrations defined from a generic point
- Single-set cubical categories and their formalisation with a proof assistant
- Parametricity via cohesion
- Hefty algebras: modular elaboration of higher-order effects
- Automating boundary filling in cubical Agda
- Controlling unfolding in type theory
- Toward the effective 2-topos
- A short proof of the Frobenius property for generic fibrations
- A parametricity-based formalization of semi-simplicial and semi-cubical sets
- Unifying cubical and multimodal type theory
- A toolkit for structured lifts
- The equivariant model structure on cartesian cubical sets
- Strict universes for Grothendieck topoi
- Complexity of cubical cofibration logics. I: coNP-complete examples
- Hofmann-Streicher lifting of fibred categories (extended version)
- Cubical models of -presheaves and the Bousfield-Kan formula
This page was built for publication: Syntax and models of Cartesian cubical type theory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5022926)
