Homotopy type theory: working invariantly in homotopy theory -Guillaume Brunerie