Synthetic homotopy theory
Content created by Egbert Rijke, Fredrik Bakke, Vojtěch Štěpančík, Raymond Baker and Jonathan Prieto-Cubides.
Created on 2021-12-21.
Last modified on 2023-09-24.
Files in the synthetic homotopy theory folder
module synthetic-homotopy-theory where open import synthetic-homotopy-theory.26-descent public open import synthetic-homotopy-theory.26-id-pushout public open import synthetic-homotopy-theory.27-sequences public open import synthetic-homotopy-theory.acyclic-maps public open import synthetic-homotopy-theory.acyclic-types public open import synthetic-homotopy-theory.cavallos-trick public open import synthetic-homotopy-theory.circle public open import synthetic-homotopy-theory.cocones-under-spans public open import synthetic-homotopy-theory.cocones-under-spans-of-pointed-types 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.conjugation-loops 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-pullback-property-pushouts 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-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.double-loop-spaces public open import synthetic-homotopy-theory.eckmann-hilton-argument public open import synthetic-homotopy-theory.flattening-lemma-coequalizers public open import synthetic-homotopy-theory.flattening-lemma-pushouts public open import synthetic-homotopy-theory.free-loops public open import synthetic-homotopy-theory.functoriality-loop-spaces 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.join-powers-of-types public open import synthetic-homotopy-theory.joins-of-types public open import synthetic-homotopy-theory.loop-spaces public open import synthetic-homotopy-theory.multiplication-circle public open import synthetic-homotopy-theory.plus-principle public open import synthetic-homotopy-theory.powers-of-loops public open import synthetic-homotopy-theory.prespectra public open import synthetic-homotopy-theory.pullback-property-pushouts public open import synthetic-homotopy-theory.pushouts public open import synthetic-homotopy-theory.pushouts-of-pointed-types public open import synthetic-homotopy-theory.sections-descent-circle public open import synthetic-homotopy-theory.smash-products-of-pointed-types public open import synthetic-homotopy-theory.spectra public open import synthetic-homotopy-theory.spheres 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.triple-loop-spaces 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-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
- 2023-09-24. Raymond Baker. Refactor Eckmann-Hilton (#788).
- 2023-09-20. Vojtěch Štěpančík. Coforks, coequalizers of types, their flattening lemma (#792).
- 2023-09-05. Egbert Rijke. The statement of the flattening lemma (#719).
- 2023-08-28. Raymond Baker and Fredrik Bakke. Suspension reorganization (#700).
- 2023-08-28. Vojtěch Štěpančík. Extending infrastructure for working with descent data for the circle (#709).