HoTT에서 equivalence를 path를 활용해서 정의하잖아요.
그런데 이런식의 정의는 직관주의 타입 이론과는 다르게 굉장히 비직관적인(비구성적인) 요소를 도입하는 것 처럼 보입니다.
두 대상의 "같음"과, 두 대상 사이의 "path" 사이에 어떤 관계가 있는지 잘 모르겠습니다. 왜 하필 "같음"이라는 것이 "path"로 표현되어야만 하는지 잘 모르겠습니다.(Path 라는 개념이 임의적으로 만들어진 개념 같음. 왜 다른 형태도 아니고 하필 두 대상 사이의 "선" 같은 것인가?)
왜 하필 path라는 위상수학적 의미가 들어간 대상으로 equivalence를 표현해야 하나요?
그야 homotopy가 애초에 위상수학에서 온거니까요?
path type은 (co)inductive type은 아니지만, cubicaltt 같은거 보면 path type에 대해서도 computation rule을 줘서 normalization property가 성립하게 만들 수 있음 - dc App
그리고 HoTT 이전에도 MLTT의 identity type이 groupoid가 된다는 관찰이 먼저 있었음.
그러니까 identity type을 path로 이해하는게 아무 맥락없이 나온건 아닌거지