Homotopy-initial algebras in type theory

DOI10.1145/3006383zbMATH Open1426.03016arXiv1504.05531OpenAlexW2963024429WikidataQ59890116 ScholiaQ59890116MaRDI QIDQ3177878FDOQ3177878

Authors: Nicola Gambino, Kristina Sojakova, Steve Awodey 

Publication date: 2 August 2018

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

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.

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

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

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)

Cited In (15)

• Pro-algebraic homotopy types
• Title not available (Why is that?)
• Title not available (Why is that?)
• Topological quantum gates in homotopy type theory
• Every Elementary Higher Topos has a Natural Number Object
• On the internal structures of inductive types
• Mathesis Universalis and Homotopy Type Theory
• Semantics of higher inductive types
• W-types in setoids
• Higher inductive types as homotopy-initial algebras
• Towards Constructive Homological Algebra in Type Theory
• Algebraic models for homotopy types
• Homotopy Type Theory
• Lawvere-Tierney sheafification in Homotopy Type Theory
• Cellular Cohomology in Homotopy Type Theory

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)