Why not W?

DOI10.4230/LIPICS.TYPES.2020.8MaRDI QIDQ7232185zbMATH OpenFDO

Authors Jasper Hugunin

Publication date 22 April 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4230/LIPICS.TYPES.2020.8

zbMATH Keywords

\(\mathtt{W}\) typesdependent typesinductive typesintensional type theory

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cites work

• Cubical type theory: a constructive interpretation of the univalence axiom
• Homotopy type theory. Univalent foundations of mathematics
• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 1342277 (Why is no real title available?)
• scientific article; zbMATH DE number 2111733 (Why is no real title available?)
• Representing inductively defined sets by wellorderings in Martin-Löf's type theory
• The gentle art of levitation
• Variations on inductive-recursive definitions

This page was built for publication: Why not \(\mathtt{W}\)?

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