Cubical methods in homotopy type theory and univalent foundations

DOI10.1017/S0960129521000311OpenAlexW4200353768MaRDI QIDQ5055493

Anders Mörtberg

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

zbMATH Keywords

homotopy type theoryunivalent foundationscubical type theorycubical set models

Mathematics Subject Classification ID

Computer science (68-XX)

Related Items (1)

Combining higher-order logic with set theory formalizations

Uses Software

• Nuprl
• cubicaltt
• GitHub
• RedPRL
• cart-cube

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