Homotopy Theory
Homotopy n-Type
Uniqueness of identity proofs and Hedbergβs theorem
Truncation
|-|n : A β ||A||n, r : πn + 1 β ||A||n, h
Lemma
is-truncatedn
n-connected
f : A β B β’ is-connectedn
Lemma
is-connected-1
Lemma
f : A β B, g : B β C β’ is-connectedn
Lemma
f : A β B, P : B β U, s β¦ s f :
Corollary
|-|n : A β ||A||n β’ is-connectedn
Corollary
b β¦ a β¦ b : B β
Lemma
f : A β B, g : ||A||n β B β’ is-truncatedn
Lemma
a0 : 1 β A β’
Lemma
f : A β B, P : A β U, Q : B β U, g :
Lemma
P, Q : A β U, f :
Lemma
f : A β B β’ is-connectedn
Orthogonal factorisation
n-truncated
f : A β B β’ is-truncatedn
Lemma
n-image
f : A β B β’ imn
Lemma
f : A β B, f~ : A β imn
Lemma
H : h1 g1 βΌ h2 g2, b : B β’ is-connectedn
Theorem
f : A β B β’ factn
Theorem
e : A β B, m : C β D, Ο :
Lemma
fibf
Reflective subuniverse
P : U β
Modality
β : U β U, Ξ·Aβ : A β βA, indβ :
Ξ©0
Homotopy group
1 β€ n β Οn
Ο1(S1)
βΊ : base = base, βΊβ : β€ β
Universal cover of π1
code
Lemma
transportcode
x : π1 β
encode
encode
decode
transportx' β¦ code
Lemma
x : π1 β p : base = x β _ : decodex
Lemma
x : π1 β
Theorem
_ : x : π1 β
Corollary
Ξ©
Corollary
Ο1
Lemma
Corollary
_ :
Theorem
Ξ©
Theorem
Corollary
x : π1 β _ :
Connectedness of suspensions
Theorem
is-n-connected
Corollary
n : β β is-
Οk β€ n of an n-connected space and Οk < n( Sn)
Lemma
Lemma
Fiber Sequences and the Long Exact Sequence
Pointed Map
Ξ©f
f : X β Y β Ξ©f : Ξ©X β Ξ©Y, Ξ©f
fiber sequence
f : X β Y β X0 β‘ Y, X1 β‘ X, f0 β‘ f, Xn + 1 β‘ fibfn - 1
Lemma
f : X β Y β f1 β‘ pr1 : fibf
ker
Exact sequence of pointed set
f
Theorem
Lemma
Corollary
Οk
Hopf fibration
Hopf fibration
H π^2 π^1 π^3
Corollary
Ο_2
Lemma
- E_Y : Y β U, E_Z : Z β U.
- e_X : x : X β E_y β¦ j
( x) β E_Z β¦ k( x) .
- y : Y β E
( inl( y) ) β‘ E_Y( y) . - z : Z β E
( inr( z) ) β‘ E_Z( z) .
H-space
- A : U,
- e : A,
- ΞΌ : A β A β A,
- a : A β ΞΌ
( e, a) = a β ΞΌ( a, e) = a.
Lemma
A : H-space β a : A β is-equiv
Fibration
A : H-space β Ξ£ A
Lemma
Ξ£A β 2 * A.
The Freudenthal suspension theorem
Lemma
Wedge connectivity lemma
Freudenthal suspension theorem
code
Lemma
Freudenthal equivalence
Stability for spheres
Theorem
Corollary
Corollary
The van Kampen theorem
Naive van Kampen theorem
Example
Example
Example
Van Kampen theorem with a set of basepoints
Whiteheadβs theorem and Whiteheadβs principle
A general statement of the encode-decode method
Additional results
Homotopy
References
- Cubical Synthetic Homotopy Theory. Anders MΓΆrtberg, LoΓ―c Pujet profile imageLoΓ―c Pujet. 2020.
- An Elementary Illustrated Introduction to Simplicial Sets. Greg Friedman. 2021.
- On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory. Floris van Doorn. 2018.
- A Cubical Approach to Synthetic Homotopy Theory. Daniel R. Licata, Guillaume Brunerie. 2015.
- Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study. 2013.