An implementation of effective homotopy of fibrations

DOI10.1016/j.jsc.2018.08.001zbMath1436.55022OpenAlexW2885035470WikidataQ125883803 ScholiaQ125883803MaRDI QIDQ2422709

Francis Sergeraert, Ana Romero, Julio Jesús Rubio García

Publication date: 20 June 2019

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jsc.2018.08.001

zbMATH Keywords

finitely generated groupscentral extensionsfibrationshomotopy groupsconstructive algebraic topologyeffective homotopyeffective setoid groupsSerre exact sequencesetoid groups

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Fiber spaces in algebraic topology (55R05)

Uses Software

• Kenzo
• Agda
• cubicaltt

Cites Work

• Unnamed Item
• Unnamed Item
• Effective homotopy of fibrations
• Finite computability of Postnikov complexes
• Stable homotopy groups of spheres. A computer-assisted approach
• The computability problem in algebraic topology
• Computational homology
• Constructive algebraic topology
• A Bousfield-Kan algorithm for computing the \textit{effective} homotopy of a space
• A combinatorial tool for computing the effective homotopy of iterated loop spaces
• Homotopy limits, completions and localizations
• Homologie singulière des espaces fibrés. Applications
• Groupes d'homotopie et classes de groupes abéliens
• A Brief Overview of Agda – A Functional Language with Dependent Types
• Effective algebraic topology
• Homotopy groups of suspended classifying spaces: An experimental approach
• Homotopy Type Theory: Univalent Foundations of Mathematics