Consider a version of HoTT where every type former specifies the "shape" of its identity type definitionally (e.g. an equality of pairs is a pair of equalities, equality of types is equivalence, etc.). With this, it must also provide a corresponding reflexivity and the two following operations.
Firstly, it must prove path induction over its identity type. For this, it may use its induction principle, univalence or anything defined in the definition's context (e.g. (path) induction of "simpler" types or type parameters). Let's call this operation $\textrm j_X$ for each type $X$.
Secondly, it must prove that it respects equivalences in all its type parameters (if it has any). Precisely, it must provide:
$$ \textrm{ap}_{\mathbb U} : (F: \mathbb U \rightarrow \mathbb U) \rightarrow (\alpha \cong \beta) \rightarrow F \alpha \cong F \beta $$
... where for example $F \alpha = \Sigma (x:A[\alpha]) B[\alpha] x$ (brackets signify dependence on symbol in them).
This is then used to prove univalence (and give it computational behaviour).
However, for functions, I'm struggling to prove the path induction principle. Given a type $(x:A) \rightarrow B x$, I don't think I can utilize $\textrm j_A$ nor $\textrm j_{B x}$, since I'm dealing with functions and have no way to construct an inhabitant of $A$ or $B x$. I thought about using $\textrm{ap}_{\mathbb U}$ (in analogy to "univalence implies funext"), but the proof I've come up with so far still relies on "homotopy" induction.
Other possible entry point is to prove $C\, a\, (a, \textrm{refl}) \cong C\, a\, (b, p)$ (where all the symbols are the familiar arguments to path induction, and $a,b$ are functions with $p$ a homotopy between them). To prove that, one needs a (pair of) path(s) $(a, \textrm{refl}) = (b, p)$, and the operation $\textrm{ap}_{(x:A)\rightarrow B\, x} : (F:((x:A)\rightarrow \mathbb U)) \rightarrow a = b \rightarrow F\, a \cong F\, b$. That might be manageable, but I haven't been able to even construct the (dependent) path between $\textrm{refl}$ and $p$.
My question is: is it possible to actually prove path induction for homotopies directly? If not, is it possible to prove $C\, a\, (a, \textrm{refl}) \cong C\, a\, (b, p)$ as outlined above? Or, is it actually impossible to do this without extra guarantees?
A bonus question is if there's some easy "patch" similar to how the universe requires all other types to prove they respect equivalences, which could be used to prove path induction for homotopies, or is just leaving path induction for this particular type undefined for anything except $\textrm{refl}$ inevitable?
Thank you for responses, as this will surely require some more work (since it might be quite non-standard setup).
Note:
When defining the $\textrm{ap}_{\mathbb U}$, one may explicitly use substitutions as in $A[\beta/\alpha]$. So for example, if one's proving it for coproducts $A[\alpha]+B[\alpha]$, one can get $Q_A : A[\alpha] \cong A[\beta/\alpha]$ by $Q_A = \textrm{ap}_{\mathbb U}^{\lambda t . A[t/\alpha]} Q$ (where $Q: \alpha \cong \beta$).