Synthetic homotopy theory
Content created by Egbert Rijke, Fredrik Bakke, Vojtěch Štěpančík, Tom de Jong, Raymond Baker and Jonathan Prieto-Cubides.
Created on 2021-12-21.
Last modified on 2025-02-27.
{-# OPTIONS --rewriting --guardedness #-}
Modules in the synthetic homotopy theory namespace
module synthetic-homotopy-theory where open import synthetic-homotopy-theory.0-acyclic-maps public open import synthetic-homotopy-theory.0-acyclic-types public open import synthetic-homotopy-theory.1-acyclic-types public open import synthetic-homotopy-theory.acyclic-maps public open import synthetic-homotopy-theory.acyclic-types public open import synthetic-homotopy-theory.category-of-connected-set-bundles-circle public open import synthetic-homotopy-theory.cavallos-trick public open import synthetic-homotopy-theory.circle public open import synthetic-homotopy-theory.cocartesian-morphisms-arrows public open import synthetic-homotopy-theory.cocones-under-pointed-span-diagrams public open import synthetic-homotopy-theory.cocones-under-sequential-diagrams public open import synthetic-homotopy-theory.cocones-under-spans public open import synthetic-homotopy-theory.codiagonals-of-maps public open import synthetic-homotopy-theory.coequalizers public open import synthetic-homotopy-theory.cofibers-of-maps public open import synthetic-homotopy-theory.cofibers-of-pointed-maps public open import synthetic-homotopy-theory.coforks public open import synthetic-homotopy-theory.coforks-cocones-under-sequential-diagrams public open import synthetic-homotopy-theory.conjugation-loops public open import synthetic-homotopy-theory.connected-set-bundles-circle public open import synthetic-homotopy-theory.connective-prespectra public open import synthetic-homotopy-theory.connective-spectra public open import synthetic-homotopy-theory.dependent-cocones-under-sequential-diagrams public open import synthetic-homotopy-theory.dependent-cocones-under-spans public open import synthetic-homotopy-theory.dependent-coforks public open import synthetic-homotopy-theory.dependent-descent-circle public open import synthetic-homotopy-theory.dependent-pullback-property-pushouts public open import synthetic-homotopy-theory.dependent-pushout-products public open import synthetic-homotopy-theory.dependent-sequential-diagrams public open import synthetic-homotopy-theory.dependent-suspension-structures public open import synthetic-homotopy-theory.dependent-universal-property-coequalizers public open import synthetic-homotopy-theory.dependent-universal-property-pushouts public open import synthetic-homotopy-theory.dependent-universal-property-sequential-colimits public open import synthetic-homotopy-theory.dependent-universal-property-suspensions public open import synthetic-homotopy-theory.descent-circle public open import synthetic-homotopy-theory.descent-circle-constant-families public open import synthetic-homotopy-theory.descent-circle-dependent-pair-types public open import synthetic-homotopy-theory.descent-circle-equivalence-types public open import synthetic-homotopy-theory.descent-circle-function-types public open import synthetic-homotopy-theory.descent-circle-subtypes public open import synthetic-homotopy-theory.descent-data-equivalence-types-over-pushouts public open import synthetic-homotopy-theory.descent-data-function-types-over-pushouts public open import synthetic-homotopy-theory.descent-data-identity-types-over-pushouts public open import synthetic-homotopy-theory.descent-data-pushouts public open import synthetic-homotopy-theory.descent-data-sequential-colimits public open import synthetic-homotopy-theory.descent-property-pushouts public open import synthetic-homotopy-theory.descent-property-sequential-colimits public open import synthetic-homotopy-theory.double-loop-spaces public open import synthetic-homotopy-theory.eckmann-hilton-argument public open import synthetic-homotopy-theory.equifibered-sequential-diagrams public open import synthetic-homotopy-theory.equivalences-cocones-under-equivalences-sequential-diagrams public open import synthetic-homotopy-theory.equivalences-coforks-under-equivalences-double-arrows public open import synthetic-homotopy-theory.equivalences-dependent-sequential-diagrams public open import synthetic-homotopy-theory.equivalences-descent-data-pushouts public open import synthetic-homotopy-theory.equivalences-sequential-diagrams public open import synthetic-homotopy-theory.families-descent-data-pushouts public open import synthetic-homotopy-theory.families-descent-data-sequential-colimits public open import synthetic-homotopy-theory.flattening-lemma-coequalizers public open import synthetic-homotopy-theory.flattening-lemma-pushouts public open import synthetic-homotopy-theory.flattening-lemma-sequential-colimits public open import synthetic-homotopy-theory.free-loops public open import synthetic-homotopy-theory.functoriality-loop-spaces public open import synthetic-homotopy-theory.functoriality-sequential-colimits public open import synthetic-homotopy-theory.functoriality-suspensions public open import synthetic-homotopy-theory.groups-of-loops-in-1-types public open import synthetic-homotopy-theory.hatchers-acyclic-type public open import synthetic-homotopy-theory.homotopy-groups public open import synthetic-homotopy-theory.identity-systems-descent-data-pushouts public open import synthetic-homotopy-theory.induction-principle-pushouts public open import synthetic-homotopy-theory.infinite-complex-projective-space public open import synthetic-homotopy-theory.infinite-cyclic-types public open import synthetic-homotopy-theory.interval-type public open import synthetic-homotopy-theory.iterated-loop-spaces public open import synthetic-homotopy-theory.iterated-suspensions-of-pointed-types public open import synthetic-homotopy-theory.join-powers-of-types public open import synthetic-homotopy-theory.joins-of-maps public open import synthetic-homotopy-theory.joins-of-types public open import synthetic-homotopy-theory.left-half-smash-products public open import synthetic-homotopy-theory.loop-homotopy-circle public open import synthetic-homotopy-theory.loop-spaces public open import synthetic-homotopy-theory.maps-of-prespectra public open import synthetic-homotopy-theory.mere-spheres public open import synthetic-homotopy-theory.morphisms-cocones-under-morphisms-sequential-diagrams public open import synthetic-homotopy-theory.morphisms-coforks-under-morphisms-double-arrows public open import synthetic-homotopy-theory.morphisms-dependent-sequential-diagrams public open import synthetic-homotopy-theory.morphisms-descent-data-circle public open import synthetic-homotopy-theory.morphisms-descent-data-pushouts public open import synthetic-homotopy-theory.morphisms-sequential-diagrams public open import synthetic-homotopy-theory.multiplication-circle public open import synthetic-homotopy-theory.null-cocones-under-pointed-span-diagrams public open import synthetic-homotopy-theory.plus-principle public open import synthetic-homotopy-theory.powers-of-loops public open import synthetic-homotopy-theory.premanifolds public open import synthetic-homotopy-theory.prespectra public open import synthetic-homotopy-theory.pullback-property-pushouts public open import synthetic-homotopy-theory.pushout-products public open import synthetic-homotopy-theory.pushouts public open import synthetic-homotopy-theory.pushouts-of-pointed-types public open import synthetic-homotopy-theory.recursion-principle-pushouts public open import synthetic-homotopy-theory.retracts-of-sequential-diagrams public open import synthetic-homotopy-theory.rewriting-pushouts public open import synthetic-homotopy-theory.sections-descent-circle public open import synthetic-homotopy-theory.sections-descent-data-pushouts public open import synthetic-homotopy-theory.sequential-colimits public open import synthetic-homotopy-theory.sequential-diagrams public open import synthetic-homotopy-theory.sequentially-compact-types public open import synthetic-homotopy-theory.shifts-sequential-diagrams public open import synthetic-homotopy-theory.smash-products-of-pointed-types public open import synthetic-homotopy-theory.spectra public open import synthetic-homotopy-theory.sphere-prespectrum public open import synthetic-homotopy-theory.spheres public open import synthetic-homotopy-theory.suspension-prespectra public open import synthetic-homotopy-theory.suspension-structures public open import synthetic-homotopy-theory.suspensions-of-pointed-types public open import synthetic-homotopy-theory.suspensions-of-propositions public open import synthetic-homotopy-theory.suspensions-of-types public open import synthetic-homotopy-theory.tangent-spheres public open import synthetic-homotopy-theory.total-cocones-families-sequential-diagrams public open import synthetic-homotopy-theory.total-sequential-diagrams public open import synthetic-homotopy-theory.triple-loop-spaces public open import synthetic-homotopy-theory.truncated-acyclic-maps public open import synthetic-homotopy-theory.truncated-acyclic-types public open import synthetic-homotopy-theory.universal-cover-circle public open import synthetic-homotopy-theory.universal-property-circle public open import synthetic-homotopy-theory.universal-property-coequalizers public open import synthetic-homotopy-theory.universal-property-pushouts public open import synthetic-homotopy-theory.universal-property-sequential-colimits public open import synthetic-homotopy-theory.universal-property-suspensions public open import synthetic-homotopy-theory.universal-property-suspensions-of-pointed-types public open import synthetic-homotopy-theory.wedges-of-pointed-types public open import synthetic-homotopy-theory.zigzags-sequential-diagrams public
Recent changes
- 2025-02-27. Egbert Rijke and Fredrik Bakke. Cleaning up for homotopy groups (#836).
- 2025-02-14. Fredrik Bakke. Define left half-smash products (#1320).
- 2025-01-07. Fredrik Bakke. Logic (#1226).
- 2024-10-18. Fredrik Bakke. Abelian ∞-groups (#1178).
- 2024-09-23. Fredrik Bakke. Some typos, wording improvements, and brief prose additions (#1186).