The correspondence between homotopy types and higher categorical analogs of groupoids which was first conjectured by Alexander Grothendieck naturally leads to a view of mathematics where sets are used to parametrize collections of objects without "internal structure" while collections of objects with "internal structure" are parametrized by more general homotopy types. Univalent Foundations are based on the combination of this view with the discovery that it is possible to directly formalize reasoning about homotopy types using Martin-Lof type theories.In this talk I will explain how to define usual mathematical objects starting with homotopy types instead of sets and show how to use Coq to reason about homotopy types.