HoTT course notes : lecture 0910