PHIL 29405/39405 Advanced Logic
This class will explore dependent type theory, with a focus on the identity relation. Different ways of thinking of the identity relation will be examined, culminating in a presentation of the Univalence axiom and a discussion of its role as a potential foundation for mathematics. (B) (II)
Although background material will be discussed in the first lectures, students will be expected to have some familiarity with the lambda calculus and the theory of types. Interested students without this background should contact the instructor in advance to discuss possible material to read to help prepare for the course.