Cubical syntax for reflection-free extensional equality

DOI10.4230/LIPICS.FSCD.2019.31MaRDI QIDQ5089034zbMATH OpenFDO

Authors Jonathan Sterling, Daniel Gratzer, Carlo Angiuli

Publication date 18 July 2022

Full work available at URL https://arxiv.org/abs/1904.08562

zbMATH Keywords

canonicitycategorical gluingcubical type theorydependent type theoryextensional equality

Mathematics Subject Classification ID

Logic in computer science (03B70) Theory of computing (68Qxx)

Recommendations

• A cubical language for Bishop sets
• Canonicity for cubical type theory
• Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
• Guarded cubical type theory

Cites work

• A cubical model of homotopy type theory
• Canonicity for cubical type theory
• Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
• Generalized algebraic theories and contextual categories
• Higher Topos Theory (AM-170)
• Homotopy type theory. Univalent foundations of mathematics
• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• scientific article; zbMATH DE number 3692654 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 1289305 (Why is no real title available?)
• scientific article; zbMATH DE number 1302059 (Why is no real title available?)
• scientific article; zbMATH DE number 512784 (Why is no real title available?)
• scientific article; zbMATH DE number 6816943 (Why is no real title available?)
• scientific article; zbMATH DE number 226803 (Why is no real title available?)
• scientific article; zbMATH DE number 3310901 (Why is no real title available?)
• Internal type theory
• On higher inductive types in cubical type theory
• On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory
• Propositions as [Types]
• Small induction recursion
• Syntax and semantics of quantitative type theory
• Type theory in type theory using quotient inductive types
• Univalence for inverse diagrams and homotopy canonicity
• Wellfounded trees in categories
• Words, free algebras, and coequalizers

Cited in

(6)

• Constructing a universe for the setoid model
• Cubical Agda: a dependently typed programming language with univalence and higher inductive types
• Syntax and models of Cartesian cubical type theory
• A cubical language for Bishop sets
• Cubical Syntax for Reflection-Free Extensional Equality
• Normalization for multimodal type theory

This page was built for publication: Cubical syntax for reflection-free extensional equality

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