I will explain the logic underlying univalent mathematics and Voevodsky's univalence axiom. I will also give examples of theorems, constructions and proofs in constructive univalent mathematics from my recent work.