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 2024-04-16.
Files in the synthetic homotopy theory folder
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.26-descent public open import synthetic-homotopy-theory.26-id-pushout 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 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.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-sequential-colimits 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-sequential-diagrams 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.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.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-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.retracts-of-sequential-diagrams public open import synthetic-homotopy-theory.sections-descent-circle 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-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
Recent changes
- 2024-04-16. Vojtěch Štěpančík. Descent data for sequential colimits and its version of the flattening lemma (#1109).
- 2024-04-10. Vojtěch Štěpančík. Shifts and unshifts of concepts around sequential colimits (#1070).
- 2024-04-06. Vojtěch Štěpančík. Rebase infrastructure for coequalizers to double arrows (#1098).
- 2024-03-13. Egbert Rijke. Refactoring pointed types (#1056).
- 2023-12-18. Vojtěch Štěpančík. Flattening lemma for sequential colimits (#972).