BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Path induction and the indiscernibility of identicals - Emily Rieh
 l (John Hopkins University\, Baltimore) 
DTSTART:20250630T150000Z
DTEND:20250630T160000Z
UID:TALK231394@talks.cam.ac.uk
CONTACT:HoD Secretary\, DPMMS
DESCRIPTION:Mathematics students learn a powerful technique for proving th
 eorems about an arbitrary natural number: the principle of mathematical in
 duction. This talk introduces a closely related proof technique called pat
 h induction\, which can be thought of as an expression of Leibniz's indisc
 ernibility of identicals: if two objects are identified\, then they must h
 ave the same properties\, and conversely. What makes this interesting is t
 hat the notion of identification referenced here is given by Per Martin-L
 öf's intensional identity types\, which encode a more flexible notion of 
 sameness than the traditional equality predicate in that an identification
  can carry data\, for instance of an explicit isomorphism or equivalence. 
 The nickname "path induction" for the elimination rule for identity types 
 derives from a new homotopical interpretation of type theory\, in which th
 e terms of a type define the points of a space and identifications corresp
 ond to paths. In this homotopical context\, indiscernibility of identicals
  is a consequence of the path lifting property of fibrations. Path inducti
 on is then justified by the fact that based path spaces are contractible.\
 n\n"LMS Hardy Lecture":https://www.dpmms.cam.ac.uk/lms-hardy-lecture-2025\
 n
LOCATION:The Chapel Churchill College\, Storey’s Way\, Cambridge\, CB3 0
 DS
END:VEVENT
END:VCALENDAR