An application of path induction Does the rule of path induction (based or unbased, I don't care) allow us to infer
$$u:A, \ v:A, \ p:u=_A v \vdash t: p = \mbox{refl}(u) \hskip 1 cm (*)$$
for some term $t$? It seems to me that this should follow from unbased path induction on $\mbox{refl}(x)=\mbox{refl}(x)$, but I am not sure.
If so, then it seems to me that path induction in general just follows from $(*)$ and the principle of the indiscernibility of identicals, as $(*)$ just tells us that any object $p$ of type $u=_A v$ and refl$(u)$ are identical, and therefore mutually substitutable. So $(*)$ seems to express the main idea of path-induction. Worries about why we should accept path induction then seem to me to boil down to worries about whether we should accept $(*)$ -- i.e., whether we should accept the claim that all elements of identity types are propositionally equal to refl.
 A: No. This assertion isn’t even well-typed.
Recall that for every type $B$, there is a type family $x, y: B \mapsto x =_B y$. It only makes syntactic sense to write $x =_B y$ when both $x$ and $y$ are of type $B$. When it is clear from context what the type of $x$ and $y$ is, we abusively write $x = y$ for simplicity, but the $B$ is implicit. $\DeclareMathOperator{refl}{refl}$
In this context, we have a type $A$, elements $u, v : A$, and a path $p : u =_A v$. We can form the term $\refl(u) : u =_A u$. When you write the term $p =_B \refl(u)$, what is the type $B$ you are using? You can’t find one that works syntactically because it cannot be shown that $u =_A u$ and $u =_A v$ are judgementally equal.
There is a well-typed version of this problem. We can ask whether $\prod u : A \prod p : u =_A u, p =_{u =_A u} \refl(u)$. If type $A$ satisfies this criterion, it is said to be a set (or to satisfy axiom K). In homotopy type theory, we deliberately postulate types for which this fails. For example, the circle has a base point $base$ where the type $base = base$ is actually equivalent to the set of integers. There is one path from $base$ to itself for each integer. This is consistent with the topological observation that the fundamental group of the circle is the integers.
However, if you are using extensional type theory, this assertion is well-typed and provable. Extensional type theory has some serious issues, however - type checking is actually computationally undecidable. There is no program that can decide whether an assertion type-checks. This is a serious issue if you want your type theory to be a new foundation of mathematics.
