A book on homotopy type theory (HoTT). Free PDF download.