Abstract: We will introduce the Univalence Axiom and discuss a few of its immediate consequences such as existence of types that are not sets, function extensionality or preservation of n-types by dependent products.