forked from UniMath/agda-unimath
-
Notifications
You must be signed in to change notification settings - Fork 0
/
synthetic-homotopy-theory.lagda.md
71 lines (68 loc) · 4.29 KB
/
synthetic-homotopy-theory.lagda.md
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
# Synthetic homotopy theory
## Files in the synthetic homotopy theory folder
```agda
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.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
```