scientific article; zbMATH DE number 7559277

DOI10.4230/LIPIcs.FSCD.2019.11MaRDI QIDQ5089011

Simon Huber, Thierry Coquand, Christian Sattler

Publication date: 18 July 2022

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

zbMATH Keywords

univalencecanonicitycubical type theoryArtin glueingsconing

Mathematics Subject Classification ID

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

Related Items (4)

Unnamed Item ⋮ 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

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Partial Horn logic and Cartesian categories
• Generalized algebraic theories and contextual categories
• The Frobenius condition, right properness, and uniform fibrations
• Canonicity for cubical type theory
• Canonicity and normalization for dependent type theory
• An algebraic weak factorisation system on 01-substitution sets: a constructive proof
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• Internal type theory
• Polynomial functors and polynomial monads
• On Higher Inductive Types in Cubical Type Theory
• A cubical approach to straightening
• Parametricity and dependent types
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Intensional interpretations of functionals of finite type I
• Univalence for inverse diagrams and homotopy canonicity

This page was built for publication: