Cubical methods in homotopy type theory and univalent foundations
From MaRDI portal
Publication:5055493
DOI10.1017/S0960129521000311OpenAlexW4200353768MaRDI QIDQ5055493
Publication date: 9 December 2022
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1017/s0960129521000311
Related Items (1)
Uses Software
Cites Work
- A cubical model of homotopy type theory
- The Frobenius condition, right properness, and uniform fibrations
- The simplicial model of univalent foundations (after Voevodsky)
- Revisiting the categorical interpretation of dependent type theory
- The univalence axiom in cubical sets
- Canonicity for cubical type theory
- Guarded cubical type theory
- Formalizing CCS and \(\pi\)-calculus in Guarded Cubical Agda
- Categorical Homotopy Theory
- The Local Universes Model
- The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories
- Locally cartesian closed categories and type theory
- Cubical Type Theory: a constructive interpretation of the univalence axiom
- Internal type theory
- Cubical Agda: A dependently typed programming language with univalence and higher inductive types
- Syntax and models of Cartesian cubical type theory
- On Church’s thesis in cubical assemblies
- Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
- On Higher Inductive Types in Cubical Type Theory
- Varieties of Cubical Sets
- Homotopy Type Theory: Univalent Foundations of Mathematics
- An experimental library of formalized Mathematics based on the univalent foundations
- Unifying Cubical Models of Univalent Type Theory
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Cubical methods in homotopy type theory and univalent foundations
