Homotopy Type Theory - Logic and Its Applications - page 6

Here is a sanity check:

Theorem 2 (Shulman 2011). The type-theoretic circle S has the correct ho-

motopy groups:

)=

Z , if n =1 ,

0 , if n

ˀ n ( S

=1 .

The proof combines classical homotopy theory with methods from constructive
type theory, and uses Voevodsky's Univalence Axiom. It has been formalized in
Coq.

Corollary 1. There are 1 -types. (This also uses univalence).

Higher Inductive Types: The Interval I

The unit interval I =[0 , 1] is also an inductive type, on the data:

:= 0 , 1:

I

I

p :0 1

1forthetype Id I (0 , 1).

again writing 0

Slogan:
In topology , we start with the interval and use it to define the notion of a
path .
In HoTT , we start with the notion of a path , and use it to define the interval .

Higher Inductive Types: Conclusion

Many basic spaces and constructions can be introduced as HITs:

- higher spheres S n ,cylinders,tori,cell complexes,...,
- suspensions ʣA ,
- homotopy pullbacks, pushouts, etc.,
- truncations, such as connected components ˀ 0 ( A ) and “bracket” types [ A ],
- quotients by equivalence relations and general quotients,
- free algebras, algebras for a monad,
- (higher) homotopy groups ˀ n , Eilenberg-MacLane spaces K ( G, n ), Postnikov
systems,
- Quillen model structure,
- real numbers,
- cumulative hierarchy of sets.