6533b836fe1ef96bd12a1547

RESEARCH PRODUCT

Inductive types in homotopy type theory

Nicola GambinoKristina SojakovaSteve Awodey

subject

FOS: Computer and information sciencesComputer Science - Logic in Computer Science03B15 03B70 03F500102 computer and information sciences01 natural sciencesComputer Science::Logic in Computer ScienceFOS: MathematicsA¹ homotopy theoryCategory Theory (math.CT)0101 mathematicsMathematicsHomotopy lifting propertyType theory inductive types homotopy-initial algebraHomotopy010102 general mathematicsMathematics - Category TheoryIntuitionistic type theoryMathematics - LogicSettore MAT/01 - Logica MatematicaLogic in Computer Science (cs.LO)Algebran-connectedType theoryTheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES010201 computation theory & mathematicsProof theoryTheoryofComputation_LOGICSANDMEANINGSOFPROGRAMSHomotopy type theoryComputer Science::Programming LanguagesLogic (math.LO)

description

Homotopy type theory is an interpretation of Martin-L\"of's constructive type theory into abstract homotopy theory. There results a link between constructive mathematics and algebraic topology, providing topological semantics for intensional systems of type theory as well as a computational approach to algebraic topology via type theory-based proof assistants such as Coq. The present work investigates inductive types in this setting. Modified rules for inductive types, including types of well-founded trees, or W-types, are presented, and the basic homotopical semantics of such types are determined. Proofs of all results have been formally verified by the Coq proof assistant, and the proof scripts for this verification form an essential component of this research.

yearjournalcountryeditionlanguage
2012-01-18
10.1109/lics.2012.21http://hdl.handle.net/10447/74875