Homotopy-initial algebras in type theory

DOI10.1145/3006383MaRDI QIDQ3177878zbMATHOpenAlexWikidataFDO

Authors Nicola Gambino, Kristina Sojakova, Steve Awodey

Publication date 2 August 2018

Published in Journal of the ACM (Search for Journal in Brave)

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

zbMATH Keywords

recursioninductionhomotopy type theoryinitial algebraW-types

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Theories (e.g., algebraic theories), structure, and semantics (18C10) Abstract and axiomatic homotopy theory in algebraic topology (55U35) Type theory (03B38)

Abstract: We investigate inductive types in type theory, using the insights provided by homotopy type theory and univalent foundations of mathematics. We do so by introducing the new notion of a homotopy-initial algebra. This notion is defined by a purely type-theoretic contractibility condition which replaces the standard, category-theoretic universal property involving the existence and uniqueness of appropriate morphisms. Our main result characterises the types that are equivalent to W-types as homotopy-initial algebras.

Recommendations

• Higher inductive types as homotopy-initial algebras
• Inductive types in homotopy type theory
• Semantics of constructions. II: The initial algebraic approach
• Semantics of higher inductive types
• A categorical semantics for inductive-inductive definitions

Cited in

(16)

• Mathesis Universalis and Homotopy Type Theory
• Lawvere-Tierney sheafification in Homotopy Type Theory
• Every elementary higher topos has a natural number object
• Topological quantum gates in homotopy type theory
• Higher inductive types as homotopy-initial algebras
• Algebraic models for homotopy types
• Homotopy Type Theory
• Towards Constructive Homological Algebra in Type Theory
• On the internal structures of inductive types
• scientific article; zbMATH DE number 1420784 (Why is no real title available?)
• scientific article; zbMATH DE number 3949678 (Why is no real title available?)
• Inductive types in homotopy type theory
• Cellular Cohomology in Homotopy Type Theory
• W-types in setoids
• Pro-algebraic homotopy types
• Semantics of higher inductive types

This page was built for publication: Homotopy-initial algebras in type theory

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