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-05-18.

{-# 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.infinite-real-projective-space 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