Computation over non-reflexivity The principle of induction over identity families, do not prohibit instances different from refl: x == x but its computation rule is only defined for this instance, i.e. ind(C,c,x,x,refl) :≡ c(x).
If a function defined by path induction receives arguments different from the expected ones for the computation rule e.g. Using the higher inductive type "Interval": ind(D, d, i0, i1, seg) :≡ ? where i0, i1: Interval, seg: i0 == i1:

*

*The computation of the function is undefined?

*This is similar to the case of inr and inl that are irreducible, i.e. inr(a) :≡ inr(a)?

 A: After analyzing, I have come with a conclusion: the path induction principle is not different from other axioms/rules that assert the existence of a function without providing an explicit definition, e.g. $succ: N \rightarrow N, inl: A \rightarrow A + B$.
As axioms, these functions do not need a definition, since a definition should be a proof of the axiom and therefore no longer an axiom. The specific case of $inr(a) :≡ inr(a)$ is due to $inr$ been not defined but rather taken as an axiom.
Path induction have the same behavior, $ind(C,c,x,y,p) :≡ ind(C,c,x,y,p)$ but have an exception when the arguments are $(x,x,refl_x)$, in this case is reducible to $c(x)$.
This seems to be where the so called non-trivial paths come, since the cases when $p \neq relf_x$ are the ones that cannot be reduced to the reflexive case $c(x)$ but exists even if they are irreducible.
e.g.
In the case of $S^1$ we have elements:
$base: S^1, loop: base = base$
We can define the inverse of loop by path induction
$loop^{-1} :≡ ind((x,y,p) \Rightarrow y = x, x \Rightarrow refl_x, base, 
base, loop)$
Since $loop \neq refl_{base}$ (Lemma 6.4.1 of the HoTT book) the definition of $loop^{-1}$ is irreducible and different from loop itself.
The proof that this new element is indeed different from loop can be seen with the equivalence $\Omega(S^1) \simeq Z $ (described on HoTT book section 8.1) that also shows that using this same irreducible non-reflexive paths we can build other new different non-reflexive paths.
