Synthetic homotopy theory

Files in the synthetic homotopy theory folder

module synthetic-homotopy-theory where

open import synthetic-homotopy-theory.24-pushouts public
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.cofibers public
open import synthetic-homotopy-theory.descent-circle public
open import synthetic-homotopy-theory.double-loop-spaces 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.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.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.pushouts public
open import synthetic-homotopy-theory.pushouts-of-pointed-types 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.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-pushouts public
open import synthetic-homotopy-theory.wedges-of-pointed-types public