scientific article; zbMATH DE number 7559297

DOI10.4230/LIPIcs.FSCD.2019.31MaRDI QIDQ5089034

Jonathan Sterling, Daniel Gratzer, Carlo Angiuli

Publication date: 18 July 2022

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

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

canonicitydependent type theorycubical type theoryextensional equalitycategorical gluing

Mathematics Subject Classification ID

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

Related Items (4)

Constructing a universe for the setoid model ⋮ Unnamed Item ⋮ Cubical Agda: A dependently typed programming language with univalence and higher inductive types ⋮ Syntax and models of Cartesian cubical type theory

Cites Work

• Generalized algebraic theories and contextual categories
• Wellfounded trees in categories
• A cubical model of homotopy type theory
• Canonicity for cubical type theory
• Type theory in type theory using quotient inductive types
• Words, free algebras, and coequalizers
• Internal type theory
• Propositions as [Types]
• Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
• Syntax and Semantics of Quantitative Type Theory
• On Higher Inductive Types in Cubical Type Theory
• Small Induction Recursion
• Homotopy Type Theory: Univalent Foundations of Mathematics
• On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory
• Higher Topos Theory (AM-170)
• Univalence for inverse diagrams and homotopy canonicity
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: