Homotopy type theory and synthetic homotopy theory