  We introduce Voevodsky's univalent foundations and univalent mathematics, and
explain how to develop them with the computer system Agda, which is based on
Martin-L\"of type theory. Agda allows us to write mathematical definitions,
constructions, theorems and proofs, for example in number theory, analysis,
group theory, topology, category theory or programming language theory,
checking them for logical and mathematical correctness.
  Agda is a constructive mathematical system by default, which amounts to
saying that it can also be considered as a programming language for
manipulating mathematical objects. But we can assume the axiom of choice or the
principle of excluded middle for pieces of mathematics that require them, at
the cost of losing the implicit programming-language character of the system.
For a fully constructive development of univalent mathematics in Agda, we would
need to use its new cubical flavour, and we hope these notes provide a base for
researchers interested in learning cubical type theory and cubical Agda as the
next step.
  Compared to most expositions of the subject, we work with explicit universe
levels.
