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