Homotopy type theory: working invariantly in homotopy theory