Unifying Cubical Models of Univalent Type Theory

DOI10.4230/LIPICS.CSL.2020.14MaRDI QIDQ5874200zbMATH OpenOpenAlexFDO

Authors Evan Cavallo, Anders Mörtberg, Andrew Swan

Publication date 7 February 2023

Full work available at URL https://drops.dagstuhl.de/opus/volltexte/2020/11657/pdf/LIPIcs-CSL-2020-14.pdf/

zbMATH Keywords

cubical set modelscubical type theoryhomotopy type theoryunivalent foundations

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Cited in

(14)

• scientific article; zbMATH DE number 6694181 (Why is no real title available?)
• scientific article; zbMATH DE number 7003193 (Why is no real title available?)
• Model structures on categories of models of type theories
• Syntax and models of Cartesian cubical type theory
• Cubical methods in homotopy type theory and univalent foundations
• Simplicial sets inside cubical sets
• Induced model structures for higher categories
• Internal Parametricity for Cubical Type Theory
• Finitary type theories with and without contexts
• scientific article; zbMATH DE number 7779294 (Why is no real title available?)
• Transpension: the right adjoint to the Pi-type
• Formalizing the algebraic small object argument in UniMath
• The equivariant model structure on cartesian cubical sets
• Cubical models of -presheaves and the Bousfield-Kan formula

This page was built for publication: Unifying Cubical Models of Univalent Type Theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5874200)