Stella Moon: Does Path Induction Need a Justification?

Invitation pdf

Stella Moon (Institute of Philosophy, CAS, Department of Logic):
Does Path Induction Need a Justification?

Homotopy type theory (HoTT) was introduced as an alternative foundation for mathematics going against set theory. In HoTT, the identity elimination rule is called 'path induction'. Some have argued that path induction needs to be justified from pre-mathematical concepts. I challenge this view by taking a Husserlian approach to mathematics and consider path induction from the perspective of the homotopy type theorists. Given this perspective, I argue that path induction can be explained by the path lifting property in homotopy theory, and thus is not in need of a further philosophical justification.