Type Theory at SSFT - slides and exercises -